[TYPES] Eliminators in type theory

[Yong Luo]

Dear all,

Thanks for your reponse to my question. I have got a few different
definitions of the fib function. All the definitions looks quite different
from the original one. So I still have anther question.

>From the definitions, we can prove that fib (n+2) is equal to fib n + fib
(n+1) for all n. However, they are not definitionally (or computationally)
equal to each other. In other words, if n is a variable, then fib (n+2)
cannot be reduced to fib n + fib (n+1). So, my question is the following.

Suppose that we have a normal type system, for example, a type system with
Nat, Pairs and function type with their eliminatiors and computation rules.
Can we define the fib function such that fib (n+2) can be reduced to fib n +
fib (n+1) where n is a variable?

Regards,

Yong