Localizations at subuniverses

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-06-28.
Last modified on 2023-11-01.

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


  1. Egbert Rijke, Michael Shulman, Bas Spitters, Modalities in homotopy type theory, Logical Methods in Computer Science, Volume 16, Issue 1, 2020 (arXiv:1706.07526, DOI:10.23638/LMCS-16(1:2)2020)
  2. Egbert Rijke, Classifying Types (arXiv:1906.09435)

Recent changes