From Church-encoding to induction principle I am looking for an algorithm to go from a Church-encoded datatype to their induction principle in the Calculus of Constructions. For example:

Unit = {t : *} -&gt; t -&gt; t
~&gt;
(x : Unit) -&gt; {P : Unit -&gt; *} -&gt; P (\{t} x. x) -&gt; P x


Nat = {t : *} -&gt; t -&gt; (t -&gt; t) -&gt; t
~&gt;
(x : Nat) -&gt; {P : Nat -&gt; *} -&gt; P (\{t} z s. z) -&gt; ({m : Nat} -&gt; P m -&gt; P (\{t} z s. s (m {t} z s))) -&gt; P x


It seems like this should be possible for any Church-encoded datatype. Does anybody know such an algorithm/translation or resources on it?
Let $F : \mathsf{Type} \to \mathsf{Type}$ be a type constructor and let $W_F$ be the inductive type defined by $W_F = F W_F$. Not every $F$ has such an inductive types, but this is not important for this discussion.

The starting point of Church's encodings is the observation that $W_F$ ought to be
$$\forall T : \mathsf{Type} \,.\, (F T \to T) \to T.$$
Thus, to get an induction principle out of a Church encoding, we take the following steps:


Rewrite the Church encoding in the form $\forall T : \mathsf{Type} \,.\, (F T \to T) \to T$ for a suitable $F$.
Derive an induction principle for $F$, as in your own answer to your own question.


Let us try a couple of examples.

Unit type

\begin{align*}
\mathsf{unit} &amp;= \forall T . T \to T \\
&amp;= \forall T . (1 \to T) \to T \\
&amp;= \forall T . (F T \to T) \to T
\end{align*}
where $F X = 1$.

Empty type

\begin{align*}
\mathsf{unit} &amp;= \forall T . T \\
&amp;= \forall T . 1 \to T \\
&amp;= \forall T . (0 \to T) \to T \\
&amp;= \forall T . (F T \to T) \to T
\end{align*}
where $F X = 0$.

Natural numbers

\begin{align*}
\mathsf{nat} &amp;= \forall T . (T \to T) \to (T \to T) \\
&amp;= \forall T . (T \to T) \times T \to T \\
&amp;= \forall T . T \times (T \to T) \to T \\
&amp;= \forall T . ((1 + T) \to T) \to T \\
&amp;= \forall T . (F T \to T) \to T
\end{align*}
where $F X = 1 + X$.

Binary trees

We can also go backwards. The binary trees are the inductive type for $F X = 1 + X \times X$, thus their Church encoding is

\begin{align*}
\mathsf{tree} &amp;= \forall T . (F T \to T) \to T \\
&amp;= \forall T . ((1 + T \times T) \to T) \to T \\
&amp;= \forall T . (T \times (T \times T \to T) \to T \\
&amp;= \forall T . T \to (T \to T \to T) \to T
\end{align*}

It all works beautifully.