{-# OPTIONS --cubical-compatible #-}

module Terra.Data.Level.Variables where
open import Terra.Data.Level public

variable
  ℓ ℓ′ ℓ″ ℓ‴ ℓ⁗ ℓ′′ : Level
  ℓ' ℓ'' : Level