is there a categorical construction to generalize arrow composition,
by allowing domain and codomain to be refined (or changed) by the
composition ?

this construction would be useful for
forming theoretical background of dependent type system.

for example, compose two functions
f : (A x -> B y)
g : (B n -> C z)
will give us a function of type (A n -> C z)


another example would be the following generalized composition in cartesian closed category :
        f   : (t1, t2) -> (t3, t4)
        g   : (t, t3, t4) -> (t6, t7)
        f;g : (t, t1, t2) -> (t6, t7)
and
        f   : (t1, t2) -> (t, t3, t4)
        g   : (t3, t4) -> (t6, t7)
        f;g : (t, t1, t2) -> (t, t6, t7)
this can be called `cut`
because it looks like gentzen's cut rule in sequent calculus,
and it can be used to provide semantic
for a stack based concatenative programming language.


------
xieyuheng