Homotopy Type Theory
localization

Idea

Localization is the process of inverting a specified class of maps.

Definition

Consider a family F: (a:A)B(a)C(a)F:\prod_{(a:A)} B(a) \to C(a) of maps. We say that a type XX is FF-local if the function

λg.g(F(a)):(C(a)X)(B(a)X)\lambda g . g (F(a)) : (C(a) \to X) \to (B(a) \to X)

is an equivalence for all (a : A).

TODO: Localisation as a HIT?

Properties

References

category: homotopy theory

Last revised on January 19, 2019 at 13:30:40. See the history of this page for a list of all contributions to it.