Homotopy Type Theory
equivalence > history (Rev #2)
Idea
A function is an equivalence if it has inverses whose composition with is homotopic to the corresponding identity map.
Definition
Let be types, and a function. We define the property of being an equivalence as follows:
The above type could also be defined as
where is the fiber of over a term
We define the type of equivalences from to as
or, phrased differently, the type of witnesses to and being equivalent types.
Properties
Every equivalence is a -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.