Life without the Terminal Type

We introduce a method of extending arbitrary categories by a terminal object and apply this method in various type theoretic settings. In particular, we show that categories that are cartesian closed except for the lack of a terminal object have a universal full extension to a cartesian closed category, and we characterize categories for which the latter category is a topos. Both the basic construction and its correctness proof are extremely simple. This is quite surprising in view of the fact that the corresponding results for the simply typed λ-calculus with surjective pairing, in particular concerning the decision problem for equality of terms in the presence of a terminal type, are comparatively involved.

• Type: Conference
• Year: 2001
• Where: CSL
• Authors: Lutz Schröder
• Keywords: Automated Reasoning, Cartesian Closed, Cartesian Closed Category, CSL 2001, Terminal Object