Homotopy Type Theory
localization (changes)

Showing changes from revision #6 to #7: Added | ~~Removed~~ | ~~Chan~~ged

Idea

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

Definition

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

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

\lambda g . g ~~\circ~~ (F(a)) ~~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

Modalities in homotopy type theory
Localization in Homotopy Type Theory
HoTT book

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.

Homotopy Type Theory localization (changes)

Idea

Definition

Properties

References

Homotopy Type Theory
localization (changes)