#
Homotopy Type Theory

localization

## 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)$ of maps. We say that a type $X$ is **$F$-local** if the function

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