Homotopy Type Theory equivalence > history (Rev #6)

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:

isBijective(R) \coloneqq \left(\prod_{a:\mathcal{T}_\mathcal{U}(A)} \mathrm{isContr}\left(\sum_{b:\mathcal{T}_\mathcal{U}(B)} R(a,b)\right)\right) \times \left(\prod_{b:\mathcal{T}_\mathcal{U}(B)} \mathrm{isContr}\left(\sum_{a:\mathcal{T}_\mathcal{U}(A)} R(a,b)\right)\right)

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

(A \simeq_\mathcal{U} B) \equiv \sum_{R : (\mathcal{T}_\mathcal{U}(A) \times \mathcal{T}_\mathcal{U}(B)) \to \mathcal{U}} isBijective(R)

Contractible fibers

Bi-invertible maps

Quasi-inverses

Half adjoint equivalences

References

HoTT book

Revision on April 29, 2022 at 20:45:40 by Anonymous?. See the history of this page for a list of all contributions to it.