by Lutz Schröder
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 lambda-calculus with surjective pairing, in particular concerning the decision problem for equality of terms in the presence of a terminal type, are comparatively involved.
Reference:
Lutz Schröder: Life without the Terminal Type, In Laurent Fribourg, ed.: Computer Science Logic, Lecture Notes in Computer Science, vol. 2142, pp. 429–442, Springer; Berlin; http://www.springer.de, 2001. [preprint]
Bibtex Entry:
@InProceedings{Schroder01c,
author = {Lutz Schr{\"o}der},
title = {Life without the Terminal Type},
year = {2001},
editor = {Laurent Fribourg},
booktitle = {Computer Science Logic},
publisher = {Springer; Berlin; http://www.springer.de},
series = {Lecture Notes in Computer Science},
volume = {2142},
pages = {429--442},
keywords = {terminal type lambda calculus topos},
url = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=2142&spage=429},
comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/TermType.pdf"> [preprint] </a>},
psurl = {http://www8.informatik.uni-erlangen.de/~schroeder/papers/TermType.ps},
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 lambda-calculus with surjective pairing, in particular concerning the decision problem for equality of terms in the presence of a terminal type, are comparatively involved.
},
}