PUBLICATIONS DE L'INSTITUT MATHÉMATIQUE (BEOGRAD) (N.S.)
Vol. 68(82), pp. 1--19 (2000)
The maximality of the typed lambda calculus and of cartesian closed categories
Kosta Dosen and Zoran Petri\'cMatematicki institit SANU, Beograd, Yugoslavia
Abstract: From the analogue of Böhm's Theorem proved for the typed lamb\-da calculus, without product types and with them, it is inferred that every cartesian closed category that satisfies an equality between arrows not satisfied in free cartesian closed categories must be a preorder. A new proof is given here of these results, which were obtained previously by Richard Statman and Alex K. Simpson.
Classification (MSC2000): 03B40; 18D15
Full text of the article:
Electronic fulltext finalized on: 1 Nov 2001. This page was last modified: 6 Feb 2002.
© 2001 Mathematical Institute of the Serbian Academy of Science and Arts