[[!redirects homotopy equivalence]] [[!redirects bijective correspondence]] [[!redirects bijective correspondences]] ## Idea ## There are multiple definitions of equivalence that are valid in [[homotopy type theory]] ## Definition ## ### Bijective correspondences ### 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 \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 ## * [[type theory]] * [[univalence]] ## References ## * [[HoTT book]]