Weed.agda

module Weed where

data ⊥ : Set where

magic : {A : Set} → ⊥ → A
magic ()

data Weed (A : Set) : Set where
  grow : (A → Weed A) → Weed A

smoke : {A : Set} (P : Weed A → Set)
  (p : (f : A → Weed A) (ih : (a : A) → P (f a)) → P (grow f))
  (w : Weed A) → P w
smoke P p (grow f) = p f λ a → smoke P p (f a)

smokeout : {A : Set} → A → Weed A → ⊥
smokeout a = smoke _ λ f ih → ih a

weed-is-magic : {A B : Set} → A → Weed A → B
weed-is-magic a w = magic (smokeout a w)