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

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

Idea

A There ~~function~~ are multiple definitions of equivalence that are valid in ~~$f : A \to B$~~ homotopy type theory ~~is an equivalence if it has inverses whose composition with~~ ~~$f$~~ is ~~homotopic~~ ~~to the corresponding identity map.~~

Definition

~~Let $A,B$ be types, and $f : A \to B$ a function. We define the property of $f$ being an equivalence as follows:~~

Bijective correspondences

~~$isequiv(f) \equiv \left( \sum_{g : B \to A} f \circ g \sim id_B \right) \times \left( \sum_{h : B \to A} h \circ f \sim id_A \right)$~~

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:

~~The above type could also be defined as~~

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)

~~$isequiv(f) \equiv \prod_{b:B} isContr(fiber(f))$~~

We define the type of equivalences from $A$ to $B$ as

~~where $fiber(f, b)$ is the fiber of $f$ over a term $b:B$~~

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

~~We define the type of equivalences from $A$ to $B$ as~~

Contractible fibers

~~$(A \simeq B) \equiv \sum_{f : A \to B} isequiv(f)$~~

Bi-invertible maps

~~or, phrased differently, the type of witnesses to $A$ and $B$ being equivalent types.~~

Quasi-inverses

~~Properties~~

Half adjoint equivalences

~~Every equivalence is a $0$ -monic function.~~

Examples

Every bijective relation is an equivalence.

References

HoTT book

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.