## Idea ## ## Definition ## 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.** +--{.query} 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. =-- ## References ## [[HoTT book]] category: category theory