nLab localization of a type at a family of functions

Idea

On localization in homotopy type theory.

Definition

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 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.

 See also

• higher inductive type

• localization

References

• 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)