# Contents

## Definition

### Localization at a function

Consider a function $f:S \to T$. We say that a type $X$ is $f$-local if the function

$\lambda g . g (f) : (S \to X) \to (T \to X)$

is an equivalence of types.

The localization of a type $X$ at $f$, $L_f(X)$, is the higher inductive type generated by

• the function $\mathrm{tolocal}:X \to L_f(X)$
• the function $\mathrm{localextend}: (S \to L_f(X)) \to (T \to L_f(X))$
• the dependent function
$\mathrm{localextension}:\prod_{h:S \to L_f(X)} \prod_{s:S} \mathrm{localextend}(h)(f(s)) = h(s)$
• the dependent function
$\mathrm{localunextension}:\prod_{g:T \to L_f(X)} \prod_{t:T} \mathrm{localextend}(g \circ f)(t) = g(t)$
• the dependent function
$\mathrm{localtriangle}:\prod_{g:T \to L_f(X)} \prod_{s:S} \mathrm{localunextension}(g)(f(s)) = \mathrm{localextension}(g \circ f)(s)$

### Localization at a type

The localization $L_S(X)$ of a type $X$ at a type $S$ is the localization $L_{u_S^\mathbb{1}}$ of $X$ at the unique function $u_S^\mathbb{1}:S \to \mathbb{1}$ from $S$ to the unit type $\mathbb{1}$, or equivalently, is the type $L_S(X)$ for which the canonical function $\mathrm{const}:L_S(X) \to (S \to L_S(X))$ is an equivalence of types.

### Localization at a family of functions

Consider a family $f:\prod_{(i:I)} S(i) \to T(i)$ of functions. We say that a type $X$ is $F$-local if the function

$\lambda g . g (f(i)) : (S(i) \to X) \to (T(i) \to X)$

is an equivalence of types for all (i : I).

The following higher inductive type can be shown to be a reflection of all types into the local types, constructing the localization of the category of types at the given family of functions.

Inductive localize X :=
| to_local : X -> localize X
| local_extend : forall (i:I) (h : S i -> localize X),
T i -> localize X
| local_extension : forall (i:I) (h : S i -> localize X) (s : S i),
local_extend i h (f i s) == h s
| local_unextension : forall (i:I) (g : T i -> localize X) (t : T i),
local_extend i (g o f i) t == g t
| local_triangle : forall (i:I) (g : T i -> localize X) (s : S i),
local_unextension i g (f i s) == local_extension i (g o f i) s.

The first constructor gives a function from X to localize X, while the other four specify exactly that localize X is local (by giving adjoint equivalence data to the function that we want to become an equivalence). See this blog post for details. This construction is also already interesting in extensional type theory.

### Localization at a family of types

The localization $L_F(X)$ of a type $X$ at a family of types $F:\prod_{i:I} S(i)$ is the family of localizations $L_F(-) \coloneqq \prod_{i:I} L_{u_{S(i)}^\mathbb{1}}(-)$ of $X$ at the family of unique functions $u_{S(i)}^\mathbb{1}:S(i) \to \mathbb{1}$ from $S(i)$ to the unit type $\mathbb{1}$, or equivalently, is the family of types $L_{S(i)}(X)$ for which each canonical function $\mathrm{const}:L_{S(i)}(X) \to (S(i) \to L_{S(i)}(X))$ is an equivalence of types.

## Examples

• The bracket type is the localization at the unique function $\mathbb{2} \to \mathbb{1}$ from the two-valued type to the unit type.

• More generally, the n-truncation modality is the localization at the unique function $S^{n + 1} \to \mathbb{1}$ from the $(n + 1)$-dimensional sphere type to the unit type.

• The shape modality which expresses real cohesion is the localization at the unique function $\mathbb{R} \to \mathbb{1}$ from the Dedekind real numbers to the unit type.

• The $n$-shape modality is the localization at the two unique functions $\mathbb{R} \to \mathbb{1}$ and $S^{n + 1} \to \mathbb{1}$.

• Let $\mathcal{R}$ be an Archimedean ordered Artinian local ring whose Archimedean subfield $\mathbb{R} \subseteq \mathcal{R}$ is the Dedekind real numbers, and let $\mathcal{D}$ be the type of all infinitesimals in $\mathcal{R}$. The infinitesimal shape modality is the localization at the unique function $\mathcal{D} \to \mathbb{1}$.