For example, let's see how to define induction principle for Nat.
We should define two terms with the following types:
NatRec : (R : Set) -> R -> (R -> R) -> Nat -> R
NatInd : (C : Nat -> Set) -> (C zero) -> ((n : Nat) -> C n -> C (suc n)) -> (n : Nat) -> (C n)
For the first we can represent zero and suc as functions of the first type (it will be church literals). However, we can't do the same for the second. We can create a term which has that type but it won't typecheck.
