{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T07:13:15Z","timestamp":1760080395121,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":40,"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:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-17-1-0363, FA9550-15-1-0053, FA9550-16-1-0292"],"award-info":[{"award-number":["FA9550-17-1-0363, FA9550-15-1-0053, FA9550-16-1-0292"]}],"id":[{"id":"10.13039\/100000181","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.3394794","type":"proceedings-article","created":{"date-parts":[[2020,5,26]],"date-time":"2020-05-26T00:23:18Z","timestamp":1590452598000},"page":"915-928","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["A Constructive Model of Directed Univalence in Bicubical Sets"],"prefix":"10.1145","author":[{"given":"Matthew Z.","family":"Weaver","sequence":"first","affiliation":[{"name":"Department of Computer Science, Princeton University"}]},{"given":"Daniel R.","family":"Licata","sequence":"additional","affiliation":[{"name":"Department of Mathematics and Computer Science, Wesleyan University"}]}],"member":"320","published-online":{"date-parts":[[2020,7,8]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n.d.]. redtt. https:\/\/github.com\/RedPRL\/redtt.  [n.d.]. redtt. https:\/\/github.com\/RedPRL\/redtt."},{"key":"e_1_3_2_1_2_1","unstructured":"Carlo Angiuli Guillaume Brunerie Thierry Coquand Kuen-Bang Hou (Favonia) Robert Harper and Daniel R. Licata. 2019. Syntax and Models of Cartesian Cubical Type Theory. (2019). Available from https:\/\/github.com\/dlicata335\/cart-cube\/blob\/master\/cart-cube.pdf.  Carlo Angiuli Guillaume Brunerie Thierry Coquand Kuen-Bang Hou (Favonia) Robert Harper and Daniel R. Licata. 2019. Syntax and Models of Cartesian Cubical Type Theory. (2019). Available from https:\/\/github.com\/dlicata335\/cart-cube\/blob\/master\/cart-cube.pdf."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Carlo Angiuli Kuen-Bang Hou (Favonia) and Robert Harper. 2017. Computational Higher Type Theory III: Univalent Universes and Exact Equality. (2017). arXiv:1712.01800.  Carlo Angiuli Kuen-Bang Hou (Favonia) and Robert Harper. 2017. Computational Higher Type Theory III: Univalent Universes and Exact Equality. (2017). arXiv:1712.01800.","DOI":"10.1145\/3009837.3009861"},{"key":"e_1_3_2_1_4_1","unstructured":"Carlo Angiuli Kuen-Bang Hou (Favonia) and Robert Harper. 2018. Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities.. In Computer Science Logic.  Carlo Angiuli Kuen-Bang Hou (Favonia) and Robert Harper. 2018. Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities.. In Computer Science Logic."},{"key":"e_1_3_2_1_5_1","unstructured":"Steve Awodey. 2019. A Quillen model structure on the category of cartesian cubical sets. (2019). Talk at Homotopy Type Theory 2019 available from https:\/\/hott.github.io\/HoTT-2019.  Steve Awodey. 2019. A Quillen model structure on the category of cartesian cubical sets. (2019). Talk at Homotopy Type Theory 2019 available from https:\/\/hott.github.io\/HoTT-2019."},{"volume-title":"Mathematical Proceedings of the Cambridge Philosophical Society","year":"2009","author":"Awodey S.","key":"e_1_3_2_1_6_1"},{"key":"e_1_3_2_1_7_1","unstructured":"Marc Bezem Thierry Coquand and Simon Huber. 2013. A model of type theory in cubical sets. (September 2013). Preprint.  Marc Bezem Thierry Coquand and Simon Huber. 2013. A model of type theory in cubical sets. (September 2013). Preprint."},{"key":"e_1_3_2_1_8_1","unstructured":"Lars Birkedal Ales Bizjak Ranald Clouston Hans Bugge Grathwohl Bas Spitters and Andrea Vezzosi. 2016. Guarded Cubical Type Theory: Path Equality for Guarded Recursion. (2016). arXiv:1606.05223.  Lars Birkedal Ales Bizjak Ranald Clouston Hans Bugge Grathwohl Bas Spitters and Andrea Vezzosi. 2016. Guarded Cubical Type Theory: Path Equality for Guarded Recursion. (2016). arXiv:1606.05223."},{"key":"e_1_3_2_1_9_1","unstructured":"Ulrik Buchholtz and Jonathan Weinberger. 2019. Type-theoretic modalities for synthetic (\u221e 1)-categories. (2019). Talk at Homotopy Type Theory 2019.  Ulrik Buchholtz and Jonathan Weinberger. 2019. Type-theoretic modalities for synthetic (\u221e 1)-categories. (2019). Talk at Homotopy Type Theory 2019."},{"key":"e_1_3_2_1_10_1","unstructured":"Evan Cavallo and Robert Harper. 2019. Parametric Cubical Type Theory. (2019). arXiv:1901.00489.  Evan Cavallo and Robert Harper. 2019. Parametric Cubical Type Theory. (2019). arXiv:1901.00489."},{"volume-title":"Post-proceedings of the 21st International Conference on Types for Proofs and Programs (TYPES 2015","year":"2018","author":"Cohen Cyril","key":"e_1_3_2_1_11_1"},{"key":"e_1_3_2_1_12_1","unstructured":"Thierry Coquand. 2019. Constructive Presheaf Models of Univalence. (2019). Talk at Homotopy Type Theory 2019.  Thierry Coquand. 2019. Constructive Presheaf Models of Univalence. (2019). Talk at Homotopy Type Theory 2019."},{"key":"e_1_3_2_1_13_1","unstructured":"Thierry Coquand and Fabian Ruch. 2019. Constructive sheaf models of type theory. (2019). arXiv:1912.10407.  Thierry Coquand and Fabian Ruch. 2019. Constructive sheaf models of type theory. (2019). arXiv:1912.10407."},{"key":"e_1_3_2_1_14_1","unstructured":"Thierry Coquand and Christian Sattler. 2016. A model structure on some presheaf categories. (2016). Available from cse.chalmers.se\/~coquand\/mod2.pdf.  Thierry Coquand and Christian Sattler. 2016. A model structure on some presheaf categories. (2016). Available from cse.chalmers.se\/~coquand\/mod2.pdf."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Lisbeth Fajstrup Eric Goubault Emmanuel Haucourt Samuel Mimram and Martin Raussen. 2016. Directed algebraic topology and concurrency. Springer.  Lisbeth Fajstrup Eric Goubault Emmanuel Haucourt Samuel Mimram and Martin Raussen. 2016. Directed algebraic topology and concurrency. Springer.","DOI":"10.1007\/978-3-319-15398-8"},{"volume-title":"Abstract Syntax and Variable Binding. In IEEE Symposium on Logic in Computer Science.","year":"1999","author":"Fiore Marcelo","key":"e_1_3_2_1_16_1"},{"key":"e_1_3_2_1_17_1","unstructured":"Nicola Gambino and Simon Henry. 2019. Towards a constructive simplicial model of Univalent Foundations. (2019). https:\/\/arxiv.org\/abs\/1905.06281.  Nicola Gambino and Simon Henry. 2019. Towards a constructive simplicial model of Univalent Foundations. (2019). https:\/\/arxiv.org\/abs\/1905.06281."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"M. Grandis. 2009. Directed Algebraic Topology: Models of non-reversible worlds. Cambridge University Press.  M. Grandis. 2009. Directed Algebraic Topology: Models of non-reversible worlds. Cambridge University Press.","DOI":"10.1017\/CBO9780511657474"},{"key":"e_1_3_2_1_19_1","unstructured":"Martin Hofmann. 1995. Extensional Concepts in Intensional Type Theory. Ph.D. Dissertation. University of Edinburgh.  Martin Hofmann. 1995. Extensional Concepts in Intensional Type Theory. Ph.D. Dissertation. University of Edinburgh."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782616"},{"key":"e_1_3_2_1_21_1","unstructured":"Simon Huber. 2018. Canonicity for Cubical Type Theory. Journal of Automated Reasoning (2018). https:\/\/doi.org\/10.1007\/s10817--018--9469--1  Simon Huber. 2018. Canonicity for Cubical Type Theory. Journal of Automated Reasoning (2018). https:\/\/doi.org\/10.1007\/s10817--018--9469--1"},{"key":"e_1_3_2_1_22_1","unstructured":"Daniel R. Licata and Robert Harper. 2011. 2-Dimensional Directed Type Theory. In Mathematical Foundations of Programming Semantics (MFPS).  Daniel R. Licata and Robert Harper. 2011. 2-Dimensional Directed Type Theory. In Mathematical Foundations of Programming Semantics (MFPS)."},{"volume-title":"Internal Universes in Models of Homotopy Type Theory. In International Conference on Formal Structures for Computation and Deduction.","year":"2018","author":"Licata Daniel R.","key":"e_1_3_2_1_23_1"},{"key":"e_1_3_2_1_24_1","unstructured":"Paige Randall North. 2018. Towards a directed homotopy type theory. (2018). arXiv:1807.10566.  Paige Randall North. 2018. Towards a directed homotopy type theory. (2018). arXiv:1807.10566."},{"key":"e_1_3_2_1_25_1","unstructured":"Andreas Nuyts. 2015. Towards a directed HoTT based on 4 kinds of variance. Master's thesis. KU Leuven.  Andreas Nuyts. 2015. Towards a directed HoTT based on 4 kinds of variance. Master's thesis. KU Leuven."},{"key":"e_1_3_2_1_26_1","unstructured":"Andreas Nuyts. 2017. A Model of Parametric Dependent Type Theory in Bridge\/Path Cubical Sets. (2017). arXiv:1706.04383.  Andreas Nuyts. 2017. A Model of Parametric Dependent Type Theory in Bridge\/Path Cubical Sets. (2017). arXiv:1706.04383."},{"key":"e_1_3_2_1_27_1","unstructured":"Ian Orton and Andrew M. Pitts. 2016. Axioms for Modelling Cubical Type Theory in a Topos. In Computer Science Logic.  Ian Orton and Andrew M. Pitts. 2016. Axioms for Modelling Cubical Type Theory in a Topos. In Computer Science Logic."},{"key":"e_1_3_2_1_28_1","first-page":"23","article-title":"2018. Axioms for Modelling Cubical Type Theory in a Topos","volume":"14","author":"Orton I.","year":"2018","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Emily Riehl. 2014. Categorical Homotopy Theory. Cambridge University Press.  Emily Riehl. 2014. Categorical Homotopy Theory. Cambridge University Press.","DOI":"10.1017\/CBO9781107261457"},{"key":"e_1_3_2_1_30_1","unstructured":"Emily Riehl. 2019. The equivariant uniform kan fibration model of cubical homotopy type theory. (2019). Talk at Homotopy Type Theory 2019.  Emily Riehl. 2019. The equivariant uniform kan fibration model of cubical homotopy type theory. (2019). Talk at Homotopy Type Theory 2019."},{"volume-title":"Joint Mathematics Meetings.","year":"2018","author":"Riehl Emily","key":"e_1_3_2_1_31_1"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Emily Riehl and Michael Shulman. 2018. A type theory for synthetic \u221e-categories. Higher Structures 1 1 (2018).  Emily Riehl and Michael Shulman. 2018. A type theory for synthetic \u221e-categories. Higher Structures 1 1 (2018).","DOI":"10.21136\/HS.2017.06"},{"key":"e_1_3_2_1_33_1","unstructured":"Emily Riehl and Dominic Verity. 2014. The theory and practice of Reedy categories. Theory and Applications of Categories 29 9 (2014).  Emily Riehl and Dominic Verity. 2014. The theory and practice of Reedy categories. Theory and Applications of Categories 29 9 (2014)."},{"key":"e_1_3_2_1_34_1","unstructured":"Christian Sattler. 2018. Do cubical models of type theory also model homotopy types? (2018). Talk at Workshop on Types Homotopy Type theory and Verification Hausdorff Institute for Mathematics.  Christian Sattler. 2018. Do cubical models of type theory also model homotopy types? (2018). Talk at Workshop on Types Homotopy Type theory and Verification Hausdorff Institute for Mathematics."},{"key":"e_1_3_2_1_35_1","unstructured":"Christian Sattler and Emily Riehl. 2018. Directed univalence for the left fibration classifier. (2018). Private correspondence.  Christian Sattler and Emily Riehl. 2018. Directed univalence for the left fibration classifier. (2018). Private correspondence."},{"key":"e_1_3_2_1_36_1","unstructured":"Michael Shulman. 2009. Homotopy limits and colimits and enriched homotopy theory. (2009). https:\/\/arxiv.org\/abs\/math\/0610194.  Michael Shulman. 2009. Homotopy limits and colimits and enriched homotopy theory. (2009). https:\/\/arxiv.org\/abs\/math\/0610194."},{"key":"e_1_3_2_1_37_1","unstructured":"Michael Shulman. 2019. All (\u221e 1)-toposes have strict univalent universes. (2019). arXiv:1904.07004.  Michael Shulman. 2019. All (\u221e 1)-toposes have strict univalent universes. (2019). arXiv:1904.07004."},{"key":"e_1_3_2_1_38_1","unstructured":"The Univalent Foundations Program Institute for Advanced Study. 2013. Homotopy Type Theory: Univalent Foundations Of Mathematics. Available from homotopytypetheory.org\/book.  The Univalent Foundations Program Institute for Advanced Study. 2013. Homotopy Type Theory: Univalent Foundations Of Mathematics. Available from homotopytypetheory.org\/book."},{"key":"e_1_3_2_1_39_1","unstructured":"Vladimir Voevodsky. 2006. A very short note on homotopy \u03bb-calculus. Unpublished (September 2006) 1--7. http:\/\/www.math.ias.edu\/vladimir\/files\/2006_09_Hlambda. pdf  Vladimir Voevodsky. 2006. A very short note on homotopy \u03bb-calculus. Unpublished (September 2006) 1--7. http:\/\/www.math.ias.edu\/vladimir\/files\/2006_09_Hlambda. pdf"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"crossref","unstructured":"Matthew Z. Weaver and Daniel R. Licata. 2020. A Constructive Model of Directed Univalence in Bicubical Sets (extended version). (2020). Available from https:\/\/dlicata.wescreates.wesleyan.edu\/.  Matthew Z. Weaver and Daniel R. Licata. 2020. A Constructive Model of Directed Univalence in Bicubical Sets (extended version). (2020). Available from https:\/\/dlicata.wescreates.wesleyan.edu\/.","DOI":"10.1145\/3373718.3394794"}],"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.3394794","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3373718.3394794","content-type":"text\/html","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373718.3394794","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373718.3394794","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:36Z","timestamp":1750197756000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394794"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,8]]},"references-count":40,"alternative-id":["10.1145\/3373718.3394794","10.1145\/3373718"],"URL":"https:\/\/doi.org\/10.1145\/3373718.3394794","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"}}]}}