LOCALIZATION

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