A functor$F : A \to B$ is an equivalence of precategories if it is a left adjoint for which $\eta$ and $\epsilon$ are isomorphisms?. We write $A \equiv B$ for the type of equivalences of precategories from $A$ to $B$.

Properties

Lemma 9.4.2

If for $F : A \to B$ there exists $G : B \to A$ and isomorphisms?$G F \cong 1_A$ and $F G \cong 1_B$, then $F$ is an equivalence of precategories.

Proof.

The proof from the HoTT book analogues the proof of Theorem 4.2.3 for equivalence of types. This has not been written up at time of writing.