 The Unifying Principle was extended to elementary type theory (the system \(\cT\) of  Section 1.3.2)  in Andrews 1971 by applying ideas in Takahashi 1967. This Unifying Principle for \(\cT\) has been used to establish cut-elimination for \(\cT\) in Andrews 1971 and completeness proofs for various systems of type theory in Huet 1973a, Kohlhase 1995, and Miller 1983. We first give a definition and then state the principle.