7
_⊔_ : Level → Level → Level
9
{-# BUILTIN LEVEL Level #-}
10
{-# BUILTIN LEVELZERO lzero #-}
11
{-# BUILTIN LEVELSUC lsuc #-}
12
{-# BUILTIN LEVELMAX _⊔_ #-}
14
record R (ℓ : Level) : Set ℓ where
19
module M (r : ∀ ℓ → R ℓ) where
21
data D (ℓ : Level) : Set ℓ where
23
id : ∀ {a} {A : Set a} → A → A
29
P : ∀ {ℓ} → K → Set ℓ → Set ℓ
36
Foo : ∀ {k a} {A : Set a} → P k A → Set