Homotopy Type Theory equivalence > history (Rev #3)

Idea

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

Definition

Bijective correspondences

Let A,BA,B be types, and R:(A×B)𝒰R : (A \times B) \to \mathcal{U} be a correspondence?. We define the property of RR being bijective as follows:

isBijective(R)( a:AisContr( b:BR(a,b)))×( b:BisContr( a:AR(a,b)))isBijective(R) \coloneqq \left(\prod_{a:A} \mathrm{isContr}\left(\sum_{b:B} R(a,b)\right)\right) \times \left(\prod_{b:B} \mathrm{isContr}\left(\sum_{a:A} R(a,b)\right)\right)

We define the type of equivalences from AA to BB as

(AB) R:(A×B)𝒰isBijective(R)(A \simeq B) \equiv \sum_{R : (A \times B) \to \mathcal{U}} isBijective(R)

Contractible fibers

Bi-invertible maps

Quasi-inverses

Half adjoint equivalences

Examples

  • Every bijective relation is an equivalence.

See also

References

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