Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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)
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, ()))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment