natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
On localization in homotopy type theory.
Consider a function $f:S \to T$. We say that a type $X$ is $f$-local if the function
is an equivalence of types.
The localization of a type $X$ at $f$, $L_f(X)$, is the higher inductive type generated by
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.
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
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.
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.
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}$.
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
Egbert Rijke, Michael Shulman, Bas Spitters, Modalities in homotopy type theory (arXiv:1706.07526)
Daniel Christensen, Morgan Opie, Egbert Rijke, Luis Scoccola, Localization in Homotopy Type Theory (arXiv:1807.04155)
David Jaz Myers, Orbifolds as microlinear types in synthetic differential cohesive homotopy type theory (arXiv:2205.15887)
Last revised on November 24, 2023 at 06:39:19. See the history of this page for a list of all contributions to it.