Showing changes from revision #2 to #3:
Added | Removed | Changed
Idea
A There function are multiple definitions of equivalence that are valid inhomotopy type theory 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:
Bijective correspondences
Let be types, and be a correspondence?. We define the property of being bijective as follows: