The maximality of the typed lambda calculus and of cartesian closed categories (Q2724040)

The proof of the maximality of the cartesian closed categories presented in this paper is based on the analogue of Böhm's theorem for the typed lambda calculus, a version of which was established by R. Statman [\textit{R. Statman}, Arch. Math. Logik Grundlagenforsch. 23, 21-26 (1983; Zbl 0537.03009)]. The authors prove this analogue first for the typed lambda calculus with only functional types and from that they pass to the analogue of Böhm's theorem for the typed lambda calculus with product types added. To pass from the analogue of Böhm's theorem for the typed lambda calculus with product types to the maximality result for the cartesian closed categories the authors use the categorical equivalence between typed lambda calculus and cartesian closed categories [\textit{J. Lambek} and \textit{P. J. Scott}, Introduction to higher order categorical logic, Cambridge University Press, Cambridge (1986; Zbl 0596.03002)]. Although the results presented in this paper were already established [\textit{A. K. Simpson}, in: M. Dezani-Ciancaglini and G. Plotkin (eds.), Typed lambda calculi and applications, Lect. Notes Comput. Sci. 902, 414-427 (1995; Zbl 0813.68040)], the proofs are essentially different thus providing the possibility of shedding some new light on the matter.