Document Open Access Logo

Models of Type Theory Based on Moore Paths

Authors Ian Orton, Andrew M. Pitts

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2017.28.pdf
  • Filesize: 0.58 MB
  • 16 pages

Document Identifiers

Author Details

Ian Orton
Andrew M. Pitts

Cite As Get BibTex

Ian Orton and Andrew M. Pitts. Models of Type Theory Based on Moore Paths. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 28:1-28:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.FSCD.2017.28

Abstract

This paper introduces a new family of models of intensional Martin-Löf type theory. We use constructive ordered algebra in toposes. Identity types in the models are given by a notion of Moore path. By considering a particular gros topos, we show that there is such a model that is non-truncated, i.e. contains non-trivial structure at all dimensions. In other words, in this model a type in a nested sequence of identity types can contain more than one element, no matter how great the degree of nesting. Although inspired by existing non-truncated models of type theory based on simplicial and on cubical sets, the notion of model presented here is notable for avoiding any form of Kan filling condition in the semantics of types.

Subject Classification

Keywords
  • dependent type theory
  • homotopy theory
  • Moore path
  • topos

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Agda. URL: http://wiki.portal.chalmers.se/agda/pmwiki.php.
  2. S. Awodey. Natural models of homotopy type theory. Mathematical Structures in Computer Science, [tba]:1-46, 2016. Google Scholar
  3. M. Bezem, T. Coquand, and S. Huber. A model of type theory in cubical sets. In Proc. TYPES 2013, volume 26 of LIPIcs, pages 107-128, 2014. Google Scholar
  4. N. Bourbaki. Algèbre, volume II of Eléments de mathématiques. Masson, 1981. Google Scholar
  5. R. Brown. Moore hyperrectangles on a space form a strict cubical omega-category. ArXiv e-prints, https://arxiv.org/abs/0909.2212, 2009.
  6. C. Cohen, T. Coquand, S. Huber, and A. Mörtberg. Cubical type theory: a constructive interpretation of the univalence axiom. ArXiv e-prints, https://arxiv.org/abs/1611.02108, 2016.
  7. T. Coquand, B. Mannaa, and F. Ruch. Stack semantics of type theory. ArXiv e-prints, https://arxiv.org/abs/arXiv:1701.02571v1, 2017.
  8. P. Dybjer. Internal type theory. In S. Berardi and M. Coppo, editors, Types for Proofs and Programs, volume 1158 of Lecture Notes in Computer Science, pages 120-134. Springer Berlin Heidelberg, 1996. Google Scholar
  9. E. Dyer and S. Eilenberg. Globalizing fibrations by schedules. Fundamenta Mathematicae, 130(2):125-136, 1988. Google Scholar
  10. A. Grothendieck and J. L. Verdier. Théorie des topos (SGA 4, exposés I-VI), volume 269-270 of Lecture Notes in Mathematics. Springer-Verlag, Berlin, 1972. Google Scholar
  11. M. Hofmann. Syntax and semantics of dependent types. In A. M. Pitts and P. Dybjer, editors, Semantics and Logics of Computation, pages 79-130. CUP, 1997. Google Scholar
  12. M. Hofmann and T. Streicher. Lifting Grothendieck universes. Unpublished note, 1999. Google Scholar
  13. P. T. Johnstone. On a topological topos. Proceedings of the London Mathematical Society, s3-38(2):237-271, 1979. Google Scholar
  14. P. T. Johnstone. Sketches of an Elephant, A Topos Theory Compendium, Volumes 1 and 2. Number 43-44 in Oxford Logic Guides. Oxford University Press, 2002. Google Scholar
  15. D. M. Kan. A combinatorial definition of homotopy groups. Annals of Mathematics, 67(2):282-312, 1958. Google Scholar
  16. M. M. Kapranov and V. A. Voevodsky. ∞-groupoids and homotopy types. Cahiers de Topologie et Géométrie Différentielle Catégoriques, 32(1):29-46, 1991. Google Scholar
  17. C. Kapulkin and P. L. Lumsdaine. The simplicial model of univalent foundations (after Voedodsky). ArXiv e-prints, https://arxiv.org/abs/arXiv:1211.2851v4, 2016.
  18. P. L. Lumsdaine and M. A. Warren. The local universes model: an overlooked coherence construction for dependent type theories. ACM Trans. Comput. Logic, 16(3):23:1-23:31, 2015. Google Scholar
  19. S. MacLane and I. Moerdijk. Sheaves in Geometry and Logic. A First Introduction to Topos Theory. Springer, 1992. Google Scholar
  20. M. E. Maietti. Modular correspondence between dependent type theories and categories including pretopoi and topoi. Math. Structures in Comp. Science, 15:1089-1149, 2005. Google Scholar
  21. P. Martin-Löf. An intuitionistic theory of types: Predicative part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium 1973, pages 73-118. North-Holland, 1975. Google Scholar
  22. P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984. Google Scholar
  23. I. Moerdijk and E. Palmgren. Wellfounded trees in categories. Annals of Pure and Applied Logic, 104(1):189-218, 2000. Google Scholar
  24. J. C. Moore. Le théorème de Freudenthal, la suite exacte de James et l'invariant de Hopf généralisé. Séminaire Henri Cartan, 7(2):exp. 22, 1-15, 1954-1955. Google Scholar
  25. P. R. North. Type Theoretic Weak Factorization Systems. PhD thesis, University of Cambridge, 2017. Google Scholar
  26. I. Orton and A. M. Pitts. Axioms for modelling cubical type theory in a topos. In Proc. CSL 2016, volume 62 of LIPIcs, pages 24:1-24:19, 2016. Google Scholar
  27. B. Spitters. Cubical sets and the topological topos. ArXiv e-prints, https://arxiv.org/abs/arXiv:1610.05270v1, 2016.
  28. The Stacks Project Authors. Stacks project. http://stacks.math.columbia.edu, 2017.
  29. T. Streicher. Universes in toposes. In L. Crosilla and P. Schuster, editors, From Sets and Types to Topology and Analysis, Towards Practicable Foundations for Constructive Mathematics, volume 48, chapter 4, pages 78-90. OUP, 2005. Google Scholar
  30. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations for Mathematics. Institute for Advanced Study, 2013. Google Scholar
  31. B. van den Berg. Path categories and propositional identity types. ArXiv e-prints, https://arxiv.org/abs/arXiv:1604.06001, 2016.
  32. B. van den Berg and R. Garner. Topological and simplicial models of identity types. ACM Trans. Comput. Logic, 13(1):3:1-3:44, 2012. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact