It is usual in category theory to define an equivalence of categories to be a functor such that there exists a functor and natural isomorphisms and . Unlike the property of being an adjunction, however, this would not be a mere proposition without truncating it, for the same reasons that the type of quasi-inverses is ill-behaved (see \autorefsec:quasi-inverses). And as in \autorefsec:hae, we can avoid this by using the usual notion of adjoint equivalence.
By \autorefct:adjprop,\autorefct:isoprop, if is a category, then the type “ is an equivalence of precategories” is a mere proposition.
If for there exists and isomorphisms and , then is an equivalence of precategories.
Just like the proof of \autorefthm:equiv-iso-adj for equivalences of types. ∎
We say a functor is split essentially surjective if for all there exists an such that .
For any precategories and and functor , the following types are equivalent.
is an equivalence of precategories.
is fully faithful and split essentially surjective.
Suppose is an equivalence of precategories, with specified. Then we have the function
For , we have
while for we have
using naturality of , and the triangle identities twice. Thus, is an equivalence, so is fully faithful. Finally, for any , we have and .
On the other hand, suppose is fully faithful and split essentially surjective. Define by sending to the given by the specified essential splitting, and write for the likewise specified isomorphism .
Now for any , define to be the unique morphism such that (which exists since is fully faithful). Finally, for define to be the unique morphism such that . It is easy to verify that is a functor and that exhibit as an equivalence of precategories.
Now consider the composite 121. We clearly recover the same function . For the action of on hom-sets, we must show that for , is the (necessarily unique) morphism such that . But this equation holds by the assumed naturality of . We also clearly recover , while is uniquely characterized by (which is one of the triangle identities assumed to hold in the structure of an equivalence of precategories). Thus, this composite is equal to the identity.
Finally, consider the other composite 212. Since being fully faithful is a mere proposition, it suffices to observe that we recover, for each , the same and isomorphism . But this is clear, since we used this function and isomorphism to define and in 1, which in turn are precisely what we used to recover 2 again. Thus, the composites in both directions are equal to identities, hence we have an equivalence . ∎
However, if is not a category, then neither type in \autorefct:ffeso may necessarily be a mere proposition. This suggests considering as well the following notions.
A functor is essentially surjective if for all , there merely exists an such that . We say is a weak equivalence if it is fully faithful and essentially surjective.
Being a weak equivalence is always a mere proposition. For categories, however, there is no difference between equivalences and weak ones.
If is fully faithful and is a category, then for any the type is a mere proposition. Hence a functor between categories is an equivalence if and only if it is a weak equivalence.
Suppose given and in . Then is an isomorphism . Since is fully faithful, we have with . And since is a category, we have with . Now implies , hence (by the characterization of equalities in dependent pair types) .
Thus, for fully faithful functors whose domain is a category, essential surjectivity is equivalent to split essential surjectivity, and so being a weak equivalence is equivalent to being an equivalence. ∎
This is an important advantage of our category theory over set-based approaches. With a purely set-based definition of category, the statement “every fully faithful and essentially surjective functor is an equivalence of categories” is equivalent to the axiom of choice . Here we have it for free, as a category-theoretic version of the principle of unique choice (\autorefsec:unique-choice). (In fact, this property characterizes categories among precategories; see \autorefsec:rezk.)
On the other hand, the following characterization of equivalences of categories is perhaps even more useful.
A functor is an isomorphism of (pre)categories if is fully faithful and is an equivalence of types.
This definition is an exception to our general rule (see \autorefsec:basics-equivalences) of only using the word “isomorphism” for sets and set-like objects. However, it does carry an appropriate connotation here, because for general precategories, isomorphism is stronger than equivalence.
Note that being an isomorphism of precategories is always a mere property. Let denote the type of isomorphisms of (pre)categories from to .
For precategories and and , the following are equivalent.
is an isomorphism of precategories.
There exist and and such that
There merely exist and and .
Note that if is not a 1-type, then (9.4.9) may not be a mere proposition.
First note that since hom-sets are sets, equalities between equalities of functors are uniquely determined by their object-parts. Thus, by function extensionality, (9.4.9) is equivalent to
for all . Note that this is precisely the triangle identity for , , and to be a proof that is a half adjoint equivalence of types.
By definition, we have , which is equal to by . To obtain , we need to show that when transported along , the identity function of becomes equal to the composite . In other words, for any we must have
But this is equivalent to
On the other side, we have , which is equal to by . To obtain , we need to show that when transported along , the identity function of becomes equal to the composite . That is, for any we must have
By naturality of , for any we have
On the other hand, for we have
(There are lemmas needed here regarding the compatibility of and whiskering, which we leave it to the reader to state and prove.) Thus, is an equivalence, so is fully faithful; i.e. 1 holds.
Now the composite 121 is equal to the identity since 1 is a mere proposition. On the other side, tracing through the above constructions we see that the composite 212 essentially preserves the object-parts , , , and the object-part of (9.4.9). And in the latter three cases, the object-part is all there is, since hom-sets are sets.
Thus, it suffices to show that we recover the action of on hom-sets. In other words, we must show that if , then
Now since 1 is a mere proposition, so is 2, so it suffices to show they are logically equivalent to 3. Of course, 23, so let us assume 3. Since 1 is a mere proposition, we may assume given , , and . Then along with and imply that is an equivalence. Moreover, we also have natural isomorphisms and , so by \autorefct:adjointification, is an equivalence of precategories, and in particular fully faithful. ∎
Let be a type and an element, and let denote the chaotic or indiscrete precategory on . By definition, we have , and for all . Then the unique functor is an equivalence of precategories, but not an isomorphism unless is contractible.
This example also shows that a precategory can be equivalent to a category without itself being a category. Of course, if a precategory is isomorphic to a category, then it must itself be a category.
However, for categories, the two notions coincide.
For categories and , a functor is an equivalence of categories if and only if it is an isomorphism of categories.
Since both are mere properties, it suffices to show they are logically equivalent. So first suppose is an equivalence of categories, with given. We have already seen that is fully faithful. By \autorefct:functor-cat, the natural isomorphisms and yield identities and , hence in particular identities and . Thus, is an equivalence of types.
Conversely, suppose is fully faithful and is an equivalence of types, with inverse , say. Then for each we have and an identity , hence an isomorphism . Thus, by \autorefct:ffeso, is an equivalence of categories. ∎
Of course, there is yet a third notion of sameness for (pre)categories: equality. However, the univalence axiom implies that it coincides with isomorphism.
As usual for dependent sum types, to give an element of is equivalent to giving
an identity ,
for each , an identity
(Again, we use the fact that the identity types of hom-sets are mere propositions.) However, by univalence, this is equivalent to giving
an equivalence of types ,
for each , an equivalence of types
and identities and .
But this consists exactly of a functor that is an isomorphism of categories. And by induction on identity, this equivalence is equal to the one obtained by induction. ∎
Thus, for categories, equality also coincides with equivalence. We can interpret this as saying that categories, functors, and natural transformations form, not just a pre-2-category, but a 2-category.
If and are categories, then the function
(defined by induction from the identity functor) is an equivalence of types.
By \autorefct:cat-eq-iso,\autorefct:eqv-levelwise. ∎
As a consequence, the type of categories is a 2-type. For since is a subtype of the type of functors from to , which are the objects of a category, it is a 1-type; hence the identity types are also 1-types.