# Type of induction principle for fixpoint types

To the Calculus of Constructions we could add a general fixpoint type constructor (accepting inconsistencies or assuming F is a Functor):

Fix : (* -> *) -> *
in  : ∀F. F (Fix F) -> Fix F
out : ∀F. Fix F -> F (Fix F)


We can then write down the type of case discrimination and folding:

case : ∀F T. (F (Fix F) -> T) -> Fix F -> T
fold : ∀F T. (F T -> T) -> Fix F -> T


But what is the type of induction (if there is one)? I've gotten this far:

ind : ∀F T (P : Fix F -> *). (∀(h : Fix F). P h -> P ???) -> (x : Fix F) -> P x


Assuming the rest is correct, what should be in the place of ???? Alternatively, what is the type of dependent case discrimination?

• The word induction is used when we construct an inductive type, i.e., the smallest or initial fixed point of a type constructor $F$. However, a general type constructor need not have an initial or smallest fixed point, and therefore no reasonable induction principle can be stated in general. – Andrej Bauer Jan 28 at 17:42
• If we let $F(X) = X \to \mathsf{Empty}$, what is $\mathsf{Fix}(F)$? – Andrej Bauer Jan 28 at 17:43
• If we constrain F in some way (for example strictly positive occurrences of X), can we then state a induction principle? – Labbekak Jan 28 at 17:53
• I think you need an additional constraint over $F$, namely that it is behaves well over "fibrations", i.e. that there is some function lift_fiber : forall A : *, (A -> *) -> (F A -> *). This is certainly enough to express what you need. – cody Jan 28 at 20:37
• @cody: right, and we don't need any strict positivity, just covariance, in order to phraase the induction principle. – Andrej Bauer Jan 28 at 20:45

ind : ∀F T (P : Fix F -> *). ((h : F (Σ (Fix F) P)) -> P (in (map fst h))) -> (x : Fix F) -> P x

With Σ being the dependent product and map the functor map of F.
• Just a note, having this Fix type is not enough to derive induction for inductive datatypes like Nat or List. You'd also need an induction principle for F. If F is constructed from unit, sums and products then you'd need induction principles for those. – Labbekak Feb 11 at 11:34