I'm just wondering if induction can be obtained for church-based Nat Nat type on Idris, Agda, Coq and the like. Please note that this is another problem related to its implementation on CoC (which, as you know, is impossible), because we have much more expressiveness (we can, for example, extract the second Sigma element).
Here is a bad proof sketch on Idris (there were 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 do this by creating a Sigma type starting from CZ ** zto path to CS (CS ... CZ) ** s (s ... z). The problem is that although I know that its first element will be equal n, I'm not sure how to prove it.