9.4 Equivalences

It is usual in category theoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath to define an equivalence of categories to be a functorMathworldPlanetmath F:AB such that there exists a functor G:BA and natural isomorphisms FG1B and GF1A. 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.

Definition 9.4.1.

A functor F:AB is an equivalence of (pre)categoriesMathworldPlanetmath if it is a left adjoint for which η and ϵ are isomorphismsMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath. We write AB for the type of equivalences of categories from A to B.

By \autorefct:adjprop,\autorefct:isoprop, if A is a category, then the type “F is an equivalence of precategories” is a mere proposition.

Lemma 9.4.2.

If for F:AB there exists G:BA and isomorphisms GF1A and FG1B, then F is an equivalence of precategories.


Just like the proof of \autorefthm:equiv-iso-adj for equivalences of types. ∎

Definition 9.4.3.

We say a functor F:AB is faithfulPlanetmathPlanetmath if for all a,b:A, the function


is injectivePlanetmathPlanetmath, and full if for all a,b:A this function is surjectivePlanetmathPlanetmath. If it is both (hence each Fa,b is an equivalence) we say F is fully faithful.

Definition 9.4.4.

We say a functor F:AB is split essentially surjective if for all b:B there exists an a:A such that Fab.

Lemma 9.4.5.

For any precategories A and B and functor F:AB, the following types are equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath.

  1. 1.

    F is an equivalence of precategories.

  2. 2.

    F is fully faithful and split essentially surjective.


Suppose F is an equivalence of precategories, with G,η,ϵ specified. Then we have the function

homB(Fa,Fb) homA(a,b),
g ηb-1G(g)ηa.

For f:homA(a,b), we have


while for g:homB(Fa,Fb) we have

F(ηb-1G(g)ηa) =F(ηb-1)F(G(g))F(ηa)

using naturality of ϵ, and the triangle identities twice. Thus, Fa,b is an equivalence, so F is fully faithful. Finally, for any b:B, we have Gb:A and ϵb:FGbb.

On the other hand, suppose F is fully faithful and split essentially surjective. Define G0:B0A0 by sending b:B to the a:A given by the specified essential splitting, and write ϵb for the likewise specified isomorphism FGbb.

Now for any g:homB(b,b), define G(g):homA(Gb,Gb) to be the unique morphism such that F(G(g))=(ϵb)-1gϵb (which exists since F is fully faithful). Finally, for a:A define ηa:homA(a,GFa) to be the unique morphism such that Fηa=ϵFa-1. It is easy to verify that G is a functor and that (G,η,ϵ) exhibit F as an equivalence of precategories.

Now consider the composite 121. We clearly recover the same function G0:B0A0. For the action of G on hom-sets, we must show that for g:homB(b,b), G(g) is the (necessarily unique) morphism such that F(G(g))=(ϵb)-1gϵb. But this equation holds by the assumed naturality of ϵ. We also clearly recover ϵ, while η is uniquely characterized by Fηa=ϵFa-1 (which is one of the triangle identities assumed to hold in the structureMathworldPlanetmath of an equivalence of precategories). Thus, this composite is equal to the identityPlanetmathPlanetmath.

Finally, consider the other composite 212. Since being fully faithful is a mere proposition, it suffices to observe that we recover, for each b:B, the same a:A and isomorphism Fab. But this is clear, since we used this function and isomorphism to define G0 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 12. ∎

However, if B is not a category, then neither type in \autorefct:ffeso may necessarily be a mere proposition. This suggests considering as well the following notions.

Definition 9.4.6.

A functor F:AB is essentially surjective if for all b:B, there merely exists an a:A such that Fab. We say F is a weak equivalenceMathworldPlanetmath if it is fully faithful and essentially surjective.

Being a weak equivalence is always a mere proposition. For categories, however, there is no differencePlanetmathPlanetmath between equivalences and weak ones.

Lemma 9.4.7.

If F:AB is fully faithful and A is a category, then for any b:B the type (a:A)(Fab) is a mere proposition. Hence a functor between categories is an equivalence if and only if it is a weak equivalence.


Suppose given (a,f) and (a,f) in (a:A)(Fab). Then f-1f is an isomorphism FaFa. Since F is fully faithful, we have g:aa with Fg=f-1f. And since A is a category, we have p:a=a with 𝗂𝖽𝗍𝗈𝗂𝗌𝗈(p)=g. Now Fg=f-1f implies ((F0)(p))*(f)=f, hence (by the characterizationMathworldPlanetmath of equalities in dependent pair types) (a,f)=(a,f).

Thus, for fully faithful functorsMathworldPlanetmath 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 choiceMathworldPlanetmath 𝖠𝖢. 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.

Definition 9.4.8.

A functor F:AB is an isomorphism of (pre)categories if F is fully faithful and F0:A0B0 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 AB denote the type of isomorphisms of (pre)categories from A to B.

Lemma 9.4.9.

For precategories A and B and F:AB, the following are equivalent.

  1. 1.

    F is an isomorphism of precategories.

  2. 2.

    There exist G:BA and η:1A=GF and ϵ:FG=1B such that

    𝖺𝗉(λH.FH)(η)=𝖺𝗉(λK.KF)(ϵ-1). (9.4.9)
  3. 3.

    There merely exist G:BA and η:1A=GF and ϵ:FG=1B.

Note that if B0 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

(F0)(η0)a=(ϵ0)-1F0a. (9.4.11)

for all a:A0. Note that this is precisely the triangle identity for G0, η0, and ϵ0 to be a proof that F0 is a half adjoint equivalence of types.

