Localizations at subuniverses

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-06-28.
Last modified on 2024-03-12.

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.

See also

References

[Rij19]
Egbert Rijke. Classifying Types. PhD thesis, Carnegie Mellon University, 06 2019. arXiv:1906.09435.
[RSS20]
Egbert Rijke, Michael Shulman, and Bas Spitters. Modalities in homotopy type theory. Logical Methods in Computer Science, 01 2020. URL: https://lmcs.episciences.org/6015, arXiv:1706.07526, doi:10.23638/LMCS-16(1:2)2020.

Recent changes