Homotopy Type Theory equivalence > history (Rev #4, changes)

Showing changes from revision #3 to #4: Added | ~~Removed~~ | ~~Chan~~ged

Idea

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

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

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 $A$ to $B$ as

(A ≃ B) \equiv \equiv_{𝒰} \sum_{R : (A \times B) \to 𝒰} isBijective (R)

(A \simeq B) ~~\equiv~~ \equiv_\mathcal{U} \sum_{R : (A \times B) \to \mathcal{U}} isBijective(R)

~~Examples~~

~~Every bijective relation is an equivalence.~~

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