{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,12]],"date-time":"2024-08-12T18:33:50Z","timestamp":1723487630521},"publisher-location":"New York, NY, USA","reference-count":26,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,7,8]],"date-time":"2021-07-08T00:00:00Z","timestamp":1625702400000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-17-1-0326"],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100014718","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1704788"],"id":[{"id":"10.13039\/100014718","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,7,8]]},"DOI":"10.1145\/3373718.3394801","type":"proceedings-article","created":{"date-parts":[[2020,5,26]],"date-time":"2020-05-26T00:23:18Z","timestamp":1590452598000},"update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Sequential Colimits in Homotopy Type Theory"],"prefix":"10.1145","author":[{"given":"Kristina","family":"Sojakova","sequence":"first","affiliation":[{"name":"Cornell University, USA"}]},{"given":"Floris van","family":"Doorn","sequence":"additional","affiliation":[{"name":"University of Pittsburgh, USA"}]},{"given":"Egbert","family":"Rijke","sequence":"additional","affiliation":[{"name":"University of Ljubljana, Slovenia"}]}],"member":"320","published-online":{"date-parts":[[2020,7,8]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"589","article-title":"Free Algebras and Automata Realizations in The Language of Categories","volume":"15","author":"Adamek J.","year":"1974","journal-title":"Commentationes Mathematicae Universitatis Carolinae"},{"key":"e_1_3_2_1_2_1","unstructured":"S. Awodey R. Garner P. Martin-L\u00f6f and V. Voevodsky (organizers). 2011. Mini-Workshop (Oberwolfach): The Homotopy Interpretation of Constructive Type Theory. (2011). Available at https:\/\/hottheory.files.wordpress.com\/2011\/06\/report- 11_2011.pdf. S. Awodey R. Garner P. Martin-L\u00f6f and V. Voevodsky (organizers). 2011. Mini-Workshop (Oberwolfach): The Homotopy Interpretation of Constructive Type Theory. (2011). Available at https:\/\/hottheory.files.wordpress.com\/2011\/06\/report- 11_2011.pdf."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004108001783"},{"key":"e_1_3_2_1_4_1","volume-title":"Studies in Logic and the Foundations of Mathematics","volume":"103","author":"Barendregt H.","year":"1985"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"F. Borceux. 1994. Handbook of Categorical Algebra. Cambridge University Press. F. Borceux. 1994. Handbook of Categorical Algebra. Cambridge University Press.","DOI":"10.1017\/CBO9780511525858"},{"key":"e_1_3_2_1_6_1","unstructured":"G. Brunerie. 2016. On the Homotopy Groups of Spheres in Homotopy Type Theory. (2016). Available at arxiv.org as arXiv:1606.05916. G. Brunerie. 2016. On the Homotopy Groups of Spheres in Homotopy Type Theory. (2016). Available at arxiv.org as arXiv:1606.05916."},{"key":"e_1_3_2_1_7_1","unstructured":"E. Cavallo. 2015. Synthetic Cohomology in Homotopy Type Theory. Master's thesis. Carnegie Mellon University. E. Cavallo. 2015. Synthetic Cohomology in Homotopy Type Theory. Master's thesis. Carnegie Mellon University."},{"key":"e_1_3_2_1_8_1","unstructured":"J. Christensen M. Opie E. Rijke and L. Scoccola. 2018. Localization in Homotopy Type Theory. (2018). J. Christensen M. Opie E. Rijke and L. Scoccola. 2018. Localization in Homotopy Type Theory. (2018)."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_3_2_1_10_1","unstructured":"R. Graham. 2017. Synthetic Homology in Homotopy Type Theory. (2017). Available at arxiv.org as arXiv:1706.01540. R. Graham. 2017. Synthetic Homology in Homotopy Type Theory. (2017). Available at arxiv.org as arXiv:1706.01540."},{"key":"e_1_3_2_1_11_1","unstructured":"C. Kapulkin and P. LeFanu Lumsdaine. 2012. The Simplicial Model of Univalent Foundations (after Voevodsky). (2012). To appear in the Journal of European Mathematical Society. Available at arxiv.org as arXiv:1203.3253v5. C. Kapulkin and P. LeFanu Lumsdaine. 2012. The Simplicial Model of Univalent Foundations (after Voevodsky). (2012). To appear in the Journal of European Mathematical Society. Available at arxiv.org as arXiv:1203.3253v5."},{"key":"e_1_3_2_1_12_1","volume-title":"To appear in Logic in Computer Science (LICS","author":"Kraus N.","year":"2019"},{"key":"e_1_3_2_1_13_1","unstructured":"P. LeFanu Lumsdaine. 2011. Higher Inductive Types: a Tour of the Menagerie. (2011). Available at https:\/\/homotopytypetheory.org\/2011\/04\/24\/higher-inductive-types-a-tour-of-the-menagerie\/. P. LeFanu Lumsdaine. 2011. Higher Inductive Types: a Tour of the Menagerie. (2011). Available at https:\/\/homotopytypetheory.org\/2011\/04\/24\/higher-inductive-types-a-tour-of-the-menagerie\/."},{"key":"e_1_3_2_1_14_1","unstructured":"P. LeFanu Lumsdaine and M. Shulman. 2017. Semantics of Higher Inductive Types. (2017). Available at arxiv.org as arXiv:1705.07088v2. P. LeFanu Lumsdaine and M. Shulman. 2017. Semantics of Higher Inductive Types. (2017). Available at arxiv.org as arXiv:1705.07088v2."},{"key":"e_1_3_2_1_15_1","article-title":"Higher Topos Theory","volume":"170","author":"Lurie J.","year":"2009","journal-title":"Annals of Mathematics Studies"},{"key":"e_1_3_2_1_16_1","volume-title":"Graduate Texts in Mathematics","volume":"5","author":"MacLane S.","year":"1971"},{"key":"e_1_3_2_1_17_1","volume-title":"Logic Colloquium","author":"Martin-L\u00f6f P.","year":"1973"},{"key":"e_1_3_2_1_18_1","unstructured":"E. Rijke. 2017. The Join Construction. (2017). Available at arxiv.org as arXiv:1701.07538. E. Rijke. 2017. The Join Construction. (2017). Available at arxiv.org as arXiv:1701.07538."},{"key":"e_1_3_2_1_19_1","unstructured":"M. Shulman. 2011. Homotopy Type Theory VI. Available at https:\/\/golem.ph.utexas.edu\/category\/2011\/04\/homotopy_type_theory_vi.html. (2011). M. Shulman. 2011. Homotopy Type Theory VI. Available at https:\/\/golem.ph.utexas.edu\/category\/2011\/04\/homotopy_type_theory_vi.html. (2011)."},{"key":"e_1_3_2_1_20_1","unstructured":"M. Shulman. 2013. Spectral Sequences. Available at https:\/\/homotopytypetheory.org\/2013\/08\/08\/spectral-sequences\/. (2013). M. Shulman. 2013. Spectral Sequences. Available at https:\/\/homotopytypetheory.org\/2013\/08\/08\/spectral-sequences\/. (2013)."},{"key":"e_1_3_2_1_21_1","unstructured":"M. Shulman. 2019. All (\u221e 1)-Toposes Have Strict Univalent Universes. (2019). Available at arxiv.org as arXiv:1904.07004. M. Shulman. 2019. All (\u221e 1)-Toposes Have Strict Univalent Universes. (2019). Available at arxiv.org as arXiv:1904.07004."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"K. Sojakova. 2016. Higher Inductive Types as Homotopy-Initial Algebras. Ph.D. Dissertation. Carnegie Mellon University. K. Sojakova. 2016. Higher Inductive Types as Homotopy-Initial Algebras. Ph.D. Dissertation. Carnegie Mellon University.","DOI":"10.1145\/2676726.2676983"},{"key":"e_1_3_2_1_23_1","unstructured":"The Univalent Foundations Program Institute for Advanced Study. 2013. Homotopy Type Theory - Univalent Foundations of Mathematics. Univalent Foundations Project. The Univalent Foundations Program Institute for Advanced Study. 2013. Homotopy Type Theory - Univalent Foundations of Mathematics. Univalent Foundations Project."},{"key":"e_1_3_2_1_24_1","volume-title":"Certified Programs and Proofs (CPP","author":"van Doorn F.","year":"2016"},{"key":"e_1_3_2_1_25_1","unstructured":"V. Voevodsky. 2010. The Equivalence Axiom and Univalent Models of Type Theory. (2010). Invited talk at Carnegie Mellon University available at arxiv.org as arXiv:1402.5556v2. V. Voevodsky. 2010. The Equivalence Axiom and Univalent Models of Type Theory. (2010). Invited talk at Carnegie Mellon University available at arxiv.org as arXiv:1402.5556v2."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","unstructured":"V. Voevodsky. 2011. Univalent Foundations of Mathematics. (2011). Invited talk at the Workshop on Logic Language Information and Computation (WoLLIC 2011). V. Voevodsky. 2011. Univalent Foundations of Mathematics. (2011). Invited talk at the Workshop on Logic Language Information and Computation (WoLLIC 2011).","DOI":"10.1007\/978-3-642-20920-8_4"}],"event":{"name":"LICS '20: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Saarbr\u00fccken Germany","acronym":"LICS '20","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"]},"container-title":["Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3373718.3394801","content-type":"text\/html","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373718.3394801","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373718.3394801","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T23:15:10Z","timestamp":1673306110000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394801"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,8]]},"references-count":26,"alternative-id":["10.1145\/3373718.3394801","10.1145\/3373718"],"URL":"http:\/\/dx.doi.org\/10.1145\/3373718.3394801","relation":{},"subject":[],"published":{"date-parts":[[2020,7,8]]},"assertion":[{"value":"2020-07-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}