{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T06:19:53Z","timestamp":1772518793385,"version":"3.50.1"},"reference-count":15,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2010,9,17]],"date-time":"2010-09-17T00:00:00Z","timestamp":1284681600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We show that for any type in Martin-L\\\"of Intensional Type Theory, the terms\nof that type and its higher identity types form a weak omega-category in the\nsense of Leinster. Precisely, we construct a contractible globular operad of\ndefinable composition laws, and give an action of this operad on the terms of\nany type and its identity types.<\/jats:p>","DOI":"10.2168\/lmcs-6(3:24)2010","type":"journal-article","created":{"date-parts":[[2010,11,26]],"date-time":"2010-11-26T21:17:19Z","timestamp":1290806239000},"source":"Crossref","is-referenced-by-count":11,"title":["Weak omega-categories from intensional type theory"],"prefix":"10.46298","volume":"Volume 6, Issue 3","author":[{"given":"Peter LeFanu","family":"Lumsdaine","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2010,9,17]]},"reference":[{"key":"10.2168\/LMCS-6(3:24)2010_awodey-warren","unstructured":"Steve Awodey and Michael A. Warren, Homotopy theoretic models of identity types, Math. Proc. Cambridge Philos. Soc. \\textbf146 (2009), no. 1, 45-55. MR2461866"},{"issue":"1","key":"10.2168\/LMCS-6(3:24)2010_batanin:natural-environment","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1006\/aima.1998.1724","volume":"136","author":"M. A. Batanin","year":"1998","journal-title":"Adv. Math."},{"issue":"3","key":"10.2168\/LMCS-6(3:24)2010_cartmell:generalised-algebraic-theories","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/0168-0072(86)90053-9","volume":"32","author":"John Cartmell","year":"1986","journal-title":"Ann. Pure Appl. Logic"},{"issue":"4","key":"10.2168\/LMCS-6(3:24)2010_cheng:duals-give-inverses","doi-asserted-by":"crossref","first-page":"439","DOI":"10.1007\/s10485-007-9081-8","volume":"15","author":"Eugenia Cheng","year":"2007","journal-title":"Appl. Categ. Structures"},{"key":"10.2168\/LMCS-6(3:24)2010_garner:homomorphisms","unstructured":"Richard Garner, Homomorphisms of higher categories, submitted, 2008."},{"issue":"4","key":"10.2168\/LMCS-6(3:24)2010_garner:2-d-models","doi-asserted-by":"crossref","first-page":"687","DOI":"10.1017\/S0960129509007646","volume":"19","author":"Richard Garner","year":"2009","journal-title":"Math. Structures Comput."},{"issue":"1","key":"10.2168\/LMCS-6(3:24)2010_gambino-garner","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1016\/j.tcs.2008.08.030","volume":"409","author":"Nicola Gambino and Richard Garner","year":"2008","journal-title":"system, Theoret. Comput. Sci."},{"key":"10.2168\/LMCS-6(3:24)2010_benno-richard","unstructured":"Richard Garner and Benno van den Berg, Types are weak\u03c9-groupoids, submitted, 2008."},{"key":"10.2168\/LMCS-6(3:24)2010_hofmann-streicher","doi-asserted-by":"crossref","unstructured":"Martin Hofmann and Thomas Streicher, The groupoid interpretation of type theory, Twenty-five years of constructive type theory (Venice, 1995), Oxford Logic Guides, vol. 36, Oxford Univ. Press, New York, 1998, pp. 83-111.","DOI":"10.1093\/oso\/9780198501275.003.0008"},{"key":"10.2168\/LMCS-6(3:24)2010_jacobs:categorical-logic","unstructured":"Bart Jacobs, Categorical logic and type theory, Studies in Logic and the Foundations of Mathematics, vol. 141, North-Holland Publishing Co., Amsterdam, 1999."},{"key":"10.2168\/LMCS-6(3:24)2010_leinster:survey","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1013377004339","volume":"10","author":"Tom Leinster","year":"2002","journal-title":"Theory Appl. Categ."},{"key":"10.2168\/LMCS-6(3:24)2010_leinster:book","doi-asserted-by":"crossref","unstructured":"Tom Leinster, Higher operads, higher categories, London Mathematical Society Lecture Note Series, vol. 298, Cambridge University Press, Cambridge, 2004.","DOI":"10.1017\/CBO9780511525896"},{"key":"10.2168\/LMCS-6(3:24)2010_street:petit-topos","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1016\/S0022-4049(99)00183-8","volume":"154","author":"Ross Street","year":"2000","journal-title":"Journal of Pure and Applied Algebra"},{"key":"10.2168\/LMCS-6(3:24)2010_benno:talk","unstructured":"Benno van den Berg, Types as weak\u03c9-categories, Lecture delivered in Uppsala, 2006, and unpublished notes."},{"key":"10.2168\/LMCS-6(3:24)2010_warren:thesis","unstructured":"Michael A. Warren, Homotopy theoretic aspects of constructive type theory, Ph.D. thesis, Carnegie Mellon University, 2008."}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1062\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1062\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:02:21Z","timestamp":1681243341000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1062"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,9,17]]},"references-count":15,"URL":"https:\/\/doi.org\/10.2168\/lmcs-6(3:24)2010","relation":{"is-same-as":[{"id-type":"arxiv","id":"0812.0409","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.0812.0409","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,9,17]]},"article-number":"1062"}}