Abstract
We show how to construct a model of dependent type theory (category with attributes) from a locally cartesian closed category (lccc). This allows to define a semantic function interpreting the syntax of type theory in an lccc. We sketch an application which gives rise to an interpretation of extensional type theory in intensional type theory.
The author is supported by a European Union HCM fellowship; contract number ERBCHBICT930420
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Michael Barr and Charles Wells. Category Theory for Computing Science. International Series in Computer Science. Prentice Hall, 1990.
J. Bénabou. Fibred categories and the foundations of naive category theory. Journal of Symbolic Logic, 50:10–37, 1985.
A. Carboni. Some free constructions in realizability and proof theory. Journal of Pure and Applied Algebra, to appear.
J. Cartmell. Generalized algebraic theories and contextual categories. PhD thesis, Univ. Oxford, 1978.
Pierre-Louis Curien. Substitution up to isomorphism. Fundamenta Informaticae, 19:51–86, 1993.
Thomas Ehrhard. Dictoses. In Proc. Conf. Category Theory and Computer Science, Manchester, UK, pages 213–223. Springer LNCS vol. 389, 1989.
Bart Jacobs. Categorical Type Theory. PhD thesis, University of Nijmegen, 1991.
Bart Jacobs. Comprehension categories and the semantics of type theory. Theoretical Computer Science, 107:169–207, 1993.
Nax P. Mendler. Quotient types via coequalisers in Martin-Löf's type theory. in the informal proceedings of the workshop on Logical Frameworks, Antibes, May 1990.
B. Nordström, K. Petersson, and J. M. Smith. Programming in Martin-Löf's Type Theory, An Introduction. Clarendon Press, Oxford, 1990.
Wesley Phoa. An introduction to fibrations, topos theory, the effective topos, and modest sets. Technical Report ECS-LFCS-92-208, LFCS Edinburgh, 1992.
Andrew Pitts. Categorical logic. In Handbook of Logic in Computer Science (Vol. VI). Oxford University Press, 199? to appear.
A. J. Power. A general coherence result. Journal of Pure and Applied Algebra, 57:165–173, 1989.
Robert A. G. Seely. Locally cartesian closed categories and type theory. Mathematical Proceedings of the Cambridge Philosophical Society, 95:33–48, 1984.
Thomas Streicher. Semantics of Type Theory. Birkhäuser, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hofmann, M. (1995). On the interpretation of type theory in locally cartesian closed categories. In: Pacholski, L., Tiuryn, J. (eds) Computer Science Logic. CSL 1994. Lecture Notes in Computer Science, vol 933. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0022273
Download citation
DOI: https://doi.org/10.1007/BFb0022273
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60017-6
Online ISBN: 978-3-540-49404-1
eBook Packages: Springer Book Archive