Reflective subuniverses

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2023-03-09.
Last modified on 2023-11-24.

module orthogonal-factorization-systems.reflective-subuniverses where
Imports
open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.retractions
open import foundation.subuniverses
open import foundation.universe-levels

open import orthogonal-factorization-systems.local-types
open import orthogonal-factorization-systems.localizations-subuniverses
open import orthogonal-factorization-systems.modal-induction
open import orthogonal-factorization-systems.modal-operators
open import orthogonal-factorization-systems.modal-subuniverse-induction

Idea

A reflective subuniverse is a subuniverse P together with a reflecting operator ○ : UU → UU that take values in P, and a modal unit A → ○ A for all small types A, with the property that the types in P are local at the modal unit for every A. Hence the modal types with respect to are precisely the types in the reflective subuniverse.

Definitions

The predicate on subuniverses of being reflective

is-reflective-subuniverse :
  {l1 l2 : Level} (P : UU l1  Prop l2)  UU (lsuc l1  l2)
is-reflective-subuniverse {l1} P =
  Σ ( operator-modality l1 l1)
    ( λ  
      Σ ( unit-modality )
        ( λ unit-○ 
          ( (X : UU l1)  is-in-subuniverse P ( X)) ×
          ( (X Y : UU l1)  is-in-subuniverse P X  is-local (unit-○ {Y}) X)))
module _
  {l1 l2 : Level} (P : subuniverse l1 l2)
  (is-reflective-P : is-reflective-subuniverse P)
  where

  operator-is-reflective-subuniverse : operator-modality l1 l1
  operator-is-reflective-subuniverse = pr1 is-reflective-P

  unit-is-reflective-subuniverse :
    unit-modality (operator-is-reflective-subuniverse)
  unit-is-reflective-subuniverse = pr1 (pr2 is-reflective-P)

  is-in-subuniverse-operator-type-is-reflective-subuniverse :
    (X : UU l1) 
    is-in-subuniverse P (operator-is-reflective-subuniverse X)
  is-in-subuniverse-operator-type-is-reflective-subuniverse =
    pr1 (pr2 (pr2 is-reflective-P))

  is-local-is-in-subuniverse-is-reflective-subuniverse :
    (X Y : UU l1) 
    is-in-subuniverse P X 
    is-local (unit-is-reflective-subuniverse {Y}) X
  is-local-is-in-subuniverse-is-reflective-subuniverse =
    pr2 (pr2 (pr2 is-reflective-P))

The type of reflective subuniverses

reflective-subuniverse : (l1 l2 : Level)  UU (lsuc l1  lsuc l2)
reflective-subuniverse l1 l2 =
  Σ (UU l1  Prop l2) (is-reflective-subuniverse)
module _
  {l1 l2 : Level} (P : reflective-subuniverse l1 l2)
  where

  subuniverse-reflective-subuniverse : subuniverse l1 l2
  subuniverse-reflective-subuniverse = pr1 P

  is-in-reflective-subuniverse : UU l1  UU l2
  is-in-reflective-subuniverse =
    is-in-subuniverse subuniverse-reflective-subuniverse

  inclusion-reflective-subuniverse :
    type-subuniverse (subuniverse-reflective-subuniverse)  UU l1
  inclusion-reflective-subuniverse =
    inclusion-subuniverse subuniverse-reflective-subuniverse

  is-reflective-subuniverse-reflective-subuniverse :
    is-reflective-subuniverse (subuniverse-reflective-subuniverse)
  is-reflective-subuniverse-reflective-subuniverse = pr2 P

  operator-reflective-subuniverse : operator-modality l1 l1
  operator-reflective-subuniverse =
    operator-is-reflective-subuniverse
      ( subuniverse-reflective-subuniverse)
      ( is-reflective-subuniverse-reflective-subuniverse)

  unit-reflective-subuniverse :
    unit-modality (operator-reflective-subuniverse)
  unit-reflective-subuniverse =
    unit-is-reflective-subuniverse
      ( subuniverse-reflective-subuniverse)
      ( is-reflective-subuniverse-reflective-subuniverse)

  is-in-subuniverse-operator-type-reflective-subuniverse :
    ( X : UU l1) 
    is-in-subuniverse
      ( subuniverse-reflective-subuniverse)
      ( operator-reflective-subuniverse X)
  is-in-subuniverse-operator-type-reflective-subuniverse =
    is-in-subuniverse-operator-type-is-reflective-subuniverse
      ( subuniverse-reflective-subuniverse)
      ( is-reflective-subuniverse-reflective-subuniverse)

  is-local-is-in-subuniverse-reflective-subuniverse :
    ( X Y : UU l1) 
    is-in-subuniverse subuniverse-reflective-subuniverse X 
    is-local (unit-reflective-subuniverse {Y}) X
  is-local-is-in-subuniverse-reflective-subuniverse =
    is-local-is-in-subuniverse-is-reflective-subuniverse
      ( subuniverse-reflective-subuniverse)
      ( is-reflective-subuniverse-reflective-subuniverse)

