# Raising universe levels

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

Created on 2022-01-26.

module foundation.raising-universe-levels where

Imports
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


## Idea

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.

## Definition

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


## Properties

### Types are equivalent to their raised equivalents

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

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 =
is-equiv-is-invertible
map-inv-raise
is-section-map-inv-raise
is-retraction-map-inv-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)
where

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 =
is-equiv-is-invertible
map-inv-equiv-raise
is-section-map-inv-equiv-raise
is-retraction-map-inv-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)

abstract
is-emb-raise : (l : Level) {l1 : Level} → is-emb (raise l {l1})
is-emb-raise l {l1} =
is-emb-is-prop-map
( λ X →
is-prop-is-proof-irrelevant
( λ (A , p) →
is-contr-equiv
( Σ (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