module WellFoundedTree where open import Level infix 1 W data W {ℓ ℓ' : Level}(A : Set ℓ)(B : A → Set ℓ') : Set (ℓ ⊔ ℓ') where sup : (x : A)(f : B x → W A B) → W A B syntax W A (λ x → B) = W x ∈ A , B