Properties

Reflective subuniverses are subuniverses that have all localizations

module _
  {l1 l2 : Level} (P : subuniverse l1 l2)
  (is-reflective-P : is-reflective-subuniverse P)
  where

  has-all-localizations-is-reflective-subuniverse :
    (A : UU l1)  subuniverse-localization P A
  pr1 (has-all-localizations-is-reflective-subuniverse A) =
    operator-is-reflective-subuniverse P is-reflective-P A
  pr1 (pr2 (has-all-localizations-is-reflective-subuniverse A)) =
    is-in-subuniverse-operator-type-is-reflective-subuniverse
      P is-reflective-P A
  pr1 (pr2 (pr2 (has-all-localizations-is-reflective-subuniverse A))) =
    unit-is-reflective-subuniverse P is-reflective-P
  pr2 (pr2 (pr2 (has-all-localizations-is-reflective-subuniverse A)))
    X is-in-subuniverse-X =
      is-local-is-in-subuniverse-is-reflective-subuniverse
        P is-reflective-P X A is-in-subuniverse-X

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

  is-reflective-has-all-localizations-subuniverse :
    is-reflective-subuniverse P
  pr1 is-reflective-has-all-localizations-subuniverse A =
    type-subuniverse-localization P (L A)
  pr1 (pr2 is-reflective-has-all-localizations-subuniverse) {A} =
    unit-subuniverse-localization P (L A)
  pr1 (pr2 (pr2 is-reflective-has-all-localizations-subuniverse)) A =
    is-in-subuniverse-subuniverse-localization P (L A)
  pr2 (pr2 (pr2 is-reflective-has-all-localizations-subuniverse))
    A B is-in-subuniverse-A =
      is-local-at-unit-is-in-subuniverse-subuniverse-localization
        P (L B) A is-in-subuniverse-A

Recursion for reflective subuniverses

module _
  {l1 l2 : Level} (P : subuniverse l1 l2)
  (is-reflective-P : is-reflective-subuniverse P)
  where

  rec-modality-is-reflective-subuniverse :
    rec-modality (unit-is-reflective-subuniverse P is-reflective-P)
  rec-modality-is-reflective-subuniverse {X} {Y} =
    map-inv-is-equiv
      ( is-local-is-in-subuniverse-is-reflective-subuniverse
        ( P)
        ( is-reflective-P)
        ( operator-is-reflective-subuniverse P is-reflective-P Y)
        ( X)
        ( is-in-subuniverse-operator-type-is-reflective-subuniverse
          ( P)
          ( is-reflective-P)
          ( Y)))

  map-is-reflective-subuniverse :
    {X Y : UU l1}  (X  Y) 
    operator-is-reflective-subuniverse P is-reflective-P X 
    operator-is-reflective-subuniverse P is-reflective-P Y
  map-is-reflective-subuniverse =
    ap-map-rec-modality
      ( unit-is-reflective-subuniverse P is-reflective-P)
      ( rec-modality-is-reflective-subuniverse)

  strong-rec-subuniverse-is-reflective-subuniverse :
    strong-rec-subuniverse-modality
      ( unit-is-reflective-subuniverse P is-reflective-P)
  strong-rec-subuniverse-is-reflective-subuniverse =
    strong-rec-subuniverse-rec-modality
      ( unit-is-reflective-subuniverse P is-reflective-P)
      ( rec-modality-is-reflective-subuniverse)

  rec-subuniverse-is-reflective-subuniverse :
    rec-subuniverse-modality (unit-is-reflective-subuniverse P is-reflective-P)
  rec-subuniverse-is-reflective-subuniverse =
    rec-subuniverse-rec-modality
      ( unit-is-reflective-subuniverse P is-reflective-P)
      ( rec-modality-is-reflective-subuniverse)

See also

References

  1. Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013) (website, arXiv:1308.0729)
  2. 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)
  3. Egbert Rijke, Classifying Types (arXiv:1906.09435)

Recent changes