UNIT : Ty n
UNIT = Nu $ TVar FZ

tt : Term {n=0} g UNIT
tt = App (Ana {a=V~>V} $ Lam $ Var Here) (Lam $ Var Here)

CONAT : Ty n
CONAT = Nu $ Sum UNIT (TVar FZ)

pred : Term {n=0} g (CONAT ~> Sum UNIT CONAT)
pred = Lam $ Out $ Var Here

zero : Term {n=0} g CONAT
zero = App (Ana {a=V~>V} $ Lam $ Inl tt) (Lam $ Var Here)

succ : Term {n=0} g (CONAT ~> CONAT)
succ = Lam $ App (Ana $ Lam $ Inr $ Var Here) (Var Here)

omega : Term {n=0} g CONAT
omega = App (Ana $ Lam $ Inr $ Var Here) tt