{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:22:22Z","timestamp":1776316942112,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":44,"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:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-21-1-0334"],"award-info":[{"award-number":["FA9550-21-1-0334"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/T000252\/1"],"award-info":[{"award-number":["EP\/T000252\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,8,2]]},"DOI":"10.1145\/3531130.3533334","type":"proceedings-article","created":{"date-parts":[[2022,8,4]],"date-time":"2022-08-04T20:23:38Z","timestamp":1659644618000},"page":"1-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Semantics for two-dimensional type theory"],"prefix":"10.1145","author":[{"given":"Benedikt","family":"Ahrens","sequence":"first","affiliation":[{"name":"Delft University of Technology, Netherlands and University of Birmingham, United Kingdom"}]},{"given":"Paige Randall","family":"North","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}]},{"given":"Niels","family":"van der Weide","sequence":"additional","affiliation":[{"name":"Radboud University, Netherlands"}]}],"member":"320","published-online":{"date-parts":[[2022,8,4]]},"reference":[{"key":"#cr-split#-e_1_3_2_1_1_1.1","unstructured":"Benedikt Ahrens Dan Frumin Marco Maggesi and Niels van\u00a0der Weide. 2019. Bicategories in Univalent Foundations. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)(Leibniz International Proceedings in Informatics (LIPIcs) Vol.\u00a0131) Herman Geuvers (Ed.). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik Dagstuhl Germany 5:1-5:17. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2019.5 10.4230\/LIPIcs.FSCD.2019.5"},{"key":"#cr-split#-e_1_3_2_1_1_1.2","unstructured":"Benedikt Ahrens Dan Frumin Marco Maggesi and Niels van\u00a0der Weide. 2019. Bicategories in Univalent Foundations. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)(Leibniz International Proceedings in Informatics (LIPIcs) Vol.\u00a0131) Herman Geuvers (Ed.). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik Dagstuhl Germany 5:1-5:17. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2019.5"},{"key":"#cr-split#-e_1_3_2_1_2_1.1","doi-asserted-by":"crossref","unstructured":"Benedikt Ahrens Dan Frumin Marco Maggesi Niccol\u00f2 Veltri and Niels van\u00a0der Weide. 2022. Bicategories in univalent foundations. Mathematical Structures in Computer Science(2022) 1-38. https:\/\/doi.org\/10.1017\/S0960129522000032 10.1017\/S0960129522000032","DOI":"10.1017\/S0960129522000032"},{"key":"#cr-split#-e_1_3_2_1_2_1.2","doi-asserted-by":"crossref","unstructured":"Benedikt Ahrens Dan Frumin Marco Maggesi Niccol\u00f2 Veltri and Niels van\u00a0der Weide. 2022. Bicategories in univalent foundations. Mathematical Structures in Computer Science(2022) 1-38. https:\/\/doi.org\/10.1017\/S0960129522000032","DOI":"10.1017\/S0960129522000032"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000486"},{"key":"e_1_3_2_1_4_1","volume-title":"Methods Comput. Sci. 15, 1","author":"Ahrens Benedikt","year":"2019","unstructured":"Benedikt Ahrens and Peter\u00a0 LeFanu Lumsdaine . 2019. Displayed Categories . Log. Methods Comput. Sci. 15, 1 ( 2019 ). https:\/\/doi.org\/10.23638\/LMCS-15(1:20)2019 10.23638\/LMCS-15(1:20)2019 Benedikt Ahrens and Peter\u00a0LeFanu Lumsdaine. 2019. Displayed Categories. Log. Methods Comput. Sci. 15, 1 (2019). https:\/\/doi.org\/10.23638\/LMCS-15(1:20)2019"},{"key":"e_1_3_2_1_5_1","volume-title":"Globular: an online proof assistant for higher-dimensional rewriting. Log. Methods Comput. Sci. 14, 1","author":"Bar Krzysztof","year":"2018","unstructured":"Krzysztof Bar , Aleks Kissinger , and Jamie Vicary . 2018. Globular: an online proof assistant for higher-dimensional rewriting. Log. Methods Comput. Sci. 14, 1 ( 2018 ). https:\/\/doi.org\/10.23638\/LMCS-14(1:8)2018 10.23638\/LMCS-14(1:8)2018 Krzysztof Bar, Aleks Kissinger, and Jamie Vicary. 2018. Globular: an online proof assistant for higher-dimensional rewriting. Log. Methods Comput. Sci. 14, 1 (2018). https:\/\/doi.org\/10.23638\/LMCS-14(1:8)2018"},{"key":"e_1_3_2_1_6_1","volume-title":"Reports of the Midwest Category Seminar","author":"B\u00e9nabou Jean","unstructured":"Jean B\u00e9nabou . 1967. Introduction to bicategories . In Reports of the Midwest Category Seminar . Springer Berlin Heidelberg , Berlin, Heidelberg , 1\u201377. https:\/\/doi.org\/10.1007\/BFb0074299 10.1007\/BFb0074299 Jean B\u00e9nabou. 1967. Introduction to bicategories. In Reports of the Midwest Category Seminar. Springer Berlin Heidelberg, Berlin, Heidelberg, 1\u201377. https:\/\/doi.org\/10.1007\/BFb0074299"},{"key":"e_1_3_2_1_7_1","volume-title":"Globular weak \u03c9-categories as models of a type theory. CoRR","author":"Benjamin Thibaut","year":"2021","unstructured":"Thibaut Benjamin , Eric Finster , and Samuel Mimram . 2021. Globular weak \u03c9-categories as models of a type theory. CoRR ( 2021 ). arXiv:2106.04475 Thibaut Benjamin, Eric Finster, and Samuel Mimram. 2021. Globular weak \u03c9-categories as models of a type theory. CoRR (2021). arXiv:2106.04475"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/pdq026"},{"key":"e_1_3_2_1_10_1","unstructured":"Ulrik Buchholtz and Jonathan Weinberger. 2021. Synthetic fibered (\u221e 1)-category theory. CoRR abs\/2105.01724(2021). arXiv:2105.01724  Ulrik Buchholtz and Jonathan Weinberger. 2021. Synthetic fibered (\u221e 1)-category theory. CoRR abs\/2105.01724(2021). arXiv:2105.01724"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2013.11.002"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005130"},{"key":"e_1_3_2_1_13_1","volume-title":"Directed Algebraic Topology and Concurrency","author":"Fajstrup Lisbeth","unstructured":"Lisbeth Fajstrup , Eric Goubault , Emmanuel Haucourt , Samuel Mimram , and Martin Raussen . 2016. Directed Algebraic Topology and Concurrency . Springer . https:\/\/doi.org\/10.1007\/978-3-319-15398-8 10.1007\/978-3-319-15398-8 Lisbeth Fajstrup, Eric Goubault, Emmanuel Haucourt, Samuel Mimram, and Martin Raussen. 2016. Directed Algebraic Topology and Concurrency. Springer. https:\/\/doi.org\/10.1007\/978-3-319-15398-8"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005124"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533363"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785708"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129509007646"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-99902-4_2"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(97)00129-1"},{"key":"e_1_3_2_1_20_1","volume-title":"Cartesian closed 2-categories and permutation equivalence in higher-order rewriting. Log. Methods Comput. Sci. 9, 3","author":"Hirschowitz Tom","year":"2013","unstructured":"Tom Hirschowitz . 2013. Cartesian closed 2-categories and permutation equivalence in higher-order rewriting. Log. Methods Comput. Sci. 9, 3 ( 2013 ). https:\/\/doi.org\/10.2168\/LMCS-9(3:10)2013 10.2168\/LMCS-9(3:10)2013 Tom Hirschowitz. 2013. Cartesian closed 2-categories and permutation equivalence in higher-order rewriting. Log. Methods Comput. Sci. 9, 3 (2013). https:\/\/doi.org\/10.2168\/LMCS-9(3:10)2013"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316071"},{"key":"e_1_3_2_1_22_1","volume-title":"Pullbacks equivalent to pseudopullbacks. Cahiers de topologie et g\u00e9om\u00e9trie diff\u00e9rentielle cat\u00e9goriques 34, 2","author":"Joyal Andr\u00e9","year":"1993","unstructured":"Andr\u00e9 Joyal and Ross Street . 1993. Pullbacks equivalent to pseudopullbacks. Cahiers de topologie et g\u00e9om\u00e9trie diff\u00e9rentielle cat\u00e9goriques 34, 2 ( 1993 ), 153\u2013156. http:\/\/eudml.org\/doc\/91518 Andr\u00e9 Joyal and Ross Street. 1993. Pullbacks equivalent to pseudopullbacks. Cahiers de topologie et g\u00e9om\u00e9trie diff\u00e9rentielle cat\u00e9goriques 34, 2 (1993), 153\u2013156. http:\/\/eudml.org\/doc\/91518"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.4171\/JEMS\/1050"},{"key":"e_1_3_2_1_25_1","volume-title":"Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, MFPS 2011","author":"R.","year":"2011","unstructured":"Daniel\u00a0 R. Licata and Robert Harper. 2011. 2-Dimensional Directed Type Theory . In Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, MFPS 2011 , Pittsburgh, PA, USA , May 25-28, 2011 (Electronic Notes in Theoretical Computer Science, Vol.\u00a0276), Michael\u00a0W. Mislove and Jo\u00ebl Ouaknine (Eds.). Elsevier, 263\u2013289. https:\/\/doi.org\/10.1016\/j.entcs.2011.09.026 10.1016\/j.entcs.2011.09.026 Daniel\u00a0R. Licata and Robert Harper. 2011. 2-Dimensional Directed Type Theory. In Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, MFPS 2011, Pittsburgh, PA, USA, May 25-28, 2011(Electronic Notes in Theoretical Computer Science, Vol.\u00a0276), Michael\u00a0W. Mislove and Jo\u00ebl Ouaknine (Eds.). Elsevier, 263\u2013289. https:\/\/doi.org\/10.1016\/j.entcs.2011.09.026"},{"key":"e_1_3_2_1_26_1","volume-title":"Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012","author":"R.","year":"2012","unstructured":"Daniel\u00a0 R. Licata and Robert Harper. 2012. Canonicity for 2-dimensional type theory . In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012 , Philadelphia, Pennsylvania, USA , January 22-28, 2012 , John Field and Michael Hicks (Eds.). ACM, 337\u2013348. https:\/\/doi.org\/10.1145\/2103656.2103697 10.1145\/2103656.2103697 Daniel\u00a0R. Licata and Robert Harper. 2012. Canonicity for 2-dimensional type theory. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, John Field and Michael Hicks (Eds.). ACM, 337\u2013348. https:\/\/doi.org\/10.1145\/2103656.2103697"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.exmath.2019.02.004"},{"key":"e_1_3_2_1_28_1","volume-title":"Weak omega-categories from intensional type theory. Log. Methods Comput. Sci. 6, 3","author":"Lumsdaine LeFanu","year":"2010","unstructured":"Peter\u00a0 LeFanu Lumsdaine . 2010. Weak omega-categories from intensional type theory. Log. Methods Comput. Sci. 6, 3 ( 2010 ). https:\/\/doi.org\/10.2168\/LMCS-6(3:24)2010 10.2168\/LMCS-6(3:24)2010 Peter\u00a0LeFanu Lumsdaine. 2010. Weak omega-categories from intensional type theory. Log. Methods Comput. Sci. 6, 3 (2010). https:\/\/doi.org\/10.2168\/LMCS-6(3:24)2010"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2019.09.012"},{"key":"e_1_3_2_1_30_1","unstructured":"Andreas Nuyts. 2015. Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance. Master\u2019s thesis. KU Leuven. https:\/\/anuyts.github.io\/files\/mathesis.pdf  Andreas Nuyts. 2015. Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance. Master\u2019s thesis. KU Leuven. https:\/\/anuyts.github.io\/files\/mathesis.pdf"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785895"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.21136\/HS.2017.06"},{"key":"e_1_3_2_1_33_1","volume-title":"Proceedings of the Symposium on Logic in Computer Science (LICS \u201987)","author":"Seely Robert","year":"1987","unstructured":"Robert A.\u00a0G. Seely . 1987 . Modelling Computations: A 2-Categorical Framework . In Proceedings of the Symposium on Logic in Computer Science (LICS \u201987) , Ithaca, New York, USA , June 22-25, 1987. IEEE Computer Society, 65\u201371. Robert A.\u00a0G. Seely. 1987. Modelling Computations: A 2-Categorical Framework. In Proceedings of the Symposium on Logic in Computer Science (LICS \u201987), Ithaca, New York, USA, June 22-25, 1987. IEEE Computer Society, 65\u201371."},{"key":"e_1_3_2_1_34_1","unstructured":"Michael Shulman. 2010. Functorially Dependent Types. https:\/\/ncatlab.org\/michaelshulman\/show\/functorially+dependent+types  Michael Shulman. 2010. Functorially Dependent Types. https:\/\/ncatlab.org\/michaelshulman\/show\/functorially+dependent+types"},{"key":"e_1_3_2_1_35_1","unstructured":"Michael Shulman. 2011. Internal Logic of a 2-Category. https:\/\/ncatlab.org\/michaelshulman\/show\/internal+logic+of+a+2-category  Michael Shulman. 2011. Internal Logic of a 2-Category. https:\/\/ncatlab.org\/michaelshulman\/show\/internal+logic+of+a+2-category"},{"key":"e_1_3_2_1_36_1","unstructured":"Michael Shulman. 2012. 2-Categorical Logic. https:\/\/ncatlab.org\/michaelshulman\/show\/2-categorical+logic  Michael Shulman. 2012. 2-Categorical Logic. https:\/\/ncatlab.org\/michaelshulman\/show\/2-categorical+logic"},{"key":"e_1_3_2_1_37_1","unstructured":"Michael Shulman. 2019. Fibrational Slice. https:\/\/ncatlab.org\/michaelshulman\/show\/fibrational+slice  Michael Shulman. 2019. Fibrational Slice. https:\/\/ncatlab.org\/michaelshulman\/show\/fibrational+slice"},{"key":"e_1_3_2_1_38_1","volume-title":"Fibrations in bicategories. Cahiers de topologie et g\u00e9om\u00e9trie diff\u00e9rentielle cat\u00e9goriques 21, 2","author":"Street Ross","year":"1980","unstructured":"Ross Street . 1980. Fibrations in bicategories. Cahiers de topologie et g\u00e9om\u00e9trie diff\u00e9rentielle cat\u00e9goriques 21, 2 ( 1980 ), 111\u2013160. http:\/\/archive.numdam.org\/item\/CTGDC_1980__21_2_111_0\/ Ross Street. 1980. Fibrations in bicategories. Cahiers de topologie et g\u00e9om\u00e9trie diff\u00e9rentielle cat\u00e9goriques 21, 2 (1980), 111\u2013160. http:\/\/archive.numdam.org\/item\/CTGDC_1980__21_2_111_0\/"},{"key":"e_1_3_2_1_39_1","volume-title":"Category Theory(Lecture Notes in Mathematics, Vol.\u00a0962), K.H. Kamps, D.\u00a0Pumpl\u00fcn, and W.\u00a0Tholen (Eds.)","author":"Street Ross","unstructured":"Ross Street . 1982. Characterization of bicategories of stacks . In Category Theory(Lecture Notes in Mathematics, Vol.\u00a0962), K.H. Kamps, D.\u00a0Pumpl\u00fcn, and W.\u00a0Tholen (Eds.) . Springer . https:\/\/doi.org\/10.1007\/BFb0066909 10.1007\/BFb0066909 Ross Street. 1982. Characterization of bicategories of stacks. In Category Theory(Lecture Notes in Mathematics, Vol.\u00a0962), K.H. Kamps, D.\u00a0Pumpl\u00fcn, and W.\u00a0Tholen (Eds.). Springer. https:\/\/doi.org\/10.1007\/BFb0066909"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1960510.1960514"},{"key":"#cr-split#-e_1_3_2_1_41_1.1","unstructured":"The Coq\u00a0Development Team. 2022. The Coq Proof Assistant. https:\/\/doi.org\/10.5281\/zenodo.5846982 10.5281\/zenodo.5846982"},{"key":"#cr-split#-e_1_3_2_1_41_1.2","unstructured":"The Coq\u00a0Development Team. 2022. The Coq Proof Assistant. https:\/\/doi.org\/10.5281\/zenodo.5846982"},{"key":"e_1_3_2_1_42_1","unstructured":"Vladimir Voevodsky Benedikt Ahrens Daniel Grayson 2022. UniMath \u2014 a computer-checked library of univalent mathematics. Available at https:\/\/unimath.org. https:\/\/github.com\/UniMath\/UniMath  Vladimir Voevodsky Benedikt Ahrens Daniel Grayson 2022. UniMath \u2014 a computer-checked library of univalent mathematics. Available at https:\/\/unimath.org. https:\/\/github.com\/UniMath\/UniMath"},{"key":"e_1_3_2_1_43_1","volume-title":"35th Annual ACM\/IEEE Symposium on Logic in Computer Science","author":"Z.","year":"2020","unstructured":"Matthew\u00a0 Z. Weaver and Daniel\u00a0R. Licata. 2020. A Constructive Model of Directed Univalence in Bicubical Sets. In LICS \u201920 : 35th Annual ACM\/IEEE Symposium on Logic in Computer Science , Saarbr\u00fccken, Germany , July 8-11, 2020 , Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller (Eds.). ACM, 915\u2013928. https:\/\/doi.org\/10.1145\/3373718.3394794 10.1145\/3373718.3394794 Matthew\u00a0Z. Weaver and Daniel\u00a0R. Licata. 2020. A Constructive Model of Directed Univalence in Bicubical Sets. In LICS \u201920: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science, Saarbr\u00fccken, Germany, July 8-11, 2020, Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller (Eds.). ACM, 915\u2013928. https:\/\/doi.org\/10.1145\/3373718.3394794"}],"event":{"name":"LICS '22: 37th Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Haifa Israel","acronym":"LICS '22","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation"]},"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.3533334","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3531130.3533334","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3531130.3533334","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.3533334"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,2]]},"references-count":44,"alternative-id":["10.1145\/3531130.3533334","10.1145\/3531130"],"URL":"https:\/\/doi.org\/10.1145\/3531130.3533334","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"}}]}}