Localizations at subuniverses

Content created by Fredrik Bakke.

Created on 2024-11-19.
Last modified on 2025-11-12.

module orthogonal-factorization-systems.localizations-at-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.equivalences-at-subuniverses
open import orthogonal-factorization-systems.types-local-at-maps

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 P-equivalence η : X → Y, i.e., a map such that for every Z in P the precomposition map

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

is an equivalence. In other words, every type in P is η-local.

Definition

The predicate on a map of being a localization at a subuniverse

is-subuniverse-localization-map :
  {l1 l2 lP : Level} (P : subuniverse l1 lP) {A : UU l2} {PA : UU l1}
  (η : A → PA) → UU (lsuc l1 ⊔ l2 ⊔ lP)
is-subuniverse-localization-map P {A} {PA} η =
  is-in-subuniverse P PA × is-subuniverse-equiv P η

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) × (subuniverse-equiv P X Y)

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 : type-subuniverse P) → is-local unit-is-subuniverse-localization (pr1 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)

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

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

  is-subuniverse-equiv-unit-subuniverse-localization :
    is-subuniverse-equiv P unit-subuniverse-localization
  is-subuniverse-equiv-unit-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