Homotopy Type Theory
equivalence > history (Rev #1)
Redirected from "CMon-enriched symmetric monoidal categories".
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:
We define the type of equivalences from to as
or, phrased differently, the type of witnesses to and being equivalent types.
Properties
See also
References
Revision on October 10, 2018 at 23:34:59 by
Ali Caglayan.
See the history of this page for a list of all contributions to it.