We can write inductive types in terms of a fixpoint type:
Fix : (* -> *) -> * In : (f : * -> *) -> f (Fix f) -> Fix f NatF r = () + r Nat = Fix NatF Z = In NatF (InL ()) S n = In NatF (InR n)
But this fix type is not sufficient for indexed datatypes and we need an indexed fixpoint:
IFix : (I : *) -> ((I -> *) -> (I -> *)) -> I -> * IIn : (I : *) -> (F : (I -> *) -> (I -> *)) -> (i : I) -> F (IFix I F) i -> IFix I F i FinF r n = (n = Z) + ((m : Nat) ** r m ** (n = S m)) Fin = IFix Nat FinF
IFix we can get
Fix back by setting the index type to unit.
What datatypes can we not write using
IFix, is there a more general fixpoint than