9.1 Categories and precategories
In classical mathematics, there are many equivalent definitions of a category. In our case, since we have dependent types, it is natural to choose the arrows to be a type family indexed by the objects. This matches the way hom-types are always used in category theory: we never even consider comparing two arrows unless we know their domains and codomains agree. Furthermore, it seems clear that for a theory of 1-categories, the hom-types should all be sets. This leads us to the following definition.
The problem with the notion of precategory is that for objects , we have two possibly-different notions of “sameness”. On the one hand, we have the type . But on the other hand, there is the standard categorical notion of isomorphism.
A morphism is an isomorphism if there is a morphism such that and . We write for the type of such isomorphisms.
For any , the type “ is an isomorphism” is a mere proposition. Therefore, for any the type is a set.
Suppose given and and , and similarly , , and . We must show . But since all hom-sets are sets, their identity types are mere propositions, so it suffices to show . For this we have
using and . ∎
If , then we write for its inverse, which by \autorefct:isoprop is uniquely determined.
The only relationship between these two notions of sameness that we have in a precategory is the following.
Lemma 9.1.4 (idtoiso).
If is a precategory and , then
By induction on identity, we may assume and are the same. But then we have , which is clearly an isomorphism. ∎
Evidently, this situation is analogous to the issue that motivated us to introduce the univalence axiom. In fact, we have the following:
There is a precategory , whose type of objects is \set, and with . The identity morphisms are identity functions and the composition is function composition. For this precategory, \autorefct:idtoiso is equal to (the restriction to sets of) the map from \autorefsec:compute-universe.
Of course, to be more precise we should call this category , since its objects are only the small sets relative to a universe .
Thus, it is natural to make the following definition.
A category is a precategory such that for all , the function from \autorefct:idtoiso is an equivalence.
In particular, in a category, if , then .
We also note the following.
In a category, the type of objects is a 1-type.
It suffices to show that for any , the type is a set. But is equivalent to , which is a set. ∎
We write for the inverse of the map from \autorefct:idtoiso. The following relationship between the two is important.
For and and , we have
Similarly, we can show
and so on.
In a preorder, a witness is an isomorphism just when there exists some witness . Thus, is the mere proposition that and . Therefore, a preorder is a category just when (1) each type is a mere proposition, and (2) for any there exists a function . In other words, must be a set, and must be antisymmetric (if and , then ). We call this a (partial) order or a poset.
If is a category, then is a set if and only if for any , the type is a mere proposition. This is equivalent to saying that every isomorphism in is an identity; thus it is rather stronger than the classical notion of “skeletal” category. Categories of this sort are sometimes called gaunt [bsp12infncats]. There is not really any notion of “skeletality” for our categories, unless one considers \autorefct:category itself to be such.
For any type , there is a precategory with as its type of objects and with . The composition operation
is defined by induction on truncation from concatenation . We call this the fundamental pregroupoid of . (In fact, we have met it already in \autorefsec:van-kampen; see also \autorefex:rezk-vankampen.)
There is a precategory whose type of objects is and with , and composition defined by induction on truncation from ordinary composition . We call this the homotopy precategory of types.
Let be the following precategory:
Its objects are sets.
For a set , we have .
For and , their composite is defined by
Suppose is an isomorphism, with inverse . We observe the following.
If and , then , and hence . Similarly, if and , then .
For any , we have , hence . Thus, there merely exists a such that and .
In conclusion, if is an isomorphism, then for each there is exactly one such that , and dually. Thus, there is a function sending each to this , which is an equivalence; hence . With a little more work, we conclude that is a category.
We might now restrict ourselves to considering categories rather than precategories. Instead, we will develop many concepts for precategories as well as categories, in order to emphasize how much better-behaved categories are, as compared both to precategories and to ordinary categories in classical mathematics.
We will also see in \crefrangesec:strict-categoriessec:dagger-categories that in slightly more exotic contexts, there are uses for certain kinds of precategories other than categories, each of which “fixes” the equality of objects in different ways. This emphasizes the “pre”-ness of precategories: they are the raw material out of which multiple important categorical structures can be defined.
|Title||9.1 Categories and precategories|