[[!redirects homotopy equivalence]] ## Idea ## A function $f : A \to B$ is an equivalence if it has inverses whose composition with $f$ is [[homotopic]] to the corresponding identity map. ## Definition ## Let $A,B$ be types, and $f : A \to B$ a function. We define the property of $f$ being an **equivalence** as follows: $$isequiv(f) \equiv \left( \sum_{g : B \to A} f \circ g \sim id_B \right) \times \left( \sum_{h : B \to A} h \circ f \sim id_A \right)$$ The above type could also be defined as $$isequiv(f) \equiv \prod_{b:B} isContr(fiber(f))$$ where $fiber(f, b)$ is the [[fiber]] of $f$ over a term $b:B$ We define the type of equivalences from $A$ to $B$ as $$(A \simeq B) \equiv \sum_{f : A \to B} isequiv(f)$$ or, phrased differently, the type of witnesses to $A$ and $B$ being equivalent types. ## Properties ## Every equivalence is a $0$-[[monic function]]. ## See also ## * [[type theory]] * [[univalence]] ## References ## * [[HoTT book]]