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:𝒰A:\mathcal{U} and B:𝒰B:\mathcal{U} be terms of the universe, and R:(𝒯 𝒰(A)×𝒯 𝒰(B))𝒰R : (\mathcal{T}_\mathcal{U}(A) \times \mathcal{T}_\mathcal{U}(B)) \to \mathcal{U} be a correspondence? between AA and BB. We define the property of RR being bijective as follows:

isBijective(R)( a:𝒯 𝒰(A)isContr( b:𝒯 𝒰(B)R(a,b)))×( b:𝒯 𝒰(B)isContr( a:𝒯 𝒰(A)R(a,b)))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 AA to BB in 𝒰\mathcal{U} as

(A 𝒰B) R:(𝒯 𝒰(A)×𝒯 𝒰(B))𝒰isBijective(R)(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

See also

References

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.