{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:33:52Z","timestamp":1750221232438,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":23,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,7,9]],"date-time":"2018-07-09T00:00:00Z","timestamp":1531094400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/M016994\/1"],"award-info":[{"award-number":["EP\/M016994\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006393","name":"U.S. Air Force","doi-asserted-by":"publisher","award":["FA9550-16-1-0029"],"award-info":[{"award-number":["FA9550-16-1-0029"]}],"id":[{"id":"10.13039\/100006393","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,7,9]]},"DOI":"10.1145\/3209108.3209183","type":"proceedings-article","created":{"date-parts":[[2018,6,27]],"date-time":"2018-06-27T12:14:43Z","timestamp":1530101683000},"page":"599-608","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Free Higher Groups in Homotopy Type Theory"],"prefix":"10.1145","author":[{"given":"Nicolai","family":"Kraus","sequence":"first","affiliation":[{"name":"University of Nottingham"}]},{"given":"Thorsten","family":"Altenkirch","sequence":"additional","affiliation":[{"name":"University of Nottingham"}]}],"member":"320","published-online":{"date-parts":[[2018,7,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1515\/9781400821259"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_16"},{"key":"e_1_3_2_1_3_1","volume-title":"Extending Homotopy Type Theory with Strict Equality. In 25th EACSL Annual Conference on Computer Science Logic (CSL","volume":"62","author":"Altenkirch Thorsten","year":"2016","unstructured":"Thorsten Altenkirch , Paolo Capriotti , and Nicolai Kraus . 2016 . Extending Homotopy Type Theory with Strict Equality. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), Jean-Marc Talbot and Laurent Regnier (Eds.) , Vol. 62 . Dagstuhl, Germany, 21:1--21:17. Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. 2016. Extending Homotopy Type Theory with Strict Equality. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), Jean-Marc Talbot and Laurent Regnier (Eds.), Vol. 62. Dagstuhl, Germany, 21:1--21:17."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_31"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"e_1_3_2_1_6_1","unstructured":"C. Angiuli K.-B. Hou and R. Harper. 2017. Computational Higher Type Theory III: Univalent Universes and Exact Equality. ArXiv e-prints (Dec. 2017). arXiv:cs.LO\/1712.01800  C. Angiuli K.-B. Hou and R. Harper. 2017. Computational Higher Type Theory III: Univalent Universes and Exact Equality. ArXiv e-prints (Dec. 2017). arXiv:cs.LO\/1712.01800"},{"key":"e_1_3_2_1_7_1","volume-title":"Two-Level Type Theory and Applications. Arxiv e-prints","author":"Annenkov Danil","year":"2017","unstructured":"Danil Annenkov , Paolo Capriotti , and Nicolai Kraus . 2017. Two-Level Type Theory and Applications. Arxiv e-prints ( 2017 ). http:\/\/arxiv.org\/abs\/1705.03307 Danil Annenkov, Paolo Capriotti, and Nicolai Kraus. 2017. Two-Level Type Theory and Applications. Arxiv e-prints (2017). http:\/\/arxiv.org\/abs\/1705.03307"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.21"},{"key":"e_1_3_2_1_9_1","volume-title":"The James construction and π4 (S3) in homotopy type theory. CoRR","author":"Brunerie Guillaume","year":"2017","unstructured":"Guillaume Brunerie . 2017. The James construction and π4 (S3) in homotopy type theory. CoRR ( 2017 ). http:\/\/arxiv.org\/abs\/1710.10307 Guillaume Brunerie. 2017. The James construction and π4 (S3) in homotopy type theory. CoRR (2017). http:\/\/arxiv.org\/abs\/1710.10307"},{"key":"e_1_3_2_1_10_1","unstructured":"Ulrik Buchholtz Floris van Doorn and Egbert Rijke. 2018. Higher Groups in Homotopy Type Theory. (2018). https:\/\/arxiv.org\/abs\/1802.04315  Ulrik Buchholtz Floris van Doorn and Egbert Rijke. 2018. Higher Groups in Homotopy Type Theory. (2018). https:\/\/arxiv.org\/abs\/1802.04315"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158132"},{"key":"e_1_3_2_1_13_1","volume-title":"24th EACSL Annual Conference on Computer Science Logic (CSL) 2015) (Leibniz International Proceedings in Informatics (LIPIcs)), Stephan Kreutzer (Ed.)","volume":"41","author":"Capriotti Paolo","year":"2015","unstructured":"Paolo Capriotti , Nicolai Kraus , and Andrea Vezzosi . 2015 . Functions out of Higher Truncations . In 24th EACSL Annual Conference on Computer Science Logic (CSL) 2015) (Leibniz International Proceedings in Informatics (LIPIcs)), Stephan Kreutzer (Ed.) , Vol. 41 . Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 359--373. Paolo Capriotti, Nicolai Kraus, and Andrea Vezzosi. 2015. Functions out of Higher Truncations. In 24th EACSL Annual Conference on Computer Science Logic (CSL) 2015) (Leibniz International Proceedings in Informatics (LIPIcs)), Stephan Kreutzer (Ed.), Vol. 41. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 359--373."},{"volume-title":"20th International Conference on Types for Proofs and Programs (TYPES 2014) (Leibniz International Proceedings in Informatics (LIPIcs))","author":"Kraus Nicolai","key":"e_1_3_2_1_14_1","unstructured":"Nicolai Kraus . 2015. The General Universal Property of the Propositional Truncation . In 20th International Conference on Types for Proofs and Programs (TYPES 2014) (Leibniz International Proceedings in Informatics (LIPIcs)) , Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau (Eds.), Vol. 39 . Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany , 111--145. Nicolai Kraus. 2015. The General Universal Property of the Propositional Truncation. In 20th International Conference on Types for Proofs and Programs (TYPES 2014) (Leibniz International Proceedings in Informatics (LIPIcs)), Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau (Eds.), Vol. 39. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 111--145."},{"key":"e_1_3_2_1_16_1","volume-title":"Notions of Anonymous Existence in Martin-L\u00f6f Type Theory. Logical Methods in Computer Science","author":"Kraus Nicolai","year":"2017","unstructured":"Nicolai Kraus , Mart\u00edn H. Escard\u00f3 , Thierry Coquand , and Thorsten Altenkirch . 2017. Notions of Anonymous Existence in Martin-L\u00f6f Type Theory. Logical Methods in Computer Science Volume 13 , Issue 1 (mar 2017 ). In the special issue of TLCA '13. Nicolai Kraus, Mart\u00edn H. Escard\u00f3, Thierry Coquand, and Thorsten Altenkirch. 2017. Notions of Anonymous Existence in Martin-L\u00f6f Type Theory. Logical Methods in Computer Science Volume 13, Issue 1 (mar 2017). In the special issue of TLCA'13."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.28"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_14"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.aim.2015.09.011"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676983"},{"key":"e_1_3_2_1_21_1","first-page":"275","article-title":"Homotopy associativity of H-spaces","volume":"108","author":"Stasheff Jim","year":"1963","unstructured":"Jim Stasheff . 1963 . Homotopy associativity of H-spaces . Trans. Amer. Math. Soc. 108 (1963), 275 -- 292 , 293--312. Jim Stasheff. 1963. Homotopy associativity of H-spaces. Trans. Amer. Math. Soc. 108 (1963), 275--292, 293--312.","journal-title":"Trans. Amer. Math. Soc."},{"key":"e_1_3_2_1_22_1","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. http:\/\/homotopytypetheory.org\/book\/ Institute for Advanced Study.  The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. http:\/\/homotopytypetheory.org\/book\/ Institute for Advanced Study."},{"key":"e_1_3_2_1_23_1","unstructured":"The Univalent Foundations Program. 2013. Semi-simplicial types. (2013). Wiki page of the Univalent Foundations project at the Institute for Advanced Studies https:\/\/uf-ias-2012.wikispaces.com\/Semi-simplicial+types.  The Univalent Foundations Program. 2013. Semi-simplicial types. (2013). Wiki page of the Univalent Foundations project at the Institute for Advanced Studies https:\/\/uf-ias-2012.wikispaces.com\/Semi-simplicial+types."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/pdq026"},{"key":"e_1_3_2_1_25_1","unstructured":"Vladimir Voevodsky. 2013. A simple type system with two identity types. (2013). Unpublished note.  Vladimir Voevodsky. 2013. A simple type system with two identity types. (2013). Unpublished note."}],"event":{"name":"LICS '18: 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"],"location":"Oxford United Kingdom","acronym":"LICS '18"},"container-title":["Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3209108.3209183","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3209108.3209183","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3209108.3209183","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:07:08Z","timestamp":1750212428000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3209108.3209183"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,9]]},"references-count":23,"alternative-id":["10.1145\/3209108.3209183","10.1145\/3209108"],"URL":"https:\/\/doi.org\/10.1145\/3209108.3209183","relation":{},"subject":[],"published":{"date-parts":[[2018,7,9]]},"assertion":[{"value":"2018-07-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}