The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

The axiom says that your morphisms are a set (homotopically) rather than a space; without it, you are secretly doing (oo, 1)-category theory, in a sense, except without the right coherence laws on your associators and identity laws.  There is a bit more on this in chapter 9 of the HoTT book.  It is never needed for objects, only for morphisms, at least if you use dependently typed morphisms rather than a single class of morphisms + dom and cod functions.  (It's possible that it's also true using dom and cod functions, if you very carefully track your use of proofs of object equality.)  It's quite possible that I don't actually make interesting use of this until I get to comma categories.

HoTT/Coq has (and Coq 8.5 will have) universe polymorphism.  Still you can get around this in 8.4 using sort polymorphism, and defining [Category : Type -> Type] to be the category on a given type of objects, and then you can define [Cat : Category { Ob : Type & Category Ob }].  This category doesn't have a Cat inside of it (unless you make another one), but this doesn't matter until you want to make Pi and want the slice over category (Cat / Cat).

-Jason

On Jan 15, 2014 3:49 AM, "AUGER Cédric" <sedrikov AT gmail.com> wrote:

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]).