Homotopy Type Theory
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:

We define the type of equivalences from $A$ to $B$ as

or, phrased differently, the type of witnesses to $A$ and $B$ being equivalent types.

Properties

See also

• type theory
• univalence

References

• HoTT book