[TYPES] Colimit Construction

[Jesper Carlström]

Geoffrey,

I thought about arbitrary colimits of setoids (sets with equivalence
relations) and wrote a preprint about it, see
http://www.math.su.se/~jesper/research/limitsinsetoid/. Maybe this helps
in seeing the pattern.

According to that construction, the colimit is the sum, but with an
equivalence relation which identifies a lot of things. In your case, the
result is isomorphic to the solution suggested by Christopher A. Stone.

Best,
Jesper Carlström