Homotopy Type Theory equivalence > history (Rev #7)

Idea

There are multiple definitions of equivalence that are valid in homotopy type theory

Definition

Bijective correspondences

Let $\mathcal{U}$ be a universe and $A:\mathcal{U}$ and $B:\mathcal{U}$ be terms of the universe, and $R : (\mathcal{T}_\mathcal{U}(A) \times \mathcal{T}_\mathcal{U}(B)) \to \mathcal{U}$ be a correspondence? between $A$ and $B$. We define the property of $R$ being bijective as follows:

We define the type of equivalences from $A$ to $B$ in $\mathcal{U}$ as

Contractible fibers

Bi-invertible maps

Quasi-inverses

Half adjoint equivalences

See also

• type theory
• univalence

References

• HoTT book