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 : (* -&gt; *) -&gt; *
in  : ∀F. F (Fix F) -&gt; Fix F
out : ∀F. Fix F -&gt; F (Fix F)


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

case : ∀F T. (F (Fix F) -&gt; T) -&gt; Fix F -&gt; T
fold : ∀F T. (F T -&gt; T) -&gt; Fix F -&gt; T


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

ind : ∀F T (P : Fix F -&gt; *). (∀(h : Fix F). P h -&gt; P ???) -&gt; (x : Fix F) -&gt; P x


Assuming the rest is correct, what should be in the place of ????
Alternatively, what is the type of dependent case discrimination?
To answer my own question, the paper Generic derivation of induction for impredicative encodings in Cedille shows a type for induction on a fixpoint type. It can look like:

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


With Σ being the dependent product and map the functor map of F.