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

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

Bibliographic References

11 Documents citing this article

Bruno Bentzen, 2021, Naive cubical type theory, PhilPapers (PhilPapers Foundation), 31, 10, pp. 1205-1231, 10.1017/s096012952200007x, https://philarchive.org/rec/BENNCT.

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, Algebra and applications, An Introduction to Higher Categories, pp. 3-16, 2019, 10.1007/978-3-030-05674-2_1.

Steve Awodey, Synthese Library/Synthese library, Mathesis Universalis and Homotopy Type Theory, pp. 13-36, 2019, 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/abs/1604.06001.

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, https://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, https://arxiv.org/abs/1402.0761.

Kristina Sojakova, arXiv (Cornell University), Higher Inductive Types as Homotopy-Initial Algebras, 2014, Mumbai India, 10.1145/2676726.2676983, https://arxiv.org/abs/1402.0761.

Á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.

Steven Awodey;Pieter J. W. 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, https://doi.org/10.1016/j.apal.2013.05.001.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1794 times.

This article's PDF has been downloaded 509 times.