×

Locally Cartesian closed categories and type theory. (English) Zbl 0539.03048

From author’s introduction: ”It is well known that for much of the mathematics of topos theory, it is in fact sufficient to use a category C whose slice categories C/A are cartesian closed. In such a category, the notion of a ’generalized set’, for example an ’A-indexed set’, is represented by a morphism \(B\to A\) of C, i.e. by an object of C/A. The point about such a category C is that C is a C-indexed category, and more, is a hyperdoctrine, so that it has a full first order logic associated with it. This logic has some peculiar aspects. For instance, the types are the objects of C and the terms are the morphisms of C. For a given type A, the predicates with a free variable of type A are morphisms into A, and ’proofs’ are morphisms over A. We see here a certain ’ambiguity’ between the notions of type, predicate, and term, of object and proof: a term of type A is a morphism into A, which is a predicate over A; a morphism 1\(\to A\) can be viewed either as an object of type A or as a proof of the proposition A. For a long time now, it has been conjectured that the logic of such categories is given by the type theory of Martin-Löf, since one of the features of Martin-Löf’s type theory is that it formalizes ’ambiguities’ of this sort. However, to the best of my knowledge, no one has ever worked out the details of the relationship, and when the question again arose in the McGill Categorical Logic Seminar in 1981-82, it was felt that making this precise was long overdue. That is the purpose of this paper. We shall describe the system ML, based on Martin-Löf’s system, and show how to construct a locally cartesian closed category from an ML theory, and vice versa. Finally, we show these constructions are inverse.”
Reviewer: M.Eytan

MSC:

03G30 Categorical logic, topoi
03B15 Higher-order logic; type theory (MSC2010)
03F99 Proof theory and constructive mathematics
18D30 Fibered categories
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] MacLane, Categories for the Working Mathematician (1971)
[2] Freyd, Bull. Australian Math. Soc 7 pp 1– (1972)
[3] Diller, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism pp 491– (1980)
[4] Seely, Mathematical Reports of the Academy of Science IV pp 271– (1982)
[5] Martin-L?f, Logic Colloquium pp 73– (1974)
[6] Prawitz, Proc. of the Second Scandinavian Logic Symposium pp 235– (1971) · doi:10.1016/S0049-237X(08)70849-8
[7] Seely, Zeitschrift f?r Math. Logik und Grundlagen der Math (1984)
[8] Prawitz, Natural Deduction: a Proof-theoretical Study (1965) · Zbl 0173.00205
[9] Par?, Indexed Categories and Their Applications (1978)
[10] Seely, McGill University Mathematics Report 82?22 (1982)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.