Homotopy Type Theory localization > history (Rev #6)

Idea

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

Consider a family $\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)

Revision on October 10, 2018 at 23:21:02 by Ali Caglayan. See the history of this page for a list of all contributions to it.