{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T18:44:08Z","timestamp":1763664248175,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,7,8]],"date-time":"2020-07-08T00:00:00Z","timestamp":1594166400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"publisher","award":["13156"],"award-info":[{"award-number":["13156"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100009927","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\/100009927","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.3394759","type":"proceedings-article","created":{"date-parts":[[2020,5,26]],"date-time":"2020-05-26T00:23:18Z","timestamp":1590452598000},"page":"807-819","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Partial Univalence in n-truncated Type Theory"],"prefix":"10.1145","author":[{"given":"Christian","family":"Sattler","sequence":"first","affiliation":[{"name":"Department of Computer Science and Engineering, Chalmers University of Technology, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Vezzosi","sequence":"additional","affiliation":[{"name":"Department of Computer Science, IT University of Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,7,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681500009X"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292608"},{"key":"e_1_3_2_1_4_1","unstructured":"Danil Annenkov Paolo Capriotti Nicolai Kraus and Christian Sattler. 2019. Two-Level Type Theory and Applications. arXiv preprint arXiv:1801.01568v3 (2019).  Danil Annenkov Paolo Capriotti Nicolai Kraus and Christian Sattler. 2019. Two-Level Type Theory and Applications. arXiv preprint arXiv:1801.01568v3 (2019)."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000268"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004108001783"},{"key":"e_1_3_2_1_7_1","unstructured":"Paolo Capriotti. 2016. Models of Type Theory with Strict Equality. Ph.D. Dissertation. School of Computer Science University of Nottingham.  Paolo Capriotti. 2016. Models of Type Theory with Strict Equality. Ph.D. Dissertation. School of Computer Science University of Nottingham."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(86)90053-9"},{"key":"e_1_3_2_1_9_1","volume-title":"Types for Proofs and Programs (TYPES 2015)","volume":"69","author":"Cohen Cyril","year":"2018"},{"key":"e_1_3_2_1_10_1","unstructured":"Thierry Coquand. 2016. Universe of Bishop sets.(2016). www.cse.chalmers.se\/~coquand\/bishop.pdf  Thierry Coquand. 2016. Universe of Bishop sets.(2016). www.cse.chalmers.se\/~coquand\/bishop.pdf"},{"volume-title":"4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) (Leibniz International Proceedings in Informatics (LIPIcs))","year":"2019","author":"Coquand Thierry","key":"e_1_3_2_1_11_1"},{"volume-title":"Types for Proofs and Programs (TYPES) (Lecture Notes in Computer Science)","author":"Dybjer Peter","key":"e_1_3_2_1_12_1"},{"volume-title":"Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs","year":"2018","author":"Frumin Dan","key":"e_1_3_2_1_13_1"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290316"},{"key":"e_1_3_2_1_15_1","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--111.  Martin Hofmann and Thomas Streicher. 1998. The groupoid interpretation of type theory. Twenty-five years of constructive type theory (Venice 1995) 36(1998) 83--111."},{"volume-title":"3rd International Conference on Formal Structures for Computation and Deduction (FSCD","year":"2018","author":"Kaposi Ambrus","key":"e_1_3_2_1_16_1"},{"volume-title":"The General Universal Property of the Prepositional Truncation. In 20th International Conference on Types for Proofs and Programs, TYPES 2014","year":"2014","author":"Kraus Nicolai","key":"e_1_3_2_1_17_1"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2729979"},{"volume-title":"Mathematical Proceedings of the Cambridge Philosophical Society","year":"2017","author":"LeFanu Lumsdaine Peter","key":"e_1_3_2_1_19_1"},{"key":"e_1_3_2_1_20_1","first-page":"73 71945","volume-title":"An Intuitionistic Theory of Types: Predicative Part. In Logic Colloquium '73","volume":"80","author":"Martin-L\u00f6f Per","year":"1975"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373835"},{"key":"e_1_3_2_1_22_1","unstructured":"Egbert Rijke. 2018. Introduction to Homotopy Type Theory. Lecture notes.  Egbert Rijke. 2018. Introduction to Homotopy Type Theory. Lecture notes."},{"key":"e_1_3_2_1_23_1","unstructured":"Egbert Rijke Michael Shulman and Bas Spitters. 2017. Modalities in homotopy type theory. arXiv preprint arXiv:1706.07526 (2017).  Egbert Rijke Michael Shulman and Bas Spitters. 2017. Modalities in homotopy type theory. arXiv preprint arXiv:1706.07526 (2017)."},{"key":"e_1_3_2_1_24_1","unstructured":"Christian Sattler and Andrea Vezzosi. 2020. Partial Univalence in n-truncated Type Theory. (2020). arXiv:2005.00260v1 [cs.LO]  Christian Sattler and Andrea Vezzosi. 2020. Partial Univalence in n-truncated Type Theory. (2020). arXiv:2005.00260v1 [cs.LO]"},{"key":"e_1_3_2_1_25_1","unstructured":"Jonathan Sterling Carlo Angiuli and Daniel Gratzer. 2019. Cubical Syntax for Reflection-Free Extensional Equality. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) (Leibniz International Proceedings in Informatics (LIPIcs)) Herman Geuvers (Ed.) Vol. 131. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik Dagstuhl Germany 31:1--31:25. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2019.31  Jonathan Sterling Carlo Angiuli and Daniel Gratzer. 2019. Cubical Syntax for Reflection-Free Extensional Equality. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) (Leibniz International Proceedings in Informatics (LIPIcs)) Herman Geuvers (Ed.) Vol. 131. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik Dagstuhl Germany 31:1--31:25. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2019.31"},{"key":"e_1_3_2_1_26_1","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study.  The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373814"}],"event":{"name":"LICS '20: 35th 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":"Saarbr\u00fccken Germany","acronym":"LICS '20"},"container-title":["Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394759","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3373718.3394759","content-type":"text\/html","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373718.3394759","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373718.3394759","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:35Z","timestamp":1750197755000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394759"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,8]]},"references-count":27,"alternative-id":["10.1145\/3373718.3394759","10.1145\/3373718"],"URL":"https:\/\/doi.org\/10.1145\/3373718.3394759","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"}}]}}