Weak omega-categories from intensional type theory

Peter LeFanu Lumsdaine

doi:10.2168/LMCS-6(3:24)2010

Peter LeFanu Lumsdaine - Weak omega-categories from intensional type theory

lmcs:1062 - Logical Methods in Computer Science, September 17, 2010, Volume 6, Issue 3 - https://doi.org/10.2168/LMCS-6(3:24)2010

Weak omega-categories from intensional type theoryArticle

Authors: Peter LeFanu Lumsdaine

We show that for any type in Martin-Löf Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. Precisely, we construct a contractible globular operad of definable composition laws, and give an action of this operad on the terms of any type and its identity types.

https://doi.org/10.2168/LMCS-6(3:24)2010

Source: arXiv.org:0812.0409

Volume: Volume 6, Issue 3

Secondary volumes: Selected Papers of the 9th Conference on Typed Lambda Calculi and Applications (TLCA 2009)

Published on: September 17, 2010

Imported on: December 1, 2009

Keywords: Mathematics - Logic, Mathematics - Category Theory, math.CT

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Publications

Has review

Review available on zbMATH Open, by Serguei V. Solov'ev (Toulouse) (English)

1 zbMATH Open

Bibliographic References

12 Documents citing this article

DAVID JAZ MYERS;ZYAD YASSER, 2025, HIGHER SCHREIER THEORY IN CUBICAL AGDA, Journal of Symbolic Logic, pp. 1-17, 10.1017/jsl.2024.78, https://doi.org/10.1017/jsl.2024.78.

Bruno Bentzen, 2021, Naive cubical type theory, arXiv (Cornell University), 31, 10, pp. 1205-1231, 10.1017/s096012952200007x, http://arxiv.org/abs/1911.05844.

Matthieu Sozeau;Cyprien Mangin, 2019, Equations reloaded: high-level dependently-typed functional programming and proving in Coq, Proceedings of the ACM on Programming Languages, 3, ICFP, pp. 1-29, 10.1145/3341690, https://doi.org/10.1145/3341690.

Simona Paoli, 2019, An Introduction to Higher Categories, Algebra and applications, pp. 3-16, 10.1007/978-3-030-05674-2_1.

Steve Awodey, 2019, Mathesis Universalis and Homotopy Type Theory, Synthese Library/Synthese library, pp. 13-36, 10.1007/978-3-030-20447-1_3.

Benno Van Den Berg, 2018, Path Categories and Propositional Identity Types, arXiv (Cornell University), 19, 2, pp. 1-32, 10.1145/3204492, https://arxiv.org/pdf/1604.06001.pdf.

DAN FRUMIN;BENNO VAN DEN BERG, 2018, A homotopy-theoretic model of function extensionality in the effective topos, Data Archiving and Networked Services (DANS), 29, 4, pp. 588-614, 10.1017/s0960129518000142, http://hdl.handle.net/2066/201798.

David Gepner;Joachim Kock, 2016, Univalence in locally cartesian closed ∞-categories, Forum Mathematicum, 29, 3, pp. 617-652, 10.1515/forum-2015-0228.

Kristina Sojakova, 2015, Higher Inductive Types as Homotopy-Initial Algebras, arXiv (Cornell University), 50, 1, pp. 31-42, 10.1145/2775051.2676983, http://arxiv.org/abs/1402.0761.

Kristina Sojakova, 2014, Higher Inductive Types as Homotopy-Initial Algebras, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 31-42, 10.1145/2676726.2676983.

Álvaro Pelayo;Michael Warren, 2014, Homotopy type theory and Voevodsky’s univalent foundations, Bulletin of the American Mathematical Society, 51, 4, pp. 597-648, 10.1090/s0273-0979-2014-01456-9, https://doi.org/10.1090/s0273-0979-2014-01456-9.

Steve Awodey;Pieter Hofstra;Michael A. Warren, 2013, Martin-Löf complexes, Annals of Pure and Applied Logic, 164, 10, pp. 928-956, 10.1016/j.apal.2013.05.001.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3619 times.

This article's PDF has been downloaded 706 times.