[TYPES] Colimit Construction

[Kevin S. Millikin]

I'm also far from a category theory expert.

But I think that the (co)cones of A --> B might still be interesting
according to the following intuition.

Consider instead of negative? = \x.(x < 0), the length function on
lists (because I find it more instructive, I guess, because length is a
more expensive computation).  Then, the limit of

        length       
List -----------> Int

is just List as Christopher Stone noted, but your cone with vertex the
dependent sum represents the linked-list implementation trick of
representing the list by a tuple (i.e., record) of the list itself and a
field holding the length.  This is an optimization if length is asked of
lists often enough.

I think that the intuition behind the cocone you want, for the length
example again, is the optimization trick of postponing computation of
something like length until we're sure that the value will be demanded
(i.e., a thunk, containing the List before it is forced and the length
afterward).

This seems to match the dependent product that you suggested, right?
----
Kevin S. Millikin           Architecture Technology Corporation
Research Scientist          Specialists in Computer Architecture
(952)829-5864 x162          http://www.atcorp.com