Induction on Church-encoded natural numbers (which I will call
indNat) can not be defined within the Calculus of Constructions.
If we assumed
indNat as an axiom, is there an untyped term that would have the semantics of the induction function? What if we had Scott-encoded natural numbers and
Can induction be inhabited in CoC +
fix (such that the function would have the proper semantics, not an infinite loop)?