Now suppose 1. Let G0:B0A0 be the inverseMathworldPlanetmathPlanetmathPlanetmathPlanetmath of F0, with η0:𝗂𝖽A0=G0F0 and ϵ0:F0G0=𝗂𝖽B0 satisfying the triangle identity, which is precisely (9.4.11). Now define Gb,b:homB(b,b)homA(G0b,G0b) by


(using the assumptionPlanetmathPlanetmath that F is fully faithful). Since 𝗂𝖽𝗍𝗈𝗂𝗌𝗈 takes inverses to inverses and concatenation to composition, and F is a functor, it follows that G is a functor.

By definition, we have (GF)0G0F0, which is equal to 𝗂𝖽A0 by η0. To obtain 1A=GF, we need to show that when transported along η0, the identity function of homA(a,a) becomes equal to the composite GFa,FaFa,a. In other words, for any f:homA(a,a) we must have


But this is equivalent to


which follows from functoriality of F, the fact that F preserves 𝗂𝖽𝗍𝗈𝗂𝗌𝗈, and (9.4.11). Thus we have η:1A=GF.

On the other side, we have (FG)0F0G0, which is equal to 𝗂𝖽B0 by ϵ0. To obtain FG=1B, we need to show that when transported along ϵ0, the identity function of homB(b,b) becomes equal to the composite FGb,GbGb,b. That is, for any g:homB(b,b) we must have


But this is just the fact that (FGb,Gb)-1 is the inverse of FGb,Gb. And we have remarked that (9.4.9) is equivalent to (9.4.11), so 2 holds.

Conversely, suppose given 2; then the object-parts of G, η, and ϵ together with (9.4.11) show that F0 is an equivalence of types. And for a,a:A0, we define G¯a,a:homB(Fa,Fa)homA(a,a) by

G¯a,a(g):𝗂𝖽𝗍𝗈𝗂𝗌𝗈(η-1)aG(g)𝗂𝖽𝗍𝗈𝗂𝗌𝗈(η)a. (9.4.12)

By naturality of 𝗂𝖽𝗍𝗈𝗂𝗌𝗈(η), for any f:homA(a,a) we have

G¯a,a(Fa,a(f)) =𝗂𝖽𝗍𝗈𝗂𝗌𝗈(η-1)aG(F(f))𝗂𝖽𝗍𝗈𝗂𝗌𝗈(η)a

On the other hand, for g:homB(Fa,Fa) we have

Fa,a(G¯a,a(g)) =F(𝗂𝖽𝗍𝗈𝗂𝗌𝗈(η-1)a)F(G(g))F(𝗂𝖽𝗍𝗈𝗂𝗌𝗈(η)a)

(There are lemmas needed here regarding the compatibility of 𝗂𝖽𝗍𝗈𝗂𝗌𝗈 and whiskering, which we leave it to the reader to state and prove.) Thus, Fa,a is an equivalence, so F 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 G0, η0, ϵ0, 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 G on hom-sets. In other words, we must show that if g:homB(b,b), then


where G¯ is defined by (9.4.12). However, this follows from functoriality of G and the other triangle identity, which we have seen in \autorefcha:equivalences is equivalent to (9.4.11).

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 G, η, and ϵ. Then G0 along with η and ϵ imply that F0 is an equivalence. Moreover, we also have natural isomorphisms 𝗂𝖽𝗍𝗈𝗂𝗌𝗈(η):1AGF and 𝗂𝖽𝗍𝗈𝗂𝗌𝗈(ϵ):FG1B, so by \autorefct:adjointification, F is an equivalence of precategories, and in particular fully faithful. ∎

From \autorefct:isoprecat2 and 𝗂𝖽𝗍𝗈𝗂𝗌𝗈 in functor categoriesPlanetmathPlanetmath, we conclude immediately that any isomorphism of precategories is an equivalence. For precategories, the converse can fail.

Example 9.4.13.

Let X be a type and x0:X an element, and let Xch denote the chaotic or indiscrete precategory on X. By definition, we have (Xch)0:X, and homXch(x,x):1 for all x,x. Then the unique functor Xch1 is an equivalence of precategories, but not an isomorphism unless X is contractibleMathworldPlanetmath.

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.

Lemma 9.4.14.

For categories A and B, a functor F:AB 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 F is an equivalence of categories, with (G,η,ϵ) given. We have already seen that F is fully faithful. By \autorefct:functor-cat, the natural isomorphisms η and ϵ yield identities 1A=GF and FG=1B, hence in particular identities 𝗂𝖽A=G0F0 and F0G0=𝗂𝖽B. Thus, F0 is an equivalence of types.

Conversely, suppose F is fully faithful and F0 is an equivalence of types, with inverse G0, say. Then for each b:B we have G0b:A and an identity FGb=b, hence an isomorphism FGbb. Thus, by \autorefct:ffeso, F 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.

Lemma 9.4.15.

If A and B are precategories, then the function


(defined by inductionMathworldPlanetmath from the identity functor) is an equivalence of types.


As usual for dependent sum types, to give an element of A=B is equivalent to giving

  • an identity P0:A0=B0,

  • for each a,b:A0, an identity

  • identities (Pa,a)*(1a)=1P0*(a) and (Pa,c)*(gf)=(Pb,c)*(g)(Pa,b)*(f).

(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 F0:A0B0,

  • for each a,b:A0, an equivalence of types

  • and identities Fa,a(1a)=1F0(a) and Fa,c(gf)=Fb,c(g)Fa,b(f).

But this consists exactly of a functor F:AB that is an isomorphism of categories. And by induction on identity, this equivalence (A=B)(AB) 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.

Theorem 9.4.16.

If A and B 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 AB is a subtype of the type of functors from A to B, which are the objects of a category, it is a 1-type; hence the identity types A=B are also 1-types.

Title 9.4 Equivalences