 Extensions of the above Unifying principle towards Church’s type theory with general semantics were studied since the mid nineties. A primary motivation was to support (refutational) completeness investigations for the proof calculi underlying the emerging higher-order automated theorem provers (see  Section 4  below). The initial interest was on a fragment of Church’s type theory, called extensional type theory, that includes the extensionality axioms, but excludes \(\iota_{(\alpha({o}\alpha))}\) and the axioms for it (description and choice were largely neglected in the automated theorem provers at the time). Analogous to before, a distinction has been made between extensional type theory with defined equality (as in  Section 1.2.1,  where equality is defined via Leibniz’ principle) and extensional type theory with primitive equality (e.g., system \(\cQ_0\) as in  Section 1.4,  or, alternatively, a system based on logical constants \(\nsim_{({o}{o})}, \lor_{(({o}{o}){o})}\), and the \(\Pi_{({o}({o}\alpha))}\)’s as in  Section 1.2.1,  but with additional primitive logical constants \(=_{{o}\alpha\alpha}\) added).