Abstract
In the paper there are introduced and discussed the concepts of an indexed category with quantifications and a higher level indexed category to present an algebraic characterization of some version of Martin-Löf Type Theory. This characterization is given by specifying an additional equational structure of those indexed categories which are models of Martin-Löf Type Theory. One can consider the presented characterization as an essentially algebraic theory of categorical models of Martin-Löf Type Theory. The paper contains a construction of an indexed category with quantifications from terms and types of the language of Martin-Löf Type Theory given in the manner of Troelstra [11]. The paper contains also an inductive definition of a valuation of these terms and types in an indexed category with quantifications.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
M. Beeson, Recursive models for constructive set theory, Annals of Mathematical Logic 23 (1982), pp. 127–178.
J. Cartmell, Generalized algebraic theories and contextual categories, Annals of Pure and Applied Logic 32 (1986), pp. 209–243.
J. Diller, Modified realization and the formulae-as-types notion, in To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. P. Seldin and J. R. Hindley (eds.), Academic Press, London, 1980.
P. Freyd, Aspects of Topoi, Bulletin of the Australian Mathematical Society 7 (1972), pp. 1–76.
G. Huet, Formal structure for computation and deduction, Notes for graduate-level course given in the Computer Science Department, Carnegie-Mellon University during the Spring 1986.
J. Lambek and P.J. Scott, Introduction to Higher Order Categorial Logic, Cambridge University Press, Cambridge, 1986.
S. Mac Lane, Categories for the Working Mathematician, Springer Verlag, New York, 1971.
P. Martin-Löf, Constructive mathematics and computer programming, in Logic, Méthodology and Philosophy of Science VI, L. J. Cohen, et. al. (eds.), North-Holland, Amsterdam, 1982, pp. 153–175.
R. Pare and D. Schumacher, Abstract families and the adjoint functor theorems, in Indexed Categories and Their Applications, Lecture Notes in Mathematics Vol. 661, 1978, pp. 1–124.
R. A. G. Seely, Locally cartesian closed categories and type theory, Mathematical Proceedings of Càmbridge Philosophical Society 95 (1984), pp. 33–48.
A. Troelstra, On the syntax of Martin-Löf theories, Theoretical Computer Science 51, no. 1, 2 (1987), pp. 1–26.
P. Taylor, Recursive domains, indexed category theory and polymorphism, Dissertation, Cambridge University, 1986.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Obtułowicz, A. Categorical and algebraic aspects of Martin-Löf Type Theory. Stud Logica 48, 299–317 (1989). https://doi.org/10.1007/BF00370827
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00370827