Homotopy Type Theory equivalence > history (Rev #1)

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)

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

See also

References

HoTT book

Revision on October 10, 2018 at 23:34:59 by Ali Caglayan. See the history of this page for a list of all contributions to it.