{-# OPTIONS --cubical-compatible --no-import-sorts #-}
module Terra.Data.Level where
open import Agda.Primitive public using (Set ; Level ; _⊔_ ; lsuc ; lzero ; SSet)

record Lift {ℓ : Level} (A : Set ℓ) (L : Level) : Set (ℓ ⊔ L) where
  constructor lift
  field
    low : A