Homotopy Type Theory equivalence > history (Rev #4)

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 \simeq B) \equiv_\mathcal{U} \sum_{R : (A \times B) \to \mathcal{U}} isBijective(R)

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.