Benno van den Berg
Abstract
In this paper we construct new categorical models for the identity types of Martin-Löf type theory, in the categories Top of topological spaces and SSet of simplicial sets. We do so building on earlier work of Awodey and Warren [2009], which has suggested that a suitable environment for the interpretation of identity types should be a category equipped with a weak factorization system in the sense of Bousfield--Quillen. It turns out that this is not quite enough for a sound model, due to some subtle coherence issues concerned with stability under substitution; and so our first task is to introduce a slightly richer structure, which we call a homotopy-theoretic model of identity types, and to prove that this is sufficient for a sound interpretation.
Now, although both Top and SSet are categories endowed with a weak factorization system---and indeed, an entire Quillen model structure---exhibiting the additional structure required for a homotopy-theoretic model is quite hard to do. However, the categories we are interested in share a number of common features, and abstracting these leads us to introduce the notion of a path object category. This is a relatively simple axiomatic framework, which is nonetheless sufficiently strong to allow the construction of homotopy-theoretic models. Now by exhibiting suitable path object structures on Top and SSet, we endow those categories with the structure of a homotopy-theoretic model and, in this way, obtain the desired topological and simplicial models of identity types.
- Awodey, S. and Warren, M. 2009. Homotopy theoretic models of identity types. Math. Proc. Cambridge Phil. Soc. 146, 1, 45--55.Google Scholar
Cross Ref
- Bousfield, A. 1977. Constructions of factorization systems in categories. J. Pure Appl. Algebra 9, 2--3, 207--220.Google ScholarCross Ref
- Cartmell, J. 1986. Generalised algebraic theories and contextual categories. Ann. Pure Appl. Logic 32, 209--243.Google ScholarCross Ref
- Gambino, N. and Garner, R. 2008. The identity type weak factorization system. Theor. Comput. Sci. 409, 94--109. Google ScholarDigital Library
- Garner, R. 2009. Two-dimensional models of type theory. Math. Struct. Comput. Sci. 19, 4, 687--736. Google ScholarDigital Library
- Garner, R. and Berg, B. v. d. 2011. Types are weak ω-groupoids. Proc. London Math. Soc. 102, 2, 370--394.Google ScholarCross Ref
- Hofmann, M. 1995. On the interpretation of type theory in locally cartesian closed categories. In Proceedings of the 8th International Workshop on Computer Science Logic. Lecture Notes in Computer Science, vol. 933, Springer, 427--441. Google ScholarDigital Library
- Hofmann, M. and Streicher, T. 1998. The groupoid interpretation of type theory. In Twenty-Five Years of Constructive Type Theory. Oxford Logic Guides Series, vol. 36, Oxford University Press, 83--111.Google Scholar
- Hyland, J. M. 1982. The effective topos. In Proceedings of the L.E.J. Brouwer Centenary Symposium. Studies in Logic and the Foundations of Mathematics Series, vol. 110, North-Holland, 165--216.Google ScholarCross Ref
- Jacobs, B. 1993. Comprehension categories and the semantics of type dependency. Theor. Comput. Sci. 107, 2, 169--207. Google ScholarDigital Library
- Johnstone, P. 1997. Cartesian monads on toposes. J. Pure Appl. Algebra 116, 199--220.Google ScholarCross Ref
- Kock, A. 1970. Monads on symmetric monoidal closed categories. Archiv der Mathematik 21, 1, 1--10.Google ScholarCross Ref
- Lumsdaine, P. L. 2009. Weak ω-categories from intensional type theory. In Typed Lambda Calculi and Applications. Lecture Notes in Computer Science, vol. 5608, Springer. Google ScholarDigital Library
- Nordström, B., Petersson, K., and Smith, J. 1990. Programming in Martin-Löf’s Type Theory. International Series of Monographs on Computer Science Series, vol. 7, Oxford University Press.Google Scholar
- Pitts, A. M. 2000. Categorical logic. In Handbook of Logic in Computer Science, Vol. 5, Algebraic and Logical Structures, S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum Eds., Oxford University Press, 39--128. Google ScholarDigital Library
- Quillen, D. G. 1967. Homotopical Algebra. Lecture Notes in Mathematics Series, vol. 43, Springer-Verlag.Google ScholarCross Ref
- Rosický, J. and Tholen, W. 2002. Lax factorization algebras. J. Pure Appl. Algebra 175, 355--382.Google ScholarCross Ref
- Street, R. 1996. Categorical structures. In Handbook of Algebra, Vol. 1. North-Holland, 529--577.Google ScholarCross Ref
- Van Oosten, J. 2010. A notion of homotopy for the effective topos. http://www.staff.science.uu.nl/∼ooste110.Google Scholar
- Warren, M. 2008. Homotopy theoretic aspects of constructive type theory. Ph.D. thesis, Carnegie Mellon University.Google Scholar
- Warren, M. 2009. A characterization of representable intervals. http://arxiv.org/abs/0903.3743.Google Scholar
Index Terms
- Topological and Simplicial Models of Identity Types
Recommendations
The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories
We present a new coherence theorem for comprehension categories, providing strict models of dependent type theory with all standard constructors, including dependent products, dependent sums, identity types, and other inductive types.
Precisely, we take ...
Path Categories and Propositional Identity Types
Connections between homotopy theory and type theory have recently attracted a lot of attention, with Voevodsky’s univalent foundations and the interpretation of Martin-Löf’s identity types in Quillen model categories as some of the highlights. In this ...
The identity type weak factorisation system
We show that the classifying category C(T) of a dependent type theory T with axioms for identity types admits a non-trivial weak factorisation system. We provide an explicit characterisation of the elements of both the left class and the right class of ...
Reviews
Jacques Carette
There are times when some new theory comes along that just seems "right," regardless of whether one can immediately see applications. The link between homotopy theory and identity types in Martin-L?f type theory has convinced many (including me) that it is one of those theories. Unfortunately, it requires quite a lot of background (dependent type theory, homotopy theory, and category theory) to properly understand. Thankfully, the main idea is simple: not all identities between terms are the same, and some identities in particular may have more computational content than others. Statements more precise than this immediately get rather technical. Of course, such an idea might have turned out to be entirely fanciful, at least until models were found. While others broke that ground, the authors here present new models, in terms of topological spaces and simplicial sets. More importantly, they present a cogent categorical framework and a set of categorical tools that allow one to much more easily identify new models. The paper is extremely well written, especially considering the technical difficulty and depth of the material. The authors spend considerable time explaining the main ideas and intuitions, and even point out what their work does not achieve. One interesting technical aspect is the use of Moore paths in their topological models. Disappointingly, no reference is associated with this. I found the presentation of dependent type theory amusingly sloppy. If the authors had formalized all of their work in a proof assistant, like Coq, they surely would have chosen a different presentation of this material. Hopefully, one day formal papers will be written using formal tools. This paper is really written for experts, whereas I'm just a highly interested bystander with almost enough of the right background to follow what is going on. In fact, the biggest barrier is the notation, which is likely standard but is not fully explained. All experts should read this paper. Those looking for an introduction to the topic should look elsewhere before coming back to it. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments