localization (Rev #7, changes)

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

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

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

$$\lambda 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?

category: homotopy theory

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