Type of induction principle for fixpoint types
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.