{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:16:19Z","timestamp":1750220179521,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":18,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,8,2]],"date-time":"2022-08-02T00:00:00Z","timestamp":1659398400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,8,2]]},"DOI":"10.1145\/3531130.3533363","type":"proceedings-article","created":{"date-parts":[[2022,8,4]],"date-time":"2022-08-04T20:23:38Z","timestamp":1659644618000},"page":"1-12","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["A Type Theory for Strictly Unital \u221e-Categories"],"prefix":"10.1145","author":[{"given":"Eric","family":"Finster","sequence":"first","affiliation":[{"name":"University of Birmingham, United Kingdom"}]},{"given":"David","family":"Reutter","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Hamburg, Germany"}]},{"given":"Jamie","family":"Vicary","sequence":"additional","affiliation":[{"name":"University of Cambridge, United Kingdom"}]},{"given":"Alex","family":"Rice","sequence":"additional","affiliation":[{"name":"University of Cambridge, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2022,8,4]]},"reference":[{"volume-title":"New Structures for Physics","author":"Baez John","key":"e_1_3_2_1_2_1","unstructured":"John Baez and Mike Stay . 2010. Physics, topology, logic and computation: a Rosetta Stone . In New Structures for Physics . Springer , 95\u2013172. https:\/\/doi.org\/10.1007\/978-3-642-12821-9_2 arXiv:0903.0340 10.1007\/978-3-642-12821-9_2 John Baez and Mike Stay. 2010. Physics, topology, logic and computation: a Rosetta Stone. In New Structures for Physics. Springer, 95\u2013172. https:\/\/doi.org\/10.1007\/978-3-642-12821-9_2 arXiv:0903.0340"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1006\/aima.1998.1724"},{"key":"e_1_3_2_1_4_1","first-page":"804","article-title":"Multitensor lifting and strictly unital higher category theory","volume":"28","author":"Batanin Michael","year":"2013","unstructured":"Michael Batanin , Denis-Charles Cisinski , and Mark Weber . 2013 . Multitensor lifting and strictly unital higher category theory . Theory and Applications of Categories 28 (2013), 804 \u2013 856 . arXiv:1209.2776 Michael Batanin, Denis-Charles Cisinski, and Mark Weber. 2013. Multitensor lifting and strictly unital higher category theory. Theory and Applications of Categories 28 (2013), 804\u2013856. arXiv:1209.2776","journal-title":"Theory and Applications of Categories"},{"volume-title":"Homotopy invariant algebraic structures on topological spaces. Vol.\u00a0347","author":"Boardman John\u00a0Michael","key":"e_1_3_2_1_6_1","unstructured":"John\u00a0Michael Boardman and Rainer\u00a0 M Vogt . 1973. Homotopy invariant algebraic structures on topological spaces. Vol.\u00a0347 . Springer . https:\/\/doi.org\/10.1007\/bfb0068547 10.1007\/bfb0068547 John\u00a0Michael Boardman and Rainer\u00a0M Vogt. 1973. Homotopy invariant algebraic structures on topological spaces. Vol.\u00a0347. Springer. https:\/\/doi.org\/10.1007\/bfb0068547"},{"key":"e_1_3_2_1_7_1","unstructured":"Guillaume Brunerie. 2016. On the homotopy groups of spheres in homotopy type theory. (2016). arXiv:1606.05916  Guillaume Brunerie. 2016. On the homotopy groups of spheres in homotopy type theory. (2016). arXiv:1606.05916"},{"key":"#cr-split#-e_1_3_2_1_8_1.1","unstructured":"Cyril Cohen Thierry Coquand Simon Huber and Anders M\u00f6rtberg. 2018. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015)(Leibniz International Proceedings in Informatics (LIPIcs) Vol.\u00a069) Tarmo Uustalu (Ed.). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik Dagstuhl Germany 5:1-5:34. https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2015.5 arXiv:1611.02108 10.4230\/LIPIcs.TYPES.2015.5"},{"key":"#cr-split#-e_1_3_2_1_8_1.2","unstructured":"Cyril Cohen Thierry Coquand Simon Huber and Anders M\u00f6rtberg. 2018. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015)(Leibniz International Proceedings in Informatics (LIPIcs) Vol.\u00a069) Tarmo Uustalu (Ed.). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik Dagstuhl Germany 5:1-5:34. https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2015.5 arXiv:1611.02108"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005124"},{"key":"e_1_3_2_1_10_1","volume-title":"Power, and Ross Street","author":"Gordon R.","year":"1995","unstructured":"R. Gordon , A.\u00a0 J. Power, and Ross Street . 1995 . Coherence for tricategories. Mem. Amer. Math. Soc . 117, 558 (1995), vi+81. https:\/\/doi.org\/10.1090\/memo\/0558 10.1090\/memo R. Gordon, A.\u00a0J. Power, and Ross Street. 1995. Coherence for tricategories. Mem. Amer. Math. Soc. 117, 558 (1995), vi+81. https:\/\/doi.org\/10.1090\/memo\/0558"},{"key":"e_1_3_2_1_11_1","volume-title":"The groupoid interpretation of type theory. Twenty-five years of constructive type theory (Venice","author":"Hofmann Martin","year":"1995","unstructured":"Martin Hofmann and Thomas Streicher . 1998. The groupoid interpretation of type theory. Twenty-five years of constructive type theory (Venice , 1995 ) 36 (1998), 83\u2013111. https:\/\/doi.org\/10.1093\/oso\/9780198501275.003.0008 10.1093\/oso Martin Hofmann and Thomas Streicher. 1998. The groupoid interpretation of type theory. Twenty-five years of constructive type theory (Venice, 1995) 36 (1998), 83\u2013111. https:\/\/doi.org\/10.1093\/oso\/9780198501275.003.0008"},{"key":"e_1_3_2_1_12_1","volume-title":"Automata and computability","author":"Kozen C","year":"1844","unstructured":"Dexter\u00a0 C Kozen . 1997. Automata and computability . Springer Science & Business Media . arXiv:10.1007\/978-1-4612- 1844 -9 Dexter\u00a0C Kozen. 1997. Automata and computability. Springer Science & Business Media. arXiv:10.1007\/978-1-4612-1844-9"},{"volume-title":"Higher operads, higher categories","author":"Leinster Tom","key":"e_1_3_2_1_13_1","unstructured":"Tom Leinster . 2004. Higher operads, higher categories . London Mathematical Society Lecture Note Series, Vol .\u00a0298. Cambridge University Press , Cambridge. xiv+433 pages. https:\/\/doi.org\/10.1017\/CBO9780511525896 arXiv:math\/0305049 10.1017\/CBO9780511525896 Tom Leinster. 2004. Higher operads, higher categories. London Mathematical Society Lecture Note Series, Vol.\u00a0298. Cambridge University Press, Cambridge. xiv+433 pages. https:\/\/doi.org\/10.1017\/CBO9780511525896 arXiv:math\/0305049"},{"volume-title":"Higher topos theory","author":"Lurie Jacob","key":"e_1_3_2_1_14_1","unstructured":"Jacob Lurie . 2009. Higher topos theory . Princeton University Press . https:\/\/doi.org\/10.1515\/9781400830558 arXiv:math\/0608040 10.1515\/9781400830558 Jacob Lurie. 2009. Higher topos theory. Princeton University Press. https:\/\/doi.org\/10.1515\/9781400830558 arXiv:math\/0608040"},{"volume-title":"Categories for the working mathematician. Vol.\u00a05","author":"Mac\u00a0Lane Saunders","key":"e_1_3_2_1_15_1","unstructured":"Saunders Mac\u00a0Lane . 1971. Categories for the working mathematician. Vol.\u00a05 . Springer Science & Business Media . https:\/\/doi.org\/10.1007\/978-1-4612-9839-7 10.1007\/978-1-4612-9839-7 Saunders Mac\u00a0Lane. 1971. Categories for the working mathematician. Vol.\u00a05. Springer Science & Business Media. https:\/\/doi.org\/10.1007\/978-1-4612-9839-7"},{"key":"e_1_3_2_1_16_1","volume-title":"arXiv:1009.2331","author":"Maltsiniotis Georges","year":"2010","unstructured":"Georges Maltsiniotis . 2010. Grothendieck \u221e-groupoids, and still another definition of \u221e-categories. ( 2010 ). arXiv:1009.2331 Georges Maltsiniotis. 2010. Grothendieck \u221e-groupoids, and still another definition of \u221e-categories. (2010). arXiv:1009.2331"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533347"},{"volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics. Homotopy Type Theory","author":"Foundations Program The Univalent","key":"e_1_3_2_1_18_1","unstructured":"The Univalent Foundations Program . 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Homotopy Type Theory , Institute for Advanced Study . The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Homotopy Type Theory, Institute for Advanced Study."},{"volume-title":"Elements of homotopy theory. Vol.\u00a061","author":"Whitehead W","key":"e_1_3_2_1_19_1","unstructured":"George\u00a0 W Whitehead . 2012. Elements of homotopy theory. Vol.\u00a061 . Springer Science & Business Media . https:\/\/doi.org\/10.1007\/978-1-4612-6318-0 10.1007\/978-1-4612-6318-0 George\u00a0W Whitehead. 2012. Elements of homotopy theory. Vol.\u00a061. Springer Science & Business Media. https:\/\/doi.org\/10.1007\/978-1-4612-6318-0"}],"event":{"name":"LICS '22: 37th Annual ACM\/IEEE Symposium on Logic in Computer Science","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"Haifa Israel","acronym":"LICS '22"},"container-title":["Proceedings of the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3531130.3533363","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3531130.3533363","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:10Z","timestamp":1750186930000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3531130.3533363"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,2]]},"references-count":18,"alternative-id":["10.1145\/3531130.3533363","10.1145\/3531130"],"URL":"https:\/\/doi.org\/10.1145\/3531130.3533363","relation":{},"subject":[],"published":{"date-parts":[[2022,8,2]]},"assertion":[{"value":"2022-08-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}