Global subuniverses

Content created by Fredrik Bakke and Egbert Rijke.

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

module where
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


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.


The predicate on families of subuniverses of being closed under equivalences

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

  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 =
  pr2 is-closed-under-equiv-subuniverses-Prop =

The global type of global subuniverses

record global-subuniverse (α : Level  Level) : UUω where
    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 α)

  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}

  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)

  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 =
      ( 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


Global subuniverses are closed under homogenous equivalences

This is true for any family of subuniverses indexed by universe levels.

module _
  {α : Level  Level} (P : global-subuniverse α)
  {l : Level} {X Y : UU l}

  is-in-global-subuniverse-homogenous-equiv :
    X  Y  is-in-global-subuniverse P X  is-in-global-subuniverse P Y
  is-in-global-subuniverse-homogenous-equiv =
    is-in-subuniverse-equiv (subuniverse-global-subuniverse P l)

  is-in-global-subuniverse-homogenous-equiv' :
    X  Y  is-in-global-subuniverse P Y  is-in-global-subuniverse P X
  is-in-global-subuniverse-homogenous-equiv' =
    is-in-subuniverse-equiv' (subuniverse-global-subuniverse P l)

Characterization of the identity type of global subuniverses at a universe level

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

  equiv-global-subuniverse-Level : (X Y : type-global-subuniverse P l)  UU l
  equiv-global-subuniverse-Level =
    equiv-subuniverse (subuniverse-global-subuniverse P l)

  equiv-eq-global-subuniverse-Level :
    (X Y : type-global-subuniverse P l) 
    X  Y  equiv-global-subuniverse-Level X Y
  equiv-eq-global-subuniverse-Level =
    equiv-eq-subuniverse (subuniverse-global-subuniverse P l)

    is-equiv-equiv-eq-global-subuniverse-Level :
      (X Y : type-global-subuniverse P l) 
      is-equiv (equiv-eq-global-subuniverse-Level X Y)
    is-equiv-equiv-eq-global-subuniverse-Level =
      is-equiv-equiv-eq-subuniverse (subuniverse-global-subuniverse P l)

  extensionality-global-subuniverse-Level :
    (X Y : type-global-subuniverse P l) 
    (X  Y)  equiv-global-subuniverse-Level X Y
  extensionality-global-subuniverse-Level =
    extensionality-subuniverse (subuniverse-global-subuniverse P l)

  eq-equiv-global-subuniverse-Level :
    {X Y : type-global-subuniverse P l} 
    equiv-global-subuniverse-Level X Y  X  Y
  eq-equiv-global-subuniverse-Level =
    eq-equiv-subuniverse (subuniverse-global-subuniverse P l)

  compute-eq-equiv-id-equiv-global-subuniverse-Level :
    {X : type-global-subuniverse P l} 
    eq-equiv-global-subuniverse-Level {X} {X} (id-equiv {A = pr1 X})  refl
  compute-eq-equiv-id-equiv-global-subuniverse-Level =
    compute-eq-equiv-id-equiv-subuniverse (subuniverse-global-subuniverse P l)

Equivalences of families of types in a global subuniverse

fam-global-subuniverse :
  {α : Level  Level} (P : global-subuniverse α)
  {l1 : Level} (l2 : Level) (X : UU l1)  UU (α l2  l1  lsuc l2)
fam-global-subuniverse P l2 X = X  type-global-subuniverse P l2

module _
  {α : Level  Level} (P : global-subuniverse α)
  {l1 : Level} (l2 : Level) {X : UU l1}
  (Y Z : fam-global-subuniverse P l2 X)

  equiv-fam-global-subuniverse : UU (l1  l2)
  equiv-fam-global-subuniverse =
    equiv-fam-subuniverse (subuniverse-global-subuniverse P l2) Y Z

  equiv-eq-fam-global-subuniverse :
    Y  Z  equiv-fam-global-subuniverse
  equiv-eq-fam-global-subuniverse =
    equiv-eq-fam-subuniverse (subuniverse-global-subuniverse P l2) Y Z

  is-equiv-equiv-eq-fam-global-subuniverse :
    is-equiv equiv-eq-fam-global-subuniverse
  is-equiv-equiv-eq-fam-global-subuniverse =
    is-equiv-equiv-eq-fam-subuniverse (subuniverse-global-subuniverse P l2) Y Z

  extensionality-fam-global-subuniverse :
    (Y  Z)  equiv-fam-global-subuniverse
  extensionality-fam-global-subuniverse =
    extensionality-fam-subuniverse (subuniverse-global-subuniverse P l2) Y Z

  eq-equiv-fam-global-subuniverse : equiv-fam-global-subuniverse  Y  Z
  eq-equiv-fam-global-subuniverse =
    map-inv-is-equiv is-equiv-equiv-eq-fam-global-subuniverse

See also

Recent changes