Is it possible to derive induction for the church-encoded Nat?

Question

I was just wondering if it is possible to derive induction for the church-encoded Nat type on Idris, Agda, Coq and similar. Notice this is a different issue from doing it on CoC (which is known to be impossible) because we have much more expressivity on those (we're able to, for example, extract the second element of Sigma).

Here is a poor proof sketch on Idris (had a lot of syntax issues):

CN : Type
CN = (t : Type) -> t -> (t -> t) -> t

CS : CN -> CN
CS n t z s = s (n t z s)

CZ : CN
CZ t z s = z

ind :
  (p : CN -> Type) ->
  (z : p CZ) ->
  (s : (n : CN) -> p n -> p (CS n)) ->
  (n : CN) ->
  p n

ind p z s n =
  let base_case  = the (x : CN ** p x) (CZ ** z) 
      step_case  = the ((x : CN ** p x) -> (y : CN ** p y)) (\ (n ** pf) => (CS n ** s n pf))
      result     = the (x : CN ** p x) (n (x : CN ** p x) base_case step_case)
      fst_result = fst result
      snd_result = snd result
      fst_is_n   = the (fst_result = n) ?fst_is_n
  in  ?wat

I'm doing it by building a Sigma type starting from CZ ** z all way up to CS (CS ... CZ) ** s (s ... z). Problem is that, while I know the first element of it will be equal to n, I'm not sure how to prove it.

Answer 1

Here's a related question I asked about homotopy type theory. I am also a little out my depth here, so take all this with a grain of salt.

I've proved that CN is isomorphic to Nat iff the free theorm for CN holds. Furthermore, it's known that there are no free theorems under the law of excluded middle (in HoTT). I.e. with LEM, you could could define CNs such as

foo : CN
foo T z s = if T is Bool then not z else z

which is not a proper church natural and would not be covered by the induction principle. Because excluded middle and HoTT are consistent with the type theories you are asking about (as far as I know), it follows that there will not be a proof of ind.

Answer 2

It is known not to be provable because there are models of the calculus of constructions where the impredicative encoding of the natural numbers is not initial (i.e. doesn't satisfy induction). It does follow from relational parametricity as Phil Wadler has shown long time ago. Hence combining Wadler with internal relational parametricity ala Moulin and Bernardy may do the trick.