Global subuniverses

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-11-24.
Last modified on 2024-01-27.

module foundation.global-subuniverses where

Imports

open import foundation.dependent-pair-types
open import foundation.iterated-dependent-product-types
open import foundation.subuniverses
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.identity-types
open import foundation-core.propositions

Idea

Global subuniverses are subtypes of the large universe that are defined at every level, and are closed under equivalences of types. This does not follow from univalence, as equivalence induction only holds for homogeneous equivalences, i.e. equivalences in a single universe.

Definitions

The predicate on families of subuniverses of being closed under equivalences

module _
  (α : Level → Level) (P : (l : Level) → subuniverse l (α l))
  (l1 l2 : Level)
  where

  is-closed-under-equiv-subuniverses : UU (α l1 ⊔ α l2 ⊔ lsuc l1 ⊔ lsuc l2)
  is-closed-under-equiv-subuniverses =
    (X : UU l1) (Y : UU l2) → X ≃ Y → type-Prop (P l1 X) → type-Prop (P l2 Y)

  is-prop-is-closed-under-equiv-subuniverses :
    is-prop is-closed-under-equiv-subuniverses
  is-prop-is-closed-under-equiv-subuniverses =
    is-prop-iterated-Π 4 (λ X Y e x → is-prop-type-Prop (P l2 Y))

  is-closed-under-equiv-subuniverses-Prop :
    Prop (α l1 ⊔ α l2 ⊔ lsuc l1 ⊔ lsuc l2)
  pr1 is-closed-under-equiv-subuniverses-Prop =
    is-closed-under-equiv-subuniverses
  pr2 is-closed-under-equiv-subuniverses-Prop =
    is-prop-is-closed-under-equiv-subuniverses

The global type of global subuniverses

record global-subuniverse (α : Level → Level) : UUω where
  field
    subuniverse-global-subuniverse :
      (l : Level) → subuniverse l (α l)

    is-closed-under-equiv-global-subuniverse :
      (l1 l2 : Level) →
      is-closed-under-equiv-subuniverses α subuniverse-global-subuniverse l1 l2

open global-subuniverse public

module _
  {α : Level → Level} (P : global-subuniverse α)
  where

  is-in-global-subuniverse : {l : Level} → UU l → UU (α l)
  is-in-global-subuniverse {l} X =
    is-in-subuniverse (subuniverse-global-subuniverse P l) X

  type-global-subuniverse : (l : Level) → UU (α l ⊔ lsuc l)
  type-global-subuniverse l =
    type-subuniverse (subuniverse-global-subuniverse P l)

  inclusion-global-subuniverse :
    {l : Level} → type-global-subuniverse l → UU l
  inclusion-global-subuniverse {l} =
    inclusion-subuniverse (subuniverse-global-subuniverse P l)

Maps in a subuniverse

We say a map is in a global subuniverse if each of its fibers is.

module _
  {α : Level → Level} (P : global-subuniverse α)
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  is-in-map-global-subuniverse : (A → B) → UU (α (l1 ⊔ l2) ⊔ l2)
  is-in-map-global-subuniverse f =
    (y : B) →
    is-in-subuniverse (subuniverse-global-subuniverse P (l1 ⊔ l2)) (fiber f y)

The predicate of essentially being in a subuniverse

We say a type is essentially in a global universe at universe level l if it is essentially in the subuniverse at level l.

module _
  {α : Level → Level} (P : global-subuniverse α)
  {l1 : Level} (l2 : Level) (X : UU l1)
  where

  is-essentially-in-global-subuniverse : UU (α l2 ⊔ l1 ⊔ lsuc l2)
  is-essentially-in-global-subuniverse =
    is-essentially-in-subuniverse (subuniverse-global-subuniverse P l2) X

  is-prop-is-essentially-in-global-subuniverse :
    is-prop is-essentially-in-global-subuniverse
  is-prop-is-essentially-in-global-subuniverse =
    is-prop-is-essentially-in-subuniverse
      ( subuniverse-global-subuniverse P l2) X

  is-essentially-in-global-subuniverse-Prop : Prop (α l2 ⊔ l1 ⊔ lsuc l2)
  is-essentially-in-global-subuniverse-Prop =
    is-essentially-in-subuniverse-Prop (subuniverse-global-subuniverse P l2) X

Properties