[[!redirects homotopy equivalence]] [[!redirects equivalences]] [[!redirects bijective correspondence]] [[!redirects bijective correspondences]] ## Idea ## There are multiple definitions of equivalence that are valid in [[homotopy type theory]] ## Definition ## ### Bijective correspondences ### Let $\mathcal{U}$ be a [[universe]] and $A:\mathcal{U}$ and $B:\mathcal{U}$ be terms of the universe, and $R : (\mathcal{T}_\mathcal{U}(A) \times \mathcal{T}_\mathcal{U}(B)) \to \mathcal{U}$ be a [[correspondence]] between $A$ and $B$. We define the property of $R$ being **bijective** as follows: $$isBijective(R) \coloneqq \left(\prod_{a:\mathcal{T}_\mathcal{U}(A)} \mathrm{isContr}\left(\sum_{b:\mathcal{T}_\mathcal{U}(B)} R(a,b)\right)\right) \times \left(\prod_{b:\mathcal{T}_\mathcal{U}(B)} \mathrm{isContr}\left(\sum_{a:\mathcal{T}_\mathcal{U}(A)} R(a,b)\right)\right)$$ We define the type of equivalences from $A$ to $B$ in $\mathcal{U}$ as $$(A \simeq_\mathcal{U} B) \equiv \sum_{R : (\mathcal{T}_\mathcal{U}(A) \times \mathcal{T}_\mathcal{U}(B)) \to \mathcal{U}} isBijective(R)$$ ### Contractible fibers ### ### Bi-invertible maps ### ### Quasi-inverses ### ### Half adjoint equivalences ### ## See also ## * [[type theory]] * [[univalence]] ## References ## * [[HoTT book]]