{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:16:18Z","timestamp":1750220178719,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":23,"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.3533347","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":2,"title":["Syllepsis in Homotopy Type Theory"],"prefix":"10.1145","author":[{"given":"Kristina","family":"Sojakova","sequence":"first","affiliation":[{"name":"Prosecco, Inria Paris, France"}]},{"given":"G. A.","family":"Kavvos","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Bristol, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2022,8,4]]},"reference":[{"volume-title":"Introduction to Homotopy Theory","author":"Arkowitz Martin","key":"e_1_3_2_1_1_1","unstructured":"Martin Arkowitz . 2011. Introduction to Homotopy Theory . Springer New York , New York, NY . https:\/\/doi.org\/10.1007\/978-1-4419-7329-0 10.1007\/978-1-4419-7329-0 Martin Arkowitz. 2011. Introduction to Homotopy Theory. Springer New York, New York, NY. https:\/\/doi.org\/10.1007\/978-1-4419-7329-0"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004108001783"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.531236"},{"key":"e_1_3_2_1_4_1","volume-title":"Baez and Michael Shulman","author":"C.","year":"2010","unstructured":"John\u00a0 C. Baez and Michael Shulman . 2010 . Lectures on n-Categories and Cohomology. In Towards Higher Categories, John\u00a0C. Baez and J.\u00a0Peter May (Eds.). The IMA Volumes in Mathematics and its Applications, Vol.\u00a0152. Springer New York , New York, NY, 1\u201368. https:\/\/doi.org\/10.1007\/978-1-4419-1524-5_1 10.1007\/978-1-4419-1524-5_1 John\u00a0C. Baez and Michael Shulman. 2010. Lectures on n-Categories and Cohomology. In Towards Higher Categories, John\u00a0C. Baez and J.\u00a0Peter May (Eds.). The IMA Volumes in Mathematics and its Applications, Vol.\u00a0152. Springer New York, New York, NY, 1\u201368. https:\/\/doi.org\/10.1007\/978-1-4419-1524-5_1"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018615"},{"key":"e_1_3_2_1_6_1","unstructured":"Thibaut Benjamin. 2018. Toward a fully formalized definition of syllepsis in weak higher-categories. http:\/\/www.t-news.cn\/Floc2018\/FLoC2018-pages\/proceedings_paper_290.pdf Abstract presented at Higher-Dimensional Rewriting and Applications 2018.  Thibaut Benjamin. 2018. Toward a fully formalized definition of syllepsis in weak higher-categories. http:\/\/www.t-news.cn\/Floc2018\/FLoC2018-pages\/proceedings_paper_290.pdf Abstract presented at Higher-Dimensional Rewriting and Applications 2018."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9468-2"},{"volume-title":"The periodic table of n-categories for low dimensions. I. Degenerate categories and degenerate bicategories","author":"Cheng Eugenia","key":"e_1_3_2_1_8_1","unstructured":"Eugenia Cheng and Nick Gurski . 2007. The periodic table of n-categories for low dimensions. I. Degenerate categories and degenerate bicategories . In Contemporary Mathematics, Alexei Davydov, Michael Batanin, Michael Johnson, Stephen Lack, and Amnon Neeman (Eds.). Vol.\u00a0431. American Mathematical Society, Providence, Rhode Island , 143\u2013164. https:\/\/doi.org\/10.1090\/conm\/431\/08270 arxiv:0708.1178 10.1090\/conm Eugenia Cheng and Nick Gurski. 2007. The periodic table of n-categories for low dimensions. I. Degenerate categories and degenerate bicategories. In Contemporary Mathematics, Alexei Davydov, Michael Batanin, Michael Johnson, Stephen Lack, and Amnon Neeman (Eds.). Vol.\u00a0431. American Mathematical Society, Providence, Rhode Island, 143\u2013164. https:\/\/doi.org\/10.1090\/conm\/431\/08270 arxiv:0708.1178"},{"key":"e_1_3_2_1_9_1","volume-title":"Retrieved","author":"Christensen Daniel","year":"2021","unstructured":"J.\u00a0 Daniel Christensen . 2021 . A very short proof of Eckmann-Hilton . Retrieved January 12, 2022 from https:\/\/groups.google.com\/g\/HomotopyTypeTheory\/c\/jelrhH5O6-k\/m\/TfjL8Kq4AQAJ Message to the Homotopy Type Theory mailing list. J.\u00a0Daniel Christensen. 2021. A very short proof of Eckmann-Hilton. Retrieved January 12, 2022 from https:\/\/groups.google.com\/g\/HomotopyTypeTheory\/c\/jelrhH5O6-k\/m\/TfjL8Kq4AQAJ Message to the Homotopy Type Theory mailing list."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1006\/aima.1997.1649"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01451367"},{"volume-title":"A proof of Eckmann-Hilton. https:\/\/github.com\/favonia\/homotopy\/blob\/master\/Path\/Omega2-abelian.agda#L37","key":"e_1_3_2_1_12_1","unstructured":"Favonia. 2012. A proof of Eckmann-Hilton. https:\/\/github.com\/favonia\/homotopy\/blob\/master\/Path\/Omega2-abelian.agda#L37 Favonia. 2012. A proof of Eckmann-Hilton. https:\/\/github.com\/favonia\/homotopy\/blob\/master\/Path\/Omega2-abelian.agda#L37"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533363"},{"key":"e_1_3_2_1_14_1","volume-title":"Categories for Quantum Theory: An Introduction (1 ed.)","author":"Heunen Chris","year":"1987","unstructured":"Chris Heunen and Jamie Vicary . 2019. Categories for Quantum Theory: An Introduction (1 ed.) . Oxford University Press . https:\/\/doi.org\/10.1093\/oso\/9780 1987 39623.001.0001 10.1093\/oso Chris Heunen and Jamie Vicary. 2019. Categories for Quantum Theory: An Introduction (1 ed.). Oxford University Press. https:\/\/doi.org\/10.1093\/oso\/9780198739623.001.0001"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2011.04.005"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.4171\/JEMS\/1050"},{"volume-title":"Number 298 in London Mathematical Society Lecture Note Series","author":"Leinster Tom","key":"e_1_3_2_1_17_1","unstructured":"Tom Leinster . 2004. Higher Operads , Higher Categories . Number 298 in London Mathematical Society Lecture Note Series . Cambridge University Press . https:\/\/doi.org\/10.1017\/cbo9780511525896 arXiv:math\/0305049 10.1017\/cbo9780511525896 Tom Leinster. 2004. Higher Operads, Higher Categories. Number 298 in London Mathematical Society Lecture Note Series. Cambridge University Press. https:\/\/doi.org\/10.1017\/cbo9780511525896 arXiv:math\/0305049"},{"key":"e_1_3_2_1_18_1","unstructured":"Daniel Licata. 2011. A Formal Proof that the Higher Fundamental Groups are Abelian. https:\/\/homotopytypetheory.org\/2011\/03\/26\/higher-fundamental-groups-are-abelian\/ Post on the Homotopy Type Theory blog.  Daniel Licata. 2011. A Formal Proof that the Higher Fundamental Groups are Abelian. https:\/\/homotopytypetheory.org\/2011\/03\/26\/higher-fundamental-groups-are-abelian\/ Post on the Homotopy Type Theory blog."},{"key":"e_1_3_2_1_19_1","first-page":"71","article-title":"Balanced Coalgebroids","volume":"7","author":"McCrudden Paddy","year":"2000","unstructured":"Paddy McCrudden . 2000 . Balanced Coalgebroids . Theory and Applications of Categories 7 , 6 (2000), 71 \u2013 147 . http:\/\/www.tac.mta.ca\/tac\/volumes\/7\/n6\/7-06abs.html Paddy McCrudden. 2000. Balanced Coalgebroids. Theory and Applications of Categories 7, 6 (2000), 71\u2013147. http:\/\/www.tac.mta.ca\/tac\/volumes\/7\/n6\/7-06abs.html","journal-title":"Theory and Applications of Categories"},{"key":"e_1_3_2_1_20_1","volume-title":"Re: Spans in 2-Categories: A monoidal tricategory. https:\/\/golem.ph.utexas.edu\/category\/2011\/12\/spans_in_2categories_a_monoida.html#c040468 Comment on a blog post on the n-Category Caf\u00e9.","author":"Shulman Mike","year":"2011","unstructured":"Mike Shulman . 2011 . Re: Spans in 2-Categories: A monoidal tricategory. https:\/\/golem.ph.utexas.edu\/category\/2011\/12\/spans_in_2categories_a_monoida.html#c040468 Comment on a blog post on the n-Category Caf\u00e9. Mike Shulman. 2011. Re: Spans in 2-Categories: A monoidal tricategory. https:\/\/golem.ph.utexas.edu\/category\/2011\/12\/spans_in_2categories_a_monoida.html#c040468 Comment on a blog post on the n-Category Caf\u00e9."},{"key":"e_1_3_2_1_21_1","volume-title":"arXiv:1904.07004","author":"Shulman Michael","year":"2019","unstructured":"Michael Shulman . 2019. All (\u221e, 1) \u2013toposes have strict univalent universes. ( 2019 ). arXiv:1904.07004 Michael Shulman. 2019. All (\u221e, 1)\u2013toposes have strict univalent universes. (2019). arXiv:1904.07004"},{"volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"Foundations Program The Univalent","key":"e_1_3_2_1_22_1","unstructured":"The Univalent Foundations Program . 2013. Homotopy Type Theory: Univalent Foundations of Mathematics . Institute for Advanced Study . https:\/\/homotopytypetheory.org\/book The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. https:\/\/homotopytypetheory.org\/book"},{"key":"e_1_3_2_1_23_1","unstructured":"Jamie Vicary. 2020. A type theory for strictly unital infinity-categories. https:\/\/youtu.be\/TSCggv_YE7M?t=4169. Homotopy Type Theory Electronic Seminar (HoTTEST) talk.  Jamie Vicary. 2020. A type theory for strictly unital infinity-categories. https:\/\/youtu.be\/TSCggv_YE7M?t=4169. Homotopy Type Theory Electronic Seminar (HoTTEST) talk."}],"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.3533347","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3531130.3533347","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:09Z","timestamp":1750186929000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3531130.3533347"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,2]]},"references-count":23,"alternative-id":["10.1145\/3531130.3533347","10.1145\/3531130"],"URL":"https:\/\/doi.org\/10.1145\/3531130.3533347","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"}}]}}