# Is there a most general fixpoint?

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


Using 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 IFix?