LOCALIZATION MODALITY

Formation

(Localization Modality). Given a family of maps a type is -local if the precomposition map is an equivalence for all , and the -localization is the universal -local type admitting a map from .

Introduction

(Localization Modality Constructors). The localization modality is generated by the following higher inductive composition structure:

data Localize (A X: U) (S T: A -> U) (F : (x:A) -> S x -> T x)
   = center (x: X)
   | ext (a: A) (f: S a -> Localize A X S T F) (t: T a)
   | isExt (a: A) (f: S a -> Localize A X S T F) (s: S a) <i>
     [ (i=0) -> ext a f (F a s) , (i=>1) -> f s ]
   | extEq (a: A) (g h: T a -> Localize A X S T F)
     (p: (s : S a) -> Path (Localize A X S T F) (g (F a s)) (h (F a s)))
     (t : T a) <i> [ (i=0) -> g t , (i=>1) -> h t ]
   | isExtEq (a: A) (g h : T a -> Localize A X S T F)
     (p: (s : S a) -> Path (Localize A X S T F) (g (F a s)) (h (F a s)))
     (s : S a) <i> [ (i=0) -> extEq {Localize A X S T F} a g h p (F a s) @ i,
                        (i=>1) -> p s @ i]

(Accessible Modality). Accessible modality is a modality than can be generated by localization. Examples: -truncations, nullification, open, closed.

Elimination

(Localization Induction Principle). For any with :

there is a section such that .

LocalizationInd (A X : U) (S T : A -> U) (F : (x:A) -> S x -> T x)
     (P : Localize A X S T F -> U)
     (n : (x : X) -> P (center x))
     (r : (a : A) (f: S a -> Localize A X S T F)
          (g: (b: S a) -> P (f b))
          (t: T a) -> P (ext a f t))
     (s : (a : A) (f: S a -> Localize A X S T F)
          (g: (b: S a) -> P (f b))
          (b: S a) -> PathP (<i> P (isExt {Localize A X S T F} a f b @ i))
                            (r a f g (F a b)) (g b))
   : (x : Localize A X S T F) -> P x

Recursor

isLocal (A X: U) (S T: A -> U) (F : (x:A) -> S x -> T x) : U = undefined
LocalizationRec (A X: U) (S T: A -> U) (F : (x:A) -> S x -> T x)
     (Y : U)
     (locality : isLocal A Y S T F)
     (f: X -> Y)
   : Localize A X S T F -> Y

LITERATURE

[1].J.Daniel Christensen, M.Opie, E.Rijke, L.Scoccola. Localization in Homotopy Type Theory.
[2]. E.Rijke, M.Shulman, B.Spitters. Modalities in Homotopy Type Theory.
[3]. M.Riley,E.Finster,D.R.Licata. Synthetic Spectra via a Monadic and Comonadic Modality.