The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 15 Jan 2014 00:07:17 -0500,
Jason Gross 
<jasongross9 AT gmail.com>
 a écrit :

> The basic category theory does not depend much on HoTT nor
> univalence; the two main dependencies are that you add an extra
> requirement saying "forall x y (f g : Hom x y) (pf1 pf2 : f = g), pf1
> = pf2", and that there is a new notion of a saturated or univalent
> category (alternatively, you can call classical categories
> unsaturated or precategories, and call precategory + univalence a
> category), but you don't need to use that.

What do you call "basic categories"? I never had to add your "forall x
y (f g : Hom x y) (pf1 pf2 : f = g), pf1 = pf2" axiom to do basic stuff
on categories. I guess you need it if you want to define some specific
categories about paths, but that is not what I would call "basic".
Category of groups, monoids and so on do not require such axiom as far
as I know. Still what Coq lacks yet is universe polymorphism if you
want to define the (bigger) category of (smaller) categories without
to define two Types (BigCat and SmallCat).

Well I think there was a similar lemma that I used, but it was not on
higher stuff (morphisms), but only on objects "forall (x y : Obj) (pf1
pf2 : x = y), pf1 = pf2". And here again that was for rather specific
categories (comma categories, I guess, where you can have objects
embeded in morphisms and need composition which does not depend on the
proof that morphisms are composable [ie. codom f = dom g]).