 We discussed earlier how the \(\lambda\)-calculus is a non-extensional theory of functions. If, in the non-extensional spirit, we understand \(\lambda\)-terms as descriptions, how should we treat equality of \(\lambda\)-terms? Various approaches are available. In this section, let us treat the equality relation = as a primitive, undefined relation holding between two \(\lambda\)-terms, and try to axiomatize the properties that equality should have. The task is to identity axioms and formulate suitable rules of inference concerning the equality of \(\lambda\)-terms.