Container.idr

module Container

%default total

record Container where
  constructor MkContainer
  shape : Type
  position : shape -> Type

container : Container -> Type -> Type
container (MkContainer s p) x = (v : s ** p v -> x)

data W : Container -> Type where
  In : container c (W c) -> W c

natC : Container
natC = MkContainer Bool (\ b => if b then Void else ())

nat : Type
nat = W natC

zero : Container.nat
zero = In (True ** \ v => absurd v)

succ : Container.nat -> Container.nat
succ n = In (False ** \ _ => n)

Fix.idr

module Fix

%default total

-- A universe of positive functor
data Desc : Type where
  Sig : (a : Type) -> (a -> Desc) -> Desc
  Rec : Desc -> Desc
  End : Desc

-- The decoding function
desc : Desc -> Type -> Type
desc (Sig a d) x = (v : a ** desc (d v) x)
desc (Rec d)   x = (x, desc d x)
desc End       x = ()

-- The least fixpoint of such a positive functor
data Mu : Desc -> Type where
  In : desc d (Mu d) -> Mu d

data NatC = ZERO | SUCC

natD : Desc
natD = Sig NatC $ \ c => case c of
  ZERO => End
  SUCC => Rec End

nat : Type
nat = Mu natD

zero : Fix.nat
zero = In (ZERO ** ())

succ : Fix.nat -> Fix.nat
succ n = In (SUCC ** (n, ()))