[TYPES] Colimit Construction

[Christopher A. Stone]

I am very far from being a category theory expert, but my understanding
is that the limits and colimits can be expressed much more simply.

The limit of the diagram 

          f
   A ---------> B

is the object A, with the arrows being the identity and f rather than
fst and snd.  (This is an exercise in Category Theory for Computer
Science by Barr and Wells.)

And in fact, the suggested limit object  Sigma x:A.S(f(x))  is
isomorphic to A.

So, the colimit of the diagram should just be B, with the arrows being f
and the identity.

Chris

-- 
Christopher A. Stone / Assistant Professor              stone at cs.hmc.edu
Computer Science Department, Harvey Mudd College   www.cs.hmc.edu/~stone
1250 North Dartmouth Avenue, Claremont, CA 91711          (909) 607-8975