Localizations at subuniverses

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-06-28.

module orthogonal-factorization-systems.localizations-subuniverses where

Imports
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.subuniverses
open import foundation.universe-levels

open import orthogonal-factorization-systems.local-types


Idea

Let P be a subuniverse. Given a type X, its localization at P, or P-localization, is a type Y in P and a map η : X → Y such that every type in P is η-local. I.e. for every Z in P, the precomposition map

  _∘ η : (Y → Z) → (X → Z)


is an equivalence.

Definition

The predicate of being a localization at a subuniverse

is-subuniverse-localization :
{l1 l2 lP : Level} (P : subuniverse l1 lP) →
UU l2 → UU l1 → UU (lsuc l1 ⊔ l2 ⊔ lP)
is-subuniverse-localization {l1} {l2} P X Y =
( is-in-subuniverse P Y) ×
( Σ ( X → Y)
( λ η → (Z : UU l1) → is-in-subuniverse P Z → is-local η Z))

module _
{l1 l2 lP : Level} (P : subuniverse l1 lP) {X : UU l2} {Y : UU l1}
(is-localization-Y : is-subuniverse-localization P X Y)
where

is-in-subuniverse-is-subuniverse-localization : is-in-subuniverse P Y
is-in-subuniverse-is-subuniverse-localization = pr1 is-localization-Y

unit-is-subuniverse-localization : X → Y
unit-is-subuniverse-localization = pr1 (pr2 is-localization-Y)

is-local-at-unit-is-in-subuniverse-is-subuniverse-localization :
(Z : UU l1) → is-in-subuniverse P Z →
is-local unit-is-subuniverse-localization Z
is-local-at-unit-is-in-subuniverse-is-subuniverse-localization =
pr2 (pr2 is-localization-Y)


The type of localizations at a subuniverse

subuniverse-localization :
{l1 l2 lP : Level} (P : subuniverse l1 lP) → UU l2 → UU (lsuc l1 ⊔ l2 ⊔ lP)
subuniverse-localization {l1} P X = Σ (UU l1) (is-subuniverse-localization P X)

module _
{l1 l2 lP : Level} (P : subuniverse l1 lP)
{X : UU l2} (L : subuniverse-localization P X)
where

type-subuniverse-localization : UU l1
type-subuniverse-localization = pr1 L

is-subuniverse-localization-subuniverse-localization :
is-subuniverse-localization P X type-subuniverse-localization
is-subuniverse-localization-subuniverse-localization = pr2 L

is-in-subuniverse-subuniverse-localization :
is-in-subuniverse P type-subuniverse-localization
is-in-subuniverse-subuniverse-localization =
is-in-subuniverse-is-subuniverse-localization P
( is-subuniverse-localization-subuniverse-localization)

unit-subuniverse-localization : X → type-subuniverse-localization
unit-subuniverse-localization =
unit-is-subuniverse-localization P
( is-subuniverse-localization-subuniverse-localization)

is-local-at-unit-is-in-subuniverse-subuniverse-localization :
(Z : UU l1) →
is-in-subuniverse P Z → is-local unit-subuniverse-localization Z
is-local-at-unit-is-in-subuniverse-subuniverse-localization =
is-local-at-unit-is-in-subuniverse-is-subuniverse-localization P
( is-subuniverse-localization-subuniverse-localization)


Properties

There is at most one P-localization

This is Proposition 5.1.2 in Classifying Types, and remains to be formalized.