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


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.


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)

  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)

  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)


There is at most one P-localization

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

See also


Egbert Rijke. Classifying Types. PhD thesis, Carnegie Mellon University, 06 2019. arXiv:1906.09435.
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