Homotopy Type Theory
localization > history (Rev #8, changes)
Showing changes from revision #7 to #8:
Added | Removed | Changed
Idea
Localization is the process of inverting a specified class of maps.
Definition
Consider a family of maps. We say that a type is -local if the function
is an equivalence for all (a : A).
TODO: Localisation as a HIT?
Properties
References
Revision on June 9, 2022 at 04:03:38 by
Anonymous?.
See the history of this page for a list of all contributions to it.