 This is usually called a “definitional equality” because it can be decided by normalizing the terms \(a\) and \(a'\) and checking whether the normal forms are identical. However, this equality is a judgment and not a proposition (type) and we thus cannot prove such judgmental equalities by induction. For this reason we need to introduce propositional identity types. For example, the identity type for natural numbers \(\I(\N,m,n)\) can be defined by \(\U\)-valued primitive recursion. We can then express and prove the Peano axioms. Moreover, extensional equality of ufnctions can be defined by