Homotopy Type Theory
equivalence > history (Rev #5, changes)
Showing changes from revision #4 to #5:
Added | Removed | Changed
Idea
There are multiple definitions of equivalence that are valid in homotopy type theory
Definition
Bijective correspondences
Let A 𝒰 , B A,B \mathcal{U} be types, a and R : ( A × B ) → 𝒰 R : (A \times B) \to \mathcal{U} universe be and a 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? . We between define the property of R A R A and B B . We define the property of R R 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:A} \left(\prod_{a:\mathcal{T}_\mathcal{U}(A)} \mathrm{isContr}\left(\sum_{b:B} \mathrm{isContr}\left(\sum_{b:\mathcal{T}_\mathcal{U}(B)} R(a,b)\right)\right) \times \left(\prod_{b:B} \left(\prod_{b:\mathcal{T}_\mathcal{U}(B)} \mathrm{isContr}\left(\sum_{a:A} \mathrm{isContr}\left(\sum_{a:\mathcal{T}_\mathcal{U}(A)} R(a,b)\right)\right) We define the type of equivalences from A A B B in 𝒰 \mathcal{U}
( A ≃ ≃ 𝒰 B ) ≡ 𝒰 ≡ ∑ R : ( 𝒯 𝒰 ( A ) × 𝒯 𝒰 ( B ) ) → 𝒰 isBijective ( R ) (A \simeq \simeq_\mathcal{U} B) \equiv_\mathcal{U} \equiv \sum_{R : (A (\mathcal{T}_\mathcal{U}(A) \times B) \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 18:49:34 by
Anonymous? .
See the history of this page for a list of all contributions to it.