In the paper "Efficiency of Lambda-Encodings in Total Type Theory" 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 -> t) -> f r -> t Fix f = forall t. Alg f t -> t -- Natural numbers NatF r = forall t. t -> (r -> t) -> 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 -> 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 -> t] (\x. alg [t] (\y. y) (/\t. \z s. z)) (/\t. \z s. s (/\t. \x. x))