Hostname: page-component-5cf477f64f-tgq86 Total loading time: 0 Render date: 2025-04-06T18:33:53.063Z Has data issue: false hasContentIssue false
  • English
  • Français

W-types in homotopy type theory

Published online by Cambridge University Press:  24 November 2014

BENNO VAN DEN BERG  and
IEKE MOERDIJK
BENNO VAN DEN BERG
Affiliation:
ILLC, Universiteit van Amsterdam, P.O. Box 94242, 1090 GE Amsterdam, the Netherlands Email: [email protected]
IEKE MOERDIJK
Affiliation:
Radboud Universiteit Nijmegen, Institute for Mathematics, Astrophysics, and Particle Physics, Heyendaalseweg 135, 6525 AJ Nijmegen, the Netherlands Email: [email protected].
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We will give a detailed account of why the simplicial sets model of the univalence axiom due to Voevodsky also models W-types. In addition, we will discuss W-types in categories of simplicial presheaves and an application to models of set theory.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 25 , Special Issue 5: From type theory and homotopy theory to Univalent Foundations of Mathematics , June 2015 , pp. 1100 - 1115
Copyright
Copyright © Cambridge University Press 2014 

References

Abbott, M., Altenkirch, T. and Ghani, N. (2005) Containers: constructing strictly positive types. Theoretical Computer Science 342 (1) 3–27.Google Scholar
Aczel, P. (1978) The type theoretic interpretation of constructive set theory. In: Logic Colloquium'77 (Proceeding Conference, Wrocław, 1977). Studies in Logic and the Foundations of Mathematics 96 55–66. (North-Holland Publishing Co., Amsterdam)Google Scholar
Aczel, P. (1988) Non-Well-Founded Sets, CSLI Lecture Notes volume 14, CSLI Publications, Stanford, CA.Google Scholar
van den Berg, B. and De Marchi, F. (2007a) Models of non-well-founded sets via an indexed final coalgebra theorem. Journal Symbolic Logic 72 (3) 767–791.Google Scholar
van den Berg, B. and De Marchi, F. (2007b) Non-well-founded trees in categories. Annals of Pure and Applied Logic 146 (1) 40–59.Google Scholar
Berger, C. and Moerdijk, I. (2011) On an extension of the notion of Reedy category. Mathematische Zeitschrift 269 (3–4) 977–1004.Google Scholar
Bergner, J. E. and Rezk, C. (2013) Reedy categories and the Θ-construction. Mathematische Zeitschrift 274 (1–2) 499–514.Google Scholar
Blass, A. (1983) Words, free algebras, and coequalizers. Fundamenta Mathematicae, 117 (2) 117–160.Google Scholar
Carboni, A. (1995) Some free constructions in realizability and proof theory. Journal of Pure and Applied Algebra 103 117–148.Google Scholar
Carboni, A. and Celia Magno, R. (1982) The free exact category on a left exact one. Journal of the Australian Mathematical Society 33 295–301.Google Scholar
Cisinski, D.-C. and Moerdijk, I. (2013) Dendroidal Segal spaces and ∞-operads. Journal of Topology 6 (3) 675–704.CrossRefGoogle Scholar
Gambino, N. and Hyland, J. M. E. (2004) Wellfounded trees and dependent polynomial functors. In: Types for proofs and programs. Springer-Verlag Lecture Notes in Computer Science 3085 210–225.Google Scholar
Goerss, P. G. and Jardine, J. F. (1999) In: Simplicial Homotopy Theory, Progress in Mathematics volume 174, Birkhäuser Verlag, Basel.CrossRefGoogle Scholar
Kapulkin, C., Lumsdaine, P. L. and Voevodsky, V. (2012) The simplicial model of univalent foundations. arXiv:1211.2851.Google Scholar
Lindström, I. (1989) A construction of non-well-founded sets within Martin-Löf's type theory. Journal of Symbolic Logic, 54 (1) 57–64.Google Scholar
Martin-Löf, P. (1984) In: Intuitionistic Type Theory, Studies in Proof Theory. Lecture Notes volume 1, Bibliopolis, Naples.Google Scholar
Moerdijk, I. and Palmgren, E. (2000) Wellfounded trees in categories. Annals of Pure and Applied Logic 104 189–218.Google Scholar
Moerdijk, I. and Palmgren, E. (2002) Type theories, toposes and constructive set theory: Predicative aspects of AST. Annals of Pure and Applied Logic 114 155–201.Google Scholar
Paré, R. and Schumacher, D. (1978) Abstract families and the adjoint functor theorems. In: Indexed Categories and their Applications, Lecture Notes in Mathematics volume 661, Springer-Verlag, Berlin 1–125.Google Scholar
Petersson, K. and Synek, D. (1989) A set constructor for inductive sets in Martin-Löf's type theory. In: Category Theory and Computer Science (Manchester, 1989). Springer Lecture Notes in Computer Science 389 128–140.Google Scholar
Quillen, D. G. (1967) Homotopical Algebra, Lecture Notes in Mathematics volume 43, Springer-Verlag, Berlin.Google Scholar
Quillen, D. G.(1968) The geometric realization of a Kan fibration is a Serre fibration. Proceedings of the American Mathematical Society 19 1499–1500.CrossRefGoogle Scholar
Quillen, D. G. (1969) Rational homotopy theory. Annals of Mathematics 90 (2) 205–295.Google Scholar
Segal, G. (1974) Categories and cohomology theories. Topology 13 293–312.Google Scholar
Shulman, M. (2013a) The univalence axiom for elegant Reedy presheaves. arXiv:1307.6248.Google Scholar
Shulman, M. (2013b) Univalence for inverse diagrams and homotopy canonicity. arXiv:103.3253.CrossRefGoogle Scholar
Voevodsky, V. (2011) Notes on type systems. Available at http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html.Google Scholar