...need indexed functors...

adt.idr

%default total

data Id : Type -> Type where
    I : a -> Id a

data Const : (a : Type) -> (b : Type) -> Type where
    K : a -> Const a b

data Sum : (a : Type -> Type) -> (b : Type -> Type) -> (c : Type) -> Type where
    SumL : a c -> Sum a b c
    SumR : b c -> Sum a b c

data ProdT : (a : Type -> Type) -> (b : Type -> Type) -> (c : Type) -> Type where
    Prod : a c -> b c -> ProdT a b c

Zero : Type
Zero = Void

One : Type -> Type
One = Const ()

instance Functor Id where
    map f (I x) = I (f x)

instance Functor (Const a) where
    map _ (K x) = K x

instance (Functor a, Functor b) => Functor (Sum a b) where
    map f (SumL x) = SumL (f `map` x)
    map f (SumR x) = SumR (f `map` x)

instance (Functor a, Functor b) => Functor (ProdT a b) where
    map f (Prod x y) = Prod (f `map` x) (f `map` y)
    
data Fix : (Type -> Type) -> Type where
    In : x (Fix x) -> Fix x

Nats : Type
Nats = Fix (Sum One Id)

zero : Nats
zero = In $ SumL $ K ()

suc : Nats -> Nats
suc = In . SumR . I

omega : Nats
omega = In $ SumR $ I omega