module WellFoundedTree where

open import Level

infix  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