[TYPES] Colimit Construction

[Geoffrey A. Washburn]

 Recently, I've come across a intriguing categorical construction, and
 am curious as to whether anyone has an insight into the nature of its
 dual construction.  The following examples will be in the category where
 the objects are types and the arrows lambda-calculus functions.  We will
 ignore specifying the definition of types and terms for the moment.
 Consider the following diagram is contained in the category (note all
 diagrams are in ASCII, so you will need to be using a monospace font):

                         \x:Int.(x < 0)
                   Int ------------------> Bool

 One interesting question we can ask about this diagram is the nature of
 its categorical limit.  It is not immediately obvious, so we can gain
 some intuition by first looking at the limit of the simpler diagram,
 that of just the objects Int and Bool.

                   Int                     Bool

 It is well known that the limit of this diagram is the product type.


                            Int x Bool
                            /        \
                           /          \
                          /            \
                    fst  /              \  snd
                        /                \
                       /                  \
                      /                    \
                     v                      v
                   Int                     Bool

 Reasoning by analogy the limit of

                         \x:Int.(x < 0)
                   Int ------------------> Bool

 is the same as the limit of

                   Int                     Bool

 with the added constraint that it must make the following diagram commute

                                P?
                            /        \
                           /          \
                          /            \
                    fst  /              \  snd
                        /                \
                       /                  \
                      /                    \
                     v   \x:Int.(x < 0)     v
                   Int ------------------> Bool

 We can think of P as having exactly the same tuple structure as Int
 x Bool, except that it must satisfy the constraint

                    (\x:Int.(x < 0)) o fst = snd

 The only way this constraint can be met is that P only types exactly
 those tuples that have a "true" second component if the first component
 is negative, and "false" if the first component is positive.  So this
 limit is a more precise type than just Int x Bool, it is actually the
 dependent sum type Sigma x:Int.S(x < 0), where S here is the injection
 for singleton types.  In general the limit of a diagram consisting of
 two object with a morphism between them will have a type dependent sum
 type like Sigma x:A.S(f(x)).

 That is all and good, but the natural question we might ask next is what
 about the colimit of the diagram?  Naively we might conclude that the dual
 construction will be a dependent product type Pi x:A.S(f(x)), but this
 does not seem to be the case.

                            Int + Bool
                            ^        ^
                           /          \
                          /            \
                    inl  /              \  inr
                        /                \
                       /                  \
                      /                    \
                     /                      \
                   Int                     Bool

 The colimit of two objects by themselves is the sum type.  Adding our
 morphism only adds an additional constraint that
 inl = (\x:Int.(x < 0)) o inr.

                                 ?
                            ^        ^
                           /          \
                          /            \
                     inl /              \  inr
                        /                \
                       /                  \
                      /                    \
                     /   \x:Int.(x < 0)     \
                   Int ------------------> Bool

 My question is whether anyone has an intuition about the nature of
 this type.  I've concocted some terms and typing rules that seem to
 apply:

 Gamma |- e : A
 ---------------------------------
 Gamma |- inl e : CoSigma x:A.S(f(x))

 Gamma, x:A |- e : S(f(x))
 --------------------------------
 Gamma |- inr e : CoSigma x:A.S(f(x))

 Gamma |- e : CoSigma x:A.S(f(x))
 Gamma, y:A |- e1 : C
 Gamma |- e2 : A
 Gamma, z:S(f(e2)) |- e3 : C
 ------------------------------------------------
 Gamma |- case e of inl y => e1 | z, e2 => e3 : C

 It is possible this is just a completely bogus construct, but it seems
 hard to believe that it doesn't correspond to something we know about.