×
Curien, Pierre-Louis; Garner, Richard; Hofmann, Martin

Revisiting the categorical interpretation of dependent type theory. (English) Zbl 1433.03029

Theor. Comput. Sci. 546, 99-119 (2014).
Summary: We show that Hofmann’s and Curien’s interpretations of Martin-Löf’s type theory, which were both designed to cure a mismatch between syntax and semantics in Seely’s original interpretation in locally Cartesian closed categories, are related via a natural isomorphism. As an outcome, we obtain a new proof of the coherence theorem needed to show the soundness after all of Seely’s interpretation.

Cited in 10 Documents

MSC:

03B38 Type theory
18D15 Closed categories (closed monoidal and Cartesian closed categories, etc.)

Keywords:

type theory; categorical semantics; dependent types; monoidal categories; locally Cartesian closed categories; Grothendieck fibrations; coherence
Cite Review PDF
Full Text: DOI

References:

[1] Awodey, S.; Warren, M., Homotopy theoretic models of identity types, Math. Proc. Cambridge Philos. Soc., 146, 45-55 (2009) · Zbl 1205.03065
[3] Blackwell, R.; Kelly, G. M.; Power, A. J., Two-dimensional monad theory, J. Pure Appl. Algebra, 59, 289-319 (1989) · Zbl 0675.18006
[4] Beylin, I.; Dybjer, P., Extracting a proof of coherence for monoidal categories from a formal proof of normalization for monoids, (Proc. TYPES’95. Proc. TYPES’95, Lecture Notes in Computer Science, vol. 1158 (1996)), 47-61 · Zbl 1407.68432
[5] Cartmell, J., Generalised algebraic theories and contextual categories (1978), Oxford University, PhD thesis
[6] Clairambault, P.; Dybjer, P., The biequivalence of locally cartesian closed categories and Martin-Löf type theory, (Proceedings TLCA 2011. Proceedings TLCA 2011, Lecture Notes in Computer Science, vol. 6690 (2011)), 91-106 · Zbl 1331.03045
[7] Curien, P.-L., Substitution up to isomorphism, Fund. Inform., 19, 51-85 (1993), (preliminary version appeared as LIENS Technical report 90-9, 1990) · Zbl 0806.03043
[8] Dybjer, P., Internal type theory, (Proc. TYPES’95. Proc. TYPES’95, Lecture Notes in Computer Science, vol. 1158 (1996)), 120-134 · Zbl 1434.03149
[9] Freyd, P., Aspects of topoi, Bull. Aust. Math. Soc., 7 (1972) · Zbl 0252.18001
[10] Garner, R.; Gambino, N., The identity type weak factorisation system, Theoret. Comput. Sci., 409, 1, 94-109 (2008) · Zbl 1157.68022
[11] Giraud, J., Cohomologie non Abélienne (1971), Springer · Zbl 0135.02401
[12] Hofmann, M., On the interpretation of type theory in locally cartesian closed categories, (Proc. Computer Science Logic. Proc. Computer Science Logic, CSL’94. Proc. Computer Science Logic. Proc. Computer Science Logic, CSL’94, Lecture Notes in Computer Science, vol. 933 (1994)), 427-441 · Zbl 1044.03544
[13] Hofmann, M., Syntax and semantics of dependent types, (Semantics and Logics of Computation (1997), Cambridge University Press), 79-130 · Zbl 0919.68083
[14] Huet, G., Initiation à la théorie des catégories (1985), notes de cours
[15] Jacobs, B., Categorical type theory (1991), Nijmegen, PhD thesis
[16] Jacobs, B., Comprehension categories and the semantics of type theory, Theoret. Comput. Sci., 107, 169-207 (1993) · Zbl 0804.18007
[17] Jacobs, B., Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics (1999), Elsevier · Zbl 0911.03001
[18] Joyal, A.; Street, R., Braided monoidal categories, Adv. Math., 102, 1, 20-78 (1993) · Zbl 0817.18007
[19] Leinster, T., Higher Operads, Higher Categories (2004), Cambridge University Press · Zbl 1160.18001
[21] Mac Lane, S., Categories for the Working Mathematician (1971), Springer · Zbl 0232.18001
[22] Nordström, B.; Peterson, K.; Smith, J. M., Programming in Martin-Löf’s Type Theory: An Introduction (1990), Oxford Science Publ. · Zbl 0744.03029
[23] Seely, R., Locally cartesian closed categories and type theory, Math. Proc. Cambridge Philos. Soc., 95, 33-48 (1984) · Zbl 0539.03048
[24] Voevodsky, V., Notes on type systems (2012), available from:
[25] Warren, M., Homotopy theoretic aspects of constructive type theory (2008), Carnegie Mellon University, PhD thesis
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.