This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Reflective subuniverses

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 : subuniverse l1 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 =
  Σ (subuniverse l1 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)

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.
[UF13]: The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book/, arXiv:1308.0729.

agda-unimath