A few weeks ago I posted a query to the TYPES mailing list about the a nature of a particular categorical construction. In particular, I was interested in the colimit of an individual morphism in the category where objects are types, and arrows terms that are functions between them. Specifically consider the diagram length int list ----------> nat Where I abbreviate the type of integers as int and the type of natural numbers as nat. (All diagrams are in ASCII so you will need to use a proportional font; maybe someday I will be able to use inline SVG diagrams). I figured that it might be instructive to understand the nature of the colimit of this diagram by first considering the limit of this diagram (with its associated UMP) X / | \ f / | \x:X.<f(x),g(x)> \ g / | \ / | \ / | \ / fst v snd \ v <----- Sigma l:int list.S(length(l)) -----> v int list nat ------------------------------------------> length Where snd o \x:X.<f(x),g(x)> = g and length o f = g. This limit Sigma l:int list.S(length(l)) is a dependent sum, essentially a tuple, that constrains its second component to be the natural number that is exactly the length of the list that is its first component. I indicate this by using the singleton type constructor S. S(length(l)) is the type of those terms that are equivalent to length(l). However, it was quickly pointed out to me on the TYPES list that there is a "simpler" limit that is isomorphic to Sigma l:int list.S(length(l)) X / | \ / | \ f / | f \ g / | \ / | \ / id v length \ v <------ int list --------> v int list nat -------------------------> length Where it must be the case that, length o f = g. What is interesting here is that while these two limits are isomorphic, operationally they are very different. We can think of the limit an abstract data-type with two operations, one that will give us a list, or the length of the list it encapsulates. In SML syntax sig type limit val fst : limit -> int list val snd : limit -> nat end When we use int list as the limit, the abstract datatype is lazy, in the sense that it does not compute the length until it is requested. My more "complex" limit on the other-hand is eager, and computes the length when constructed. This actually provides even more intuition as to what is going on with the colimit. First the simpler colimit length ------------------> int list nat \ --------> nat <---- / \ length | id / \ | / \ | / f \ | g / g \ | / \ | / v v v X Where it must be the case that g o length = f. Returning to our abstract datatype analogy, sig type colimit val inl : int list -> colimit val inr : nat -> colimit end Here, our abstract datatype is encapsulates the length of a list, which can either be given directly, or by supplying a list. This simpler colimit can thought of as being eager, because it calculates the length of the list immediately when injecting into the "abstract type". Therefore, if our intuitions are correct, the a dependent colimit should compute the length lazily... length --------------------------------------------> int list nat \ -----> CoSigma l:int list.S(length(l)) <----- / \ inl | inr / \ | / \ | / f \ | [f,g] / g \ | / \ | / v v v X Where [f,g] o inl = f and g o length = f. And indeed it is. Instead of calculating the length immediately, it requires that the function deconstructing the "abstract type" compute length if given a list instead of a length; this is forced by the requirement that f must be the same as g o length. My remaining unanswered questions: Are there any other interesting isomorphic (co)limits than the two discussed above? It is possible to add enough structure to the category so that these (co)limits can be distinguished? Naively we might have expected the dual of a dependent sum type to be a dependent product (as existential types are dual to universal types). Is there a construction that corresponds to the dual of a dependent product? Is there a relationship between the CoSigma type and other known mathematical structures? What are the typing rules for CoSigma? Sigma l:int list.S(length(l)) should be isomorphic to the more common dependent type Sigma n:nat.int list(n). How does CoSigma l:int list.S(length(l)) relate to the type CoSigma n:nat.int list(n)?