{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:18Z","timestamp":1747173438567,"version":"3.40.5"},"reference-count":46,"publisher":"Cambridge University Press (CUP)","issue":"7","license":[{"start":{"date-parts":[[2021,10,18]],"date-time":"2021-10-18T00:00:00Z","timestamp":1634515200000},"content-version":"unspecified","delay-in-days":78,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2021,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We prove a strictification theorem for cartesian closed bicategories. First, we adapt Power\u2019s proof of coherence for bicategories with finite bilimits to show that every bicategory with bicategorical cartesian closed structure is biequivalent to a 2-category with 2-categorical cartesian closed structure. Then we show how to extend this result to a Mac Lane-style \u201call pasting diagrams commute\u201d coherence theorem: precisely, we show that in the free cartesian closed bicategory on a graph, there is at most one 2-cell between any parallel pair of 1-cells. The argument we employ is reminiscent of that used by \u010cubri\u0107, Dybjer, and Scott to show normalisation for the simply-typed lambda calculus (\u010cubri\u0107 et al., 1998). The main results first appeared in a conference paper (Fiore and Saville, 2020) but for reasons of space many details are omitted there; here we provide the full development.<\/jats:p>","DOI":"10.1017\/s0960129521000281","type":"journal-article","created":{"date-parts":[[2021,10,19]],"date-time":"2021-10-19T10:17:34Z","timestamp":1634638654000},"page":"822-849","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":3,"title":["Coherence for bicategorical cartesian closed structure"],"prefix":"10.1017","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8558-3492","authenticated-orcid":false,"given":"Marcelo","family":"Fiore","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8320-0280","authenticated-orcid":false,"given":"Philip","family":"Saville","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2021,10,18]]},"reference":[{"key":"S0960129521000281_ref19","doi-asserted-by":"publisher","DOI":"10.1090\/memo\/1184"},{"key":"S0960129521000281_ref37","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(95)00029-1"},{"key":"S0960129521000281_ref17","unstructured":"Forest, S. and Mimram, S. (2018). Coherence of Gray categories via rewriting. In: 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik."},{"key":"S0960129521000281_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0074298"},{"key":"S0960129521000281_ref9","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1998.705658"},{"key":"S0960129521000281_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(87)90121-6"},{"key":"S0960129521000281_ref10","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129597002508"},{"key":"S0960129521000281_ref5","doi-asserted-by":"crossref","unstructured":"Borceux, F. (1994). Bicategories and Distributors, volume 1 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, 281\u2013324.","DOI":"10.1017\/CBO9780511525858.009"},{"key":"S0960129521000281_ref14","unstructured":"Fiore, M. and Joyal, A. 2015. Theory of para-toposes. Talk at the Category Theory 2015 Conference. Departamento de Matematica, Universidade de Aveiro (Portugal)."},{"key":"S0960129521000281_ref41","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(89)90113-8"},{"key":"S0960129521000281_ref29","first-page":"105","volume-title":"A 2-Categories Companion","author":"Lack","year":"2010"},{"key":"S0960129521000281_ref39","unstructured":"Paquet, H. (2020). Probabilistic concurrent game semantics. PhD thesis, University of Cambridge."},{"volume-title":"An Algebraic Theory of Tricategories","year":"2006","author":"Gurski","key":"S0960129521000281_ref22"},{"key":"S0960129521000281_ref42","unstructured":"Power, A. J. (1998). 2-categories. BRICS Notes Series."},{"key":"S0960129521000281_ref30","first-page":"1","article-title":"Bicategories of spans as cartesian bicategories","volume":"24","author":"Lack","year":"2010","journal-title":"Theory and Applications of Categories"},{"key":"S0960129521000281_ref34","unstructured":"Mac Lane, S. (1963). Natural associativity and commutativity. Rice University Studies."},{"key":"S0960129521000281_ref23","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139542333"},{"key":"S0960129521000281_ref35","unstructured":"Mac Lane, S. (1998). Categories for the Working Mathematician, vol. 5. Graduate Texts in Mathematics, second edition. Springer-Verlag New York."},{"key":"S0960129521000281_ref12","doi-asserted-by":"publisher","DOI":"10.1006\/aima.1997.1649"},{"key":"S0960129521000281_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(89)90160-6"},{"key":"S0960129521000281_ref28","unstructured":"Kelly, G. M. (1982). Basic Concepts of Enriched Category Theory. Number 64 in London Mathematical Society Lecture Note Series. Cambridge University Press."},{"key":"S0960129521000281_ref38","unstructured":"Ouaknine, J. (1997). A two-dimensional extension of Lambek\u2019s categorical proof theory. Master\u2019s thesis, McGill University."},{"key":"S0960129521000281_ref43","unstructured":"Saville, P. (2020). Cartesian closed bicategories: type theory and coherence. PhD thesis, University of Cambridge."},{"key":"S0960129521000281_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0061280"},{"key":"S0960129521000281_ref36","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(85)90087-8"},{"key":"S0960129521000281_ref25","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(3:10)2013"},{"key":"S0960129521000281_ref46","first-page":"111","article-title":"Fibrations in bicategories","volume":"21","author":"Street","year":"1980","journal-title":"Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques"},{"key":"S0960129521000281_ref33","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511525896"},{"key":"S0960129521000281_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)80713-4"},{"key":"S0960129521000281_ref45","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(72)90019-9"},{"key":"S0960129521000281_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(93)90035-R"},{"key":"S0960129521000281_ref32","unstructured":"Leinster, T. (1998). Basic Bicategories. Available at https:\/\/arxiv.org\/abs\/math\/9810017."},{"key":"S0960129521000281_ref13","doi-asserted-by":"publisher","DOI":"10.1112\/jlms\/jdm096"},{"key":"S0960129521000281_ref26","unstructured":"Houston, R. (2007). Linear Logic without Units. PhD thesis, University of Manchester."},{"key":"S0960129521000281_ref40","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/092\/1003207"},{"key":"S0960129521000281_ref27","doi-asserted-by":"publisher","DOI":"10.1006\/aima.1993.1055"},{"volume-title":"Introduction to Higher Order Categorical Logic","year":"1986","author":"Lambek","key":"S0960129521000281_ref31"},{"key":"S0960129521000281_ref18","unstructured":"Frey, J. (2019). A language for closed cartesian bicategories. Category Theory 2019, University of Edinburgh, Edinburgh, UK."},{"key":"S0960129521000281_ref3","doi-asserted-by":"publisher","DOI":"10.2307\/2273784"},{"key":"S0960129521000281_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0060438"},{"volume-title":"Memoirs of the American Mathematical Society","year":"2006","author":"Fiore","key":"S0960129521000281_ref16"},{"key":"S0960129521000281_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36576-1_2"},{"key":"S0960129521000281_ref44","first-page":"755","article-title":"Compact closed bicategories","volume":"31","author":"Stay","year":"2016","journal-title":"Theories and Applications of Categories"},{"key":"S0960129521000281_ref6","first-page":"93","article-title":"Cartesian bicategories II","volume":"19","author":"Carboni","year":"2008","journal-title":"Theory and Applications of Categories"},{"key":"S0960129521000281_ref20","doi-asserted-by":"publisher","DOI":"10.1090\/memo\/0558"},{"key":"S0960129521000281_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394769"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129521000281","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,28]],"date-time":"2022-02-28T12:57:25Z","timestamp":1646053045000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129521000281\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8]]},"references-count":46,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["S0960129521000281"],"URL":"https:\/\/doi.org\/10.1017\/s0960129521000281","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2021,8]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}