Raising universe levels of the booleans

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2026-05-02.
Last modified on 2026-05-02.

module foundation.raising-universe-levels-booleans where
Imports 
open import foundation.universe-levels

open import foundation-core.booleans
open import foundation-core.equivalences
open import foundation-core.raising-universe-levels

Idea

We can raise the type of booleans to any universe.

Definition

Raising universe levels of the booleans

raise-bool : (l : Level) → UU l
raise-bool l = raise l bool

raise-true : (l : Level) → raise-bool l
raise-true l = map-raise true

raise-false : (l : Level) → raise-bool l
raise-false l = map-raise false

compute-raise-bool : (l : Level) → bool ≃ raise-bool l
compute-raise-bool l = compute-raise l bool

Recent changes