# Homotopy Type Theory equivalence of precategories (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Homepage

category: people

## 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.

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

Revision on September 14, 2018 at 11:52:31 by Ali Caglayan. See the history of this page for a list of all contributions to it.