HoTT/HoTT — pull request #246 by JasonGross (2013-11-10 14:56:59+00:00)
Title: Comma

Port comma categories, universal morphisms, Kan extensions, and (co)limits.

I'm not terribly happy with the ASCII infix notation `T |v| S`, but I couldn't
figure out how to make `T , S` work, and I don't think I'm supposed to use
unicode.

I haven't figured out how to get the intro and elim rules for (co)limits to behave (I
don't want extra compositions with identity morphisms). I also haven't
ported the morphisms between limits of the same functor, which was in
the catdb file. (That should be straightforward, though, if we want
it.) I might tackle those soon.

The next big port after this one will probably be adjoints, including the proof that (co)limits assemble into a functor adjoint to the constant diagram functor (and similarly for Kan extensions).