Showing changes from revision #1 to #2:
Added | Removed | Changed
A function is an equivalence if it has inverses whose composition with is homotopic to the corresponding identity map.
Let be types, and a function. We define the property of being an equivalence as follows:
We The define above the type of could equivalences also from be defined as to as
or, where phrased differently, the type of witnesses to and is thefiber being of equivalent types. over a term
We define the type of equivalences from to as
or, phrased differently, the type of witnesses to and being equivalent types.
Every equivalence is a -monic function.