[[!redirects Localization]] [[!redirects localisation]] ## Idea ## Localization is the process of inverting a specified class of maps. ## Definition ## Consider a [[type family|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)$$ is an [[equivalence]]. ## Properties ## ## References ## * [[Modalities in homotopy type theory]] * [[Localization in Homotopy Type Theory]] * [[HoTT book]] category: homotopy theory