Is the Mendler-encoding in System-F adequate? In the paper &quot;Efficiency of Lambda-Encodings in Total Type Theory&quot; it is mentioned that the Church-encoding is adequate and the Parigot encoding is not adequate. This means that any inhabitant of an encoded datatype actually represents an element of the datatype.
My question is if the Mendler-style encoding is adequate. I think I found a counter example (in System F):
-- Mendler-style encoding
Alg f t = forall r. (r -&gt; t) -&gt; f r -&gt; t
Fix f = forall t. Alg f t -&gt; t

-- Natural numbers
NatF r = forall t. t -&gt; (r -&gt; t) -&gt; t
Nat = Fix Nat

-- the valid constructors for natural numbers
Z : Nat = /\t. \alg. alg [Nat] (\y. y [t] alg) (/\t. \z s. z)
S : Nat -&gt; Nat = \n. /\t. \alg. alg [Nat] (\y. y [t] alg) (/\t. \z s. s n)

-- An inhabitant of Nat that is not a valid natural number
wrong : Nat =
  /\t. \alg.
    alg [forall t. t -&gt; t]
    (\x. alg [t] (\y. y) (/\t. \z s. z))
    (/\t. \z s. s (/\t. \x. x))
$\newcommand{\Alg}{\mathsf{Alg}\ }$
$\newcommand{\NatF}{\mathsf{NatF}\ }$
$\newcommand{\Nat}{\mathsf{Nat}}$
$\newcommand{\map}{\mathrm{map}\ }$
$\newcommand{\Z}{\mathrm{Z}}$
$\newcommand{\S}{\mathrm{S}}$
I don't think this is an actual counter-example.
Parametricity implies:
$$∀(α : \Alg \NatF t) (g : r → t)(x : \NatF r). \\
α\ [r]\ g\ x = α\ [t]\ (λx.x)\ (\map g\ x)
$$
(a special case of the free theorem), where
$$\map g\ x = Λt. λz\ s. x\ [t]\ z\ (s \circ h)$$
let:
$$h : (∀s. s → s) → t \\
h\ \_ = α\ [t]\ (λy. y)\ (Λt. λz\ s. z)$$
which is your first argument to $α$. Then in your example:
$$α\ [∀s. s→s]\ h\ x \\
= α\ [t]\ (λx.x)\ (\map h\ x) \\
= α\ [t]\ (λx.x)\ (Λt. λ\_\ s. s (α\ [t]\ (λx. x)\ (Λt. λz\ \_. z)))$$
Now observe the following from $\Z$ and $\S$
$$
α\ [\Nat]\ (λy. y\ [t]\ α)\ (Λt. λz\ \_. z)  \\
  = α\ [t]\ (λx.x)\ (\map (λy. y\ [t]\ α) (Λt. λz\ \_. z)) \\
  = α\ [t]\ (λx.x)\ (Λt. λz\ \_. z)
$$
$$
α\ [\Nat]\ (λy. y\ [t]\ α)\ (Λt. λ\_\ s. s\ n) \\
 = α\ [t]\ (λx.x)\ (map (λy. y\ [t]\ α) (Λt. λ\_\ s. s n)) \\
 = α\ [t]\ (λx.x)\ (Λt. λ\_\ s. s (n\ [t]\ α))
$$
Then, if we go back to the calculation from your example:
$$
α\ [t]\ (λx.x)\ (Λt. λ\_ s. s (α\ [t]\ (λx.x)\ (Λt. λz\ \_. z))) \\
  = α\ [t]\ (λx.x)\ (Λt. λ\_\ s. s (\Z\ [t]\ α)) \\
  = \S\ \Z\ [t]\ α
$$
So your example is extensionally equal to $1$, assuming my calculations are correct.