Homotopy Type Theory equivalence > history (Rev #2)

Idea

A function f:ABf : A \to B is an equivalence if it has inverses whose composition with ff is homotopic to the corresponding identity map.

Definition

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

isequiv(f)( g:BAfgid B)×( h:BAhfid A)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)

The above type could also be defined as

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

where fiber(f,b)fiber(f, b) is the fiber of ff over a term b:Bb:B

We define the type of equivalences from AA to BB as

(AB) f:ABisequiv(f)(A \simeq B) \equiv \sum_{f : A \to B} isequiv(f)

or, phrased differently, the type of witnesses to AA and BB being equivalent types.

Properties

Every equivalence is a 00-monic function.

See also

References

Revision on March 12, 2022 at 19:36:21 by Anonymous?. See the history of this page for a list of all contributions to it.