Life without the terminal type

Abstract

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 A-calculus with surjective pairing, in particular concerning the decision problem for equality of terms in the presence of a terminal type, are comparatively involved.