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 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 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.
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)
Last revised on June 9, 2022 at 02:40:23. See the history of this page for a list of all contributions to it.