1
{-# OPTIONS --universe-polymorphism #-}
2
module CompareLevel where
4
open import Common.Level
8
Foo : (a b : Level) → Set (a ⊔ b) → Set
9
Bar : Foo _ _ X -- solve _1 ⊔ _2 = 0
12
id : ∀ {a}{A : Set a} → A → A
13
apply : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) → A → B
15
Any : (ℓ : Level) → Set ℓ