[TYPES] Implementing induction principles

[Patricia Johann]

Dear Types,

I'm trying to implement the induction principle for the natural numbers.

Briefly, given P: Nat -> * and

u: P(0)
v: forall n:Nat. Pn -> P(n+1)

I can bundle these together to form a 1+_-algebra on the type Sigma n:Nat. 
P n, i.e., a function

my_algebra  : (1 + Sigma n:Nat. P n) -> Sigma n:Nat. P n
my_algebra = [ (0,u), \(n,p) -> (n+1, v n p)]

Then I can write

ind P :: forall n:Nat. P n
ind P n = p where (m,p) = iterate my_algebra n

To show that this is correct, I need to show that n=m. This is easily done 
using the uniqueness of the iteration operator.

Here are my questions:

1. Can I implement ind in a programming language, theorem prover or 
intensional type theory where the uniqueness of the iteration operator is 
not available? Maybe this can be done because I only need to know that 
projection after a specific iterator is the identity. Or maybe there is a 
different approach to implementing ind?

2. Is there a programming language or theorem prover where the uniqueness 
of the iteration operator can be used?

3. Or are there theoretical reasons (perhaps due to undecidability of type 
checking) why this is not possible?

Thanks very much in advance,
-patty