Homotopy Equivalence

Idea

Homotopy equivalence is a core concept of homotopy type theory and algebraic topology.

Definition

An equivalence between two types $A$ and $B$ is a function $f:A\to B$ paired with a proof that all of the fibers of $f$ are contractible.

$$\mathsf{isEquiv}(f):\equiv \prod _{y:B}\mathsf{isContr}({\mathsf{fib}}_f(y))$$

This type is a mere proposition.

Remarks

The Univalence Axiom gives us an equivalences between equivalences and paths.

See also

Quasi-Inverse