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

[xieyuheng <xyheme@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 1186 bytes --]

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

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 1548 bytes --]