I have the following initial thoughts but can't work out to define zero as 
a w type

data Zro : Set  where

data One : Set where
  O1 : One

data Two : Set where
  O2 : Two
  I2 : Two
-- w types 

rec2 : (x y : Set) -> Two -> Set
rec2 x _ O2 = x
rec2 _ y I2 = y


data W (A : Set) (B : A -> Set) : Set where -- well founded trees
  w : (s : A) -> B s -> W A B
  sup : (a : A) -> ((B a) -> ((x : A) -> W A B )) -> W A B

natw : Set
natw = W Two (rec2 Zro One) -- nat type as w type

zero_w : natw
zero_w = sup O2 (λ x y → {!!})