Raising universe levels

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Daniel Gratzer and Elisabeth Stenholm.

Created on 2022-01-26.
Last modified on 2023-11-27.

module foundation.raising-universe-levels where
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.univalence
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.embeddings
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.propositional-maps
open import foundation-core.propositions
open import foundation-core.sets


In Agda, types have a designated universe levels, and universes in Agda don't overlap. Using data types we can construct for any type A of universe level l an equivalent type in any higher universe.


data raise (l : Level) {l1 : Level} (A : UU l1) : UU (l1  l) where
  map-raise : A  raise l A

data raiseω {l1 : Level} (A : UU l1) : UUω where
  map-raiseω : A  raiseω A


Types are equivalent to their raised equivalents

module _
  {l l1 : Level} {A : UU l1}

  map-inv-raise : raise l A  A
  map-inv-raise (map-raise x) = x

  is-section-map-inv-raise : (map-raise  map-inv-raise) ~ id
  is-section-map-inv-raise (map-raise x) = refl

  is-retraction-map-inv-raise : (map-inv-raise  map-raise) ~ id
  is-retraction-map-inv-raise x = refl

  is-equiv-map-raise : is-equiv (map-raise {l} {l1} {A})
  is-equiv-map-raise =

compute-raise : (l : Level) {l1 : Level} (A : UU l1)  A  raise l A
pr1 (compute-raise l A) = map-raise
pr2 (compute-raise l A) = is-equiv-map-raise

Raise : (l : Level) {l1 : Level} (A : UU l1)  Σ (UU (l1  l))  X  A  X)
pr1 (Raise l A) = raise l A
pr2 (Raise l A) = compute-raise l A

Raising universe levels of propositions

raise-Prop : (l : Level) {l1 : Level}  Prop l1  Prop (l  l1)
pr1 (raise-Prop l P) = raise l (type-Prop P)
pr2 (raise-Prop l P) =
  is-prop-equiv' (compute-raise l (type-Prop P)) (is-prop-type-Prop P)

Raising universe levels of sets

raise-Set : (l : Level) {l1 : Level}  Set l1  Set (l  l1)
pr1 (raise-Set l A) = raise l (type-Set A)
pr2 (raise-Set l A) =
  is-set-equiv' (type-Set A) (compute-raise l (type-Set A)) (is-set-type-Set A)

Raising equivalent types

module _
  {l1 l2 : Level} (l3 l4 : Level) {A : UU l1} {B : UU l2} (e : A  B)

  map-equiv-raise : raise l3 A  raise l4 B
  map-equiv-raise (map-raise x) = map-raise (map-equiv e x)

  map-inv-equiv-raise : raise l4 B  raise l3 A
  map-inv-equiv-raise (map-raise y) = map-raise (map-inv-equiv e y)

  is-section-map-inv-equiv-raise :
    ( map-equiv-raise  map-inv-equiv-raise) ~ id
  is-section-map-inv-equiv-raise (map-raise y) =
    ap map-raise (is-section-map-inv-equiv e y)

  is-retraction-map-inv-equiv-raise :
    ( map-inv-equiv-raise  map-equiv-raise) ~ id
  is-retraction-map-inv-equiv-raise (map-raise x) =
    ap map-raise (is-retraction-map-inv-equiv e x)

  is-equiv-map-equiv-raise : is-equiv map-equiv-raise
  is-equiv-map-equiv-raise =

  equiv-raise : raise l3 A  raise l4 B
  pr1 equiv-raise = map-equiv-raise
  pr2 equiv-raise = is-equiv-map-equiv-raise

Raising universe levels from l1 to l ⊔ l1 is an embedding from UU l1 to UU (l ⊔ l1)

  is-emb-raise : (l : Level) {l1 : Level}  is-emb (raise l {l1})
  is-emb-raise l {l1} =
      ( λ X 
          ( λ (A , p) 
              ( Σ (UU l1)  A'  A'  A))
              ( equiv-tot
                ( λ A' 
                  ( equiv-postcomp-equiv (inv-equiv (compute-raise l A)) A') ∘e
                  ( equiv-precomp-equiv (compute-raise l A') (raise l A)) ∘e
                  ( equiv-univalence) ∘e
                  ( equiv-concat' (raise l A') (inv p))))
              ( is-torsorial-equiv' A)))

emb-raise : (l : Level) {l1 : Level}  UU l1  UU (l1  l)
pr1 (emb-raise l) = raise l
pr2 (emb-raise l) = is-emb-raise l

Recent changes