CINXE.COM
cartesian bicategory in nLab
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1 plus MathML 2.0 plus SVG 1.1//EN" "http://www.w3.org/2002/04/xhtml-math-svg/xhtml-math-svg-flat.dtd" > <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title> cartesian bicategory in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="index,follow" /> <meta name="viewport" content="width=device-width, initial-scale=1" /> <link href="/stylesheets/instiki.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/mathematics.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/syntax.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/nlab.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link rel="stylesheet" type="text/css" href="https://cdn.jsdelivr.net/gh/dreampulse/computer-modern-web-font@master/fonts.css"/> <style type="text/css"> h1#pageName, div.info, .newWikiWord a, a.existingWikiWord, .newWikiWord a:hover, [actiontype="toggle"]:hover, #TextileHelp h3 { color: #226622; } a:visited.existingWikiWord { color: #164416; } </style> <style type="text/css"><!--/*--><![CDATA[/*><!--*/ .toc ul {margin: 0; padding: 0;} .toc ul ul {margin: 0; padding: 0 0 0 10px;} .toc li > p {margin: 0} .toc ul li {list-style-type: none; position: relative;} .toc div {border-top:1px dotted #ccc;} .rightHandSide h2 {font-size: 1.5em;color:#008B26} table.plaintable { border-collapse:collapse; margin-left:30px; border:0; } .plaintable td {border:1px solid #000; padding: 3px;} .plaintable th {padding: 3px;} .plaintable caption { font-weight: bold; font-size:1.1em; text-align:center; margin-left:30px; } /* Query boxes for questioning and answering mechanism */ div.query{ background: #f6fff3; border: solid #ce9; border-width: 2px 1px; padding: 0 1em; margin: 0 1em; max-height: 20em; overflow: auto; } /* Standout boxes for putting important text */ div.standout{ background: #fff1f1; border: solid black; border-width: 2px 1px; padding: 0 1em; margin: 0 1em; overflow: auto; } /* Icon for links to n-category arXiv documents (commented out for now i.e. disabled) a[href*="http://arxiv.org/"] { background-image: url(../files/arXiv_icon.gif); background-repeat: no-repeat; background-position: right bottom; padding-right: 22px; } */ /* Icon for links to n-category cafe posts (disabled) a[href*="http://golem.ph.utexas.edu/category"] { background-image: url(../files/n-cafe_5.gif); background-repeat: no-repeat; background-position: right bottom; padding-right: 25px; } */ /* Icon for links to pdf files (disabled) a[href$=".pdf"] { background-image: url(../files/pdficon_small.gif); background-repeat: no-repeat; background-position: right bottom; padding-right: 25px; } */ /* Icon for links to pages, etc. -inside- pdf files (disabled) a[href*=".pdf#"] { background-image: url(../files/pdf_entry.gif); background-repeat: no-repeat; background-position: right bottom; padding-right: 25px; } */ a.existingWikiWord { color: #226622; } a.existingWikiWord:visited { color: #226622; } a.existingWikiWord[title] { border: 0px; color: #aa0505; text-decoration: none; } a.existingWikiWord[title]:visited { border: 0px; color: #551111; text-decoration: none; } a[href^="http://"] { border: 0px; color: #003399; } a[href^="http://"]:visited { border: 0px; color: #330066; } a[href^="https://"] { border: 0px; color: #003399; } a[href^="https://"]:visited { border: 0px; color: #330066; } div.dropDown .hide { display: none; } div.dropDown:hover .hide { display:block; } div.clickDown .hide { display: none; } div.clickDown:focus { outline:none; } div.clickDown:focus .hide, div.clickDown:hover .hide { display: block; } div.clickDown .clickToReveal, div.clickDown:focus .clickToHide { display:block; } div.clickDown:focus .clickToReveal, div.clickDown .clickToHide { display:none; } div.clickDown .clickToReveal:after { content: "A(Hover to reveal, click to "hold")"; font-size: 60%; } div.clickDown .clickToHide:after { content: "A(Click to hide)"; font-size: 60%; } div.clickDown .clickToHide, div.clickDown .clickToReveal { white-space: pre-wrap; } .un_theorem, .num_theorem, .un_lemma, .num_lemma, .un_prop, .num_prop, .un_cor, .num_cor, .un_defn, .num_defn, .un_example, .num_example, .un_note, .num_note, .un_remark, .num_remark { margin-left: 1em; } span.theorem_label { margin-left: -1em; } .proof span.theorem_label { margin-left: 0em; } :target { background-color: #BBBBBB; border-radius: 5pt; } /*]]>*/--></style> <script src="/javascripts/prototype.js?1660229990" type="text/javascript"></script> <script src="/javascripts/effects.js?1660229990" type="text/javascript"></script> <script src="/javascripts/dragdrop.js?1660229990" type="text/javascript"></script> <script src="/javascripts/controls.js?1660229990" type="text/javascript"></script> <script src="/javascripts/application.js?1660229990" type="text/javascript"></script> <script src="/javascripts/page_helper.js?1660229990" type="text/javascript"></script> <script src="/javascripts/thm_numbering.js?1660229990" type="text/javascript"></script> <script type="text/x-mathjax-config"> <!--//--><![CDATA[//><!-- MathJax.Ajax.config.path["Contrib"] = "/MathJax"; MathJax.Hub.Config({ MathML: { useMathMLspacing: true }, "HTML-CSS": { scale: 90, extensions: ["handle-floats.js"] } }); MathJax.Hub.Queue( function () { var fos = document.getElementsByTagName('foreignObject'); for (var i = 0; i < fos.length; i++) { MathJax.Hub.Typeset(fos[i]); } }); //--><!]]> </script> <script type="text/javascript"> <!--//--><![CDATA[//><!-- window.addEventListener("DOMContentLoaded", function () { var div = document.createElement('div'); var math = document.createElementNS('http://www.w3.org/1998/Math/MathML', 'math'); document.body.appendChild(div); div.appendChild(math); // Test for MathML support comparable to WebKit version https://trac.webkit.org/changeset/203640 or higher. div.setAttribute('style', 'font-style: italic'); var mathml_unsupported = !(window.getComputedStyle(div.firstChild).getPropertyValue('font-style') === 'normal'); div.parentNode.removeChild(div); if (mathml_unsupported) { // MathML does not seem to be supported... var s = document.createElement('script'); s.src = "https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.7/MathJax.js?config=MML_HTMLorMML-full"; document.querySelector('head').appendChild(s); } else { document.head.insertAdjacentHTML("beforeend", '<style>svg[viewBox] {max-width: 100%}</style>'); } }); //--><!]]> </script> <link href="https://ncatlab.org/nlab/atom_with_headlines" rel="alternate" title="Atom with headlines" type="application/atom+xml" /> <link href="https://ncatlab.org/nlab/atom_with_content" rel="alternate" title="Atom with full content" type="application/atom+xml" /> <script type="text/javascript"> document.observe("dom:loaded", function() { generateThmNumbers(); }); </script> </head> <body> <div id="Container"> <div id="Content"> <h1 id="pageName"> <span style="float: left; margin: 0.5em 0.25em -0.25em 0"> <svg xmlns="http://www.w3.org/2000/svg" width="1.872em" height="1.8em" viewBox="0 0 190 181"> <path fill="#226622" d="M72.8 145c-1.6 17.3-15.7 10-23.6 20.2-5.6 7.3 4.8 15 11.4 15 11.5-.2 19-13.4 26.4-20.3 3.3-3 8.2-4 11.2-7.2a14 14 0 0 0 2.9-11.1c-1.4-9.6-12.4-18.6-16.9-27.2-5-9.6-10.7-27.4-24.1-27.7-17.4-.3-.4 26 4.7 30.7 2.4 2.3 5.4 4.1 7.3 6.9 1.6 2.3 2.1 5.8-1 7.2-5.9 2.6-12.4-6.3-15.5-10-8.8-10.6-15.5-23-26.2-31.8-5.2-4.3-11.8-8-18-3.7-7.3 4.9-4.2 12.9.2 18.5a81 81 0 0 0 30.7 23c3.3 1.5 12.8 5.6 10 10.7-2.5 5.2-11.7 3-15.6 1.1-8.4-3.8-24.3-21.3-34.4-13.7-3.5 2.6-2.3 7.6-1.2 11.1 2.8 9 12.2 17.2 20.9 20.5 17.3 6.7 34.3-8 50.8-12.1z"/> <path fill="#a41e32" d="M145.9 121.3c-.2-7.5 0-19.6-4.5-26-5.4-7.5-12.9-1-14.1 5.8-1.4 7.8 2.7 14.1 4.8 21.3 3.4 12 5.8 29-.8 40.1-3.6-6.7-5.2-13-7-20.4-2.1-8.2-12.8-13.2-15.1-1.9-2 9.7 9 21.2 12 30.1 1.2 4 2 8.8 6.4 10.3 6.9 2.3 13.3-4.7 17.7-8.8 12.2-11.5 36.6-20.7 43.4-36.4 6.7-15.7-13.7-14-21.3-7.2-9.1 8-11.9 20.5-23.6 25.1 7.5-23.7 31.8-37.6 38.4-61.4 2-7.3-.8-29.6-13-19.8-14.5 11.6-6.6 37.6-23.3 49.2z"/> <path fill="#193c78" d="M86.3 47.5c0-13-10.2-27.6-5.8-40.4 2.8-8.4 14.1-10.1 17-1 3.8 11.6-.3 26.3-1.8 38 11.7-.7 10.5-16 14.8-24.3 2.1-4.2 5.7-9.1 11-6.7 6 2.7 7.4 9.2 6.6 15.1-2.2 14-12.2 18.8-22.4 27-3.4 2.7-8 6.6-5.9 11.6 2 4.4 7 4.5 10.7 2.8 7.4-3.3 13.4-16.5 21.7-16 14.6.7 12 21.9.9 26.2-5 1.9-10.2 2.3-15.2 3.9-5.8 1.8-9.4 8.7-15.7 8.9-6.1.1-9-6.9-14.3-9-14.4-6-33.3-2-44.7-14.7-3.7-4.2-9.6-12-4.9-17.4 9.3-10.7 28 7.2 35.7 12 2 1.1 11 6.9 11.4 1.1.4-5.2-10-8.2-13.5-10-11.1-5.2-30-15.3-35-27.3-2.5-6 2.8-13.8 9.4-13.6 6.9.2 13.4 7 17.5 12C70.9 34 75 43.8 86.3 47.4z"/> </svg> </span> <span class="webName">nLab</span> cartesian bicategory </h1> <div class="navigation"> <span class="skipNav"><a href='#navEnd'>Skip the Navigation Links</a> | </span> <span style="display:inline-block; width: 0.3em;"></span> <a href="/nlab/show/HomePage" accesskey="H" title="Home page">Home Page</a> | <a href="/nlab/all_pages" accesskey="A" title="List of all pages">All Pages</a> | <a href="/nlab/latest_revisions" accesskey="U" title="Latest edits and page creations">Latest Revisions</a> | <a href="https://nforum.ncatlab.org/discussion/11463/#Item_4" title="Discuss this page in its dedicated thread on the nForum" style="color: black">Discuss this page</a> | <form accept-charset="utf-8" action="/nlab/search" id="navigationSearchForm" method="get"> <fieldset class="search"><input type="text" id="searchField" name="query" value="Search" style="display:inline-block; float: left;" onfocus="this.value == 'Search' ? this.value = '' : true" onblur="this.value == '' ? this.value = 'Search' : true" /></fieldset> </form> <span id='navEnd'></span> </div> <div id="revision"> <html xmlns="http://www.w3.org/1999/xhtml" xmlns:svg="http://www.w3.org/2000/svg" xml:lang="en" lang="en"> <head><meta http-equiv="Content-type" content="application/xhtml+xml;charset=utf-8" /><title>Contents</title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <h4 id="2category_theory">2-Category theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/2-category+theory">2-category theory</a></strong></p> <p><strong>Definitions</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/2-category">2-category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/strict+2-category">strict 2-category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/bicategory">bicategory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/enriched+bicategory">enriched bicategory</a></p> </li> </ul> <p><strong>Transfors between 2-categories</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/2-functor">2-functor</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/pseudofunctor">pseudofunctor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/lax+functor">lax functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/equivalence+of+2-categories">equivalence of 2-categories</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/2-natural+transformation">2-natural transformation</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/lax+natural+transformation">lax natural transformation</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/icon">icon</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/modification">modification</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Yoneda+lemma+for+bicategories">Yoneda lemma for bicategories</a></p> </li> </ul> <p><strong>Morphisms in 2-categories</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/fully+faithful+morphism">fully faithful morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/faithful+morphism">faithful morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/conservative+morphism">conservative morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/pseudomonic+morphism">pseudomonic morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/discrete+morphism">discrete morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/eso+morphism">eso morphism</a></p> </li> </ul> <p><strong>Structures in 2-categories</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/adjunction">adjunction</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/mate">mate</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/monad">monad</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cartesian+object">cartesian object</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/fibration+in+a+2-category">fibration in a 2-category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/codiscrete+cofibration">codiscrete cofibration</a></p> </li> </ul> <p><strong>Limits in 2-categories</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/2-limit">2-limit</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/2-pullback">2-pullback</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/comma+object">comma object</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/inserter">inserter</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/inverter">inverter</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/equifier">equifier</a></p> </li> </ul> <p><strong>Structures on 2-categories</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/2-monad">2-monad</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/lax-idempotent+2-monad">lax-idempotent 2-monad</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/pseudomonad">pseudomonad</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/pseudoalgebra+for+a+2-monad">pseudoalgebra for a 2-monad</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/monoidal+2-category">monoidal 2-category</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/cartesian+bicategory">cartesian bicategory</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Gray+tensor+product">Gray tensor product</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/proarrow+equipment">proarrow equipment</a></p> </li> </ul> </div></div> <h4 id="monoidal_categories">Monoidal categories</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/monoidal+categories">monoidal categories</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/enriched+monoidal+category">enriched monoidal category</a>, <a class="existingWikiWord" href="/nlab/show/tensor+category">tensor category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/string+diagram">string diagram</a>, <a class="existingWikiWord" href="/nlab/show/tensor+network">tensor network</a></p> </li> </ul> <p><strong>With braiding</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/braided+monoidal+category">braided monoidal category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/balanced+monoidal+category">balanced monoidal category</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/twist">twist</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+category">symmetric monoidal category</a></p> </li> </ul> <p><strong>With duals for objects</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/category+with+duals">category with duals</a> (list of them)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/dualizable+object">dualizable object</a> (what they have)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/rigid+monoidal+category">rigid monoidal category</a>, a.k.a. <a class="existingWikiWord" href="/nlab/show/autonomous+category">autonomous category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/pivotal+category">pivotal category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/spherical+category">spherical category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/ribbon+category">ribbon category</a>, a.k.a. <a class="existingWikiWord" href="/nlab/show/tortile+category">tortile category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/compact+closed+category">compact closed category</a></p> </li> </ul> <p><strong>With duals for morphisms</strong></p> <ul> <li> <p><span class="newWikiWord">monoidal dagger-category<a href="/nlab/new/monoidal+dagger-category">?</a></span></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+dagger-category">symmetric monoidal dagger-category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/dagger+compact+category">dagger compact category</a></p> </li> </ul> <p><strong>With traces</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/trace">trace</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/traced+monoidal+category">traced monoidal category</a></p> </li> </ul> <p><strong>Closed structure</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/closed+monoidal+category">closed monoidal category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cartesian+closed+category">cartesian closed category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/closed+category">closed category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/star-autonomous+category">star-autonomous category</a></p> </li> </ul> <p><strong>Special sorts of products</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/cartesian+monoidal+category">cartesian monoidal category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/semicartesian+monoidal+category">semicartesian monoidal category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/monoidal+category+with+diagonals">monoidal category with diagonals</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/multicategory">multicategory</a></p> </li> </ul> <p><strong>Semisimplicity</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/semisimple+category">semisimple category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/fusion+category">fusion category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/modular+tensor+category">modular tensor category</a></p> </li> </ul> <p><strong>Morphisms</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/monoidal+functor">monoidal functor</a></p> <p>(<a class="existingWikiWord" href="/nlab/show/lax+monoidal+functor">lax</a>, <a class="existingWikiWord" href="/nlab/show/oplax+monoidal+functor">oplax</a>, <a class="existingWikiWord" href="/nlab/show/strong+monoidal+functor">strong</a> <a class="existingWikiWord" href="/nlab/show/bilax+monoidal+functor">bilax</a>, <a class="existingWikiWord" href="/nlab/show/Frobenius+monoidal+functor">Frobenius</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/braided+monoidal+functor">braided monoidal functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+functor">symmetric monoidal functor</a></p> </li> </ul> <p><strong>Internal monoids</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/monoid+in+a+monoidal+category">monoid in a monoidal category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/commutative+monoid+in+a+symmetric+monoidal+category">commutative monoid in a symmetric monoidal category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/module+over+a+monoid">module over a monoid</a></p> </li> </ul> <p><strong id="_examples">Examples</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/tensor+product">tensor product</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/closed+monoidal+structure+on+presheaves">closed monoidal structure on presheaves</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Day+convolution">Day convolution</a></p> </li> </ul> <p><strong>Theorems</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/coherence+theorem+for+monoidal+categories">coherence theorem for monoidal categories</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/monoidal+Dold-Kan+correspondence">monoidal Dold-Kan correspondence</a></p> </li> </ul> <p><strong>In higher category theory</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/monoidal+2-category">monoidal 2-category</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/braided+monoidal+2-category">braided monoidal 2-category</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/monoidal+bicategory">monoidal bicategory</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/cartesian+bicategory">cartesian bicategory</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/k-tuply+monoidal+n-category">k-tuply monoidal n-category</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/little+cubes+operad">little cubes operad</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/monoidal+%28%E2%88%9E%2C1%29-category">monoidal (∞,1)-category</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+%28%E2%88%9E%2C1%29-category">symmetric monoidal (∞,1)-category</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/compact+double+category">compact double category</a></p> </li> </ul> </div></div> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <li><a href='#technical_preliminaries'>Technical preliminaries</a></li> <ul> <li><a href='#2adjunctions_between_2categories'>2-adjunctions between 2-categories</a></li> <li><a href='#lax_adjunctions_between_2categories'>Lax adjunctions between 2-categories</a></li> <li><a href='#the_2category_'>The 2-category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math></a></li> </ul> <li><a href='#definition_of_cartesian_structure_and_basic_results'>Definition of cartesian structure and basic results</a></li> <ul> <li><a href='#symmetric_monoidal_structure_via_cartesian_structure'>Symmetric monoidal structure via cartesian structure</a></li> <li><a href='#comparison_with_carboniwalters'>Comparison with Carboni-Walters</a></li> <li><a href='#local_cartesian_products'>Local cartesian products</a></li> <li><a href='#essential_uniqueness_of_cartesian_structure'>Essential uniqueness of cartesian structure</a></li> </ul> <li><a href='#cartesian_bicategories_and_hyperdoctrines'>Cartesian bicategories and hyperdoctrines</a></li> <li><a href='#frobenius'>Frobenius conditions</a></li> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="idea">Idea</h2> <p>A <strong>cartesian bicategory</strong> is a <a class="existingWikiWord" href="/nlab/show/bicategory">bicategory</a> with properties that make it behave like a bicategory of generalized <a class="existingWikiWord" href="/nlab/show/relations">relations</a>.</p> <p>Examples of cartesian bicategories include</p> <ul> <li>the bicategory <a class="existingWikiWord" href="/nlab/show/Rel">Rel</a> of sets and relations,</li> <li>more generally, the <a class="existingWikiWord" href="/nlab/show/bicategory+of+relations">bicategory of relations</a> of a <a class="existingWikiWord" href="/nlab/show/regular+category">regular category</a>,</li> <li>the bicategory <a class="existingWikiWord" href="/nlab/show/Span">Span</a> of sets and spans,</li> <li>more generally, the bicategory of <a class="existingWikiWord" href="/nlab/show/spans">spans</a> in a finitely <a class="existingWikiWord" href="/nlab/show/complete+category">complete category</a>,</li> <li>the bicategory <a class="existingWikiWord" href="/nlab/show/profunctor">Prof</a> of (small) categories and profunctors,</li> <li>more generally, the bicategory of internal categories and <a class="existingWikiWord" href="/nlab/show/modules">modules</a> (<a class="existingWikiWord" href="/nlab/show/profunctors">profunctors</a>) in a finitely complete category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>,</li> <li>as an alternative generalization, the bicategory of enriched categories and modules over a <em>cartesian</em> monoidal category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math>.</li> </ul> <p>Non-examples include</p> <ul> <li>the locally-discrete bicategory <a class="existingWikiWord" href="/nlab/show/Set">Set</a> of sets and functions,</li> <li>the bicategory <a class="existingWikiWord" href="/nlab/show/Cat">Cat</a> of categories and functors,</li> <li>the bicategory of profunctors and enriched in a <em>noncartesian</em> monoidal category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math>.</li> </ul> <p>Consider for example the bicategory <a class="existingWikiWord" href="/nlab/show/Rel">Rel</a>. This bicategory admits a symmetric monoidal structure given by the cartesian product. Because the cartesian product is <em>not</em> the categorical product, this symmetric monoidal structure is <em>not</em> <a class="existingWikiWord" href="/nlab/show/cartesian+monoidal+category">cartesian monoidal</a>. However, the cartesian product restricts to the locally-discrete sub-bicategory <a class="existingWikiWord" href="/nlab/show/Set">Set</a> of sets and functions, on which it <em>is</em> the categorical product. Note that a relation is the graph of a function if and only if it possesses a right adjoint (which is given by the opposite relation). In a general bicategory, a 1-cell is called <em>map-like</em> if it possesses a right adjoint, and these are the 1-cells playing the role that functions play in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Rel</mi></mrow><annotation encoding="application/x-tex">Rel</annotation></semantics></math>.</p> <p>Generalizing this situation, a cartesian bicategory <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> is a symmetric monoidal bicategory for which the monoidal product restricts to the categorical product on the sub-bicategory of map-like 1-cells, subject to natural compatibility conditions. Remarkably, the structure of such a tensor is <a class="existingWikiWord" href="/nlab/show/property-like+structure">property-like</a> (is essentially unique when it exists). Thus the definition can be formulated directly in terms of the bicategory <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> without mentioning a symmetric monoidal structure at all. Not only is this technically convenient (as the precise definition of a symmetric monoidal bicategory is quite technical), but it is moreover a very natural perspective to take.</p> <p>Like allegories, cartesian bicategories provide a convenient abstract setting in which to study the calculus of relations, but unlike allegories they embrace higher examples like <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Span</mi></mrow><annotation encoding="application/x-tex">Span</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Mod</mi></mrow><annotation encoding="application/x-tex">Mod</annotation></semantics></math>. The original idea, as explained by Carboni and Walters in their paper, clearly had these various examples in mind but was initially confined to the locally posetal case; in part this was due to the lack at the time (circa 1987) of a complete definition of symmetric monoidal bicategories. In more recent years a full bicategorical treatment has emerged, due principally to Carboni, Kelly, Verity, and Wood. The alternative treatment we give below has not yet appeared in the literature as far as this author (<a class="existingWikiWord" href="/nlab/show/Todd+Trimble">Todd Trimble</a>) is aware.</p> <h2 id="technical_preliminaries">Technical preliminaries</h2> <p>Note: All compositions will be written in the traditional order, in which application proceeds from right to left.</p> <p>We work with familiar notions of the theory of bicategories (which, for reasons of consonance with 2-terminology, we also call 2-categories) but in some cases under new names. We calculate with pasting diagrams in 2-categories as if they were strict 2-categories.</p> <p>Our notion of morphism between 2-categories has gone under various names: “homomorphism” in the sense of Bénabou, also known as “pseudofunctor” or weak 2-functor, where the structural constraints are isomorphisms. Here they are simply called <strong>2-functors</strong>.</p> <p>Each 2-category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> gives rise to a hom 2-functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>hom</mi><mo>:</mo><msup><mi>B</mi> <mi>op</mi></msup><mo>×</mo><mi>B</mi><mo>→</mo><mi>Cat</mi></mrow><annotation encoding="application/x-tex">hom: B^{op} \times B \to Cat</annotation></semantics></math>, which we denote by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">B(-, -)</annotation></semantics></math>, with the contravariant argument in the first place as is customary.</p> <p>Given 2-functors <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo>,</mo><mi>G</mi><mo>:</mo><mi>B</mi><mo>→</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">F, G: B \to C</annotation></semantics></math>, it is for our purposes convenient to use the <a class="existingWikiWord" href="/nlab/show/lax+natural+transformation">lax notion of morphism</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>θ</mi><mo>:</mo><mi>F</mi><mo>→</mo><mi>G</mi></mrow><annotation encoding="application/x-tex">\theta: F \to G</annotation></semantics></math> between 2-functors for which the structural cells <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>θ</mi><mo>⋅</mo><mi>f</mi></mrow><annotation encoding="application/x-tex">\theta \cdot f</annotation></semantics></math> (for 1-cells <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>a</mi><mo>→</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">f: a \to b</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>) point in the direction</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>F</mi><mi>a</mi></mtd> <mtd><mover><mo>→</mo><mrow><mi>θ</mi><mi>a</mi></mrow></mover></mtd> <mtd><mi>G</mi><mi>a</mi></mtd></mtr> <mtr><mtd><mi>F</mi><mi>f</mi><mo stretchy="false">↓</mo></mtd> <mtd><mover><mo>⇒</mo><mrow><mi>θ</mi><mo>⋅</mo><mi>f</mi></mrow></mover></mtd> <mtd><mo stretchy="false">↓</mo><mi>G</mi><mi>f</mi></mtd></mtr> <mtr><mtd><mi>F</mi><mi>b</mi></mtd> <mtd><munder><mo>→</mo><mrow><mi>θ</mi><mi>b</mi></mrow></munder></mtd> <mtd><mi>G</mi><mi>b</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ F a & \overset{\theta a}{\to} & G a\\ F f \downarrow & \overset{\theta \cdot f}{\Rightarrow} & \downarrow G f\\ F b & \underset{\theta b}{\to} & G b } </annotation></semantics></math></div> <p>These are called “oplax transformations” by some authors such as Bénabou and “lax transformations” by other authors such as Johnstone; on this page we will simply call them (2-)<strong>transformations</strong>. A transformation is <strong>strong</strong> if the structural cells <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>θ</mi><mo>⋅</mo><mi>f</mi></mrow><annotation encoding="application/x-tex">\theta \cdot f</annotation></semantics></math> are isomorphisms.</p> <p>There is a well-known notion of morphism between transformation which has been called <a class="existingWikiWord" href="/nlab/show/modification">modification</a>. We retain this usage, but as an aside we counsel against inventing a new term (e.g., “perturbation” between modifications) every time a new level of morphism is reached – a more uniform terminology is called for. The term “transfor” (due to Sjoerd Crans) has been tentatively adopted elsewhere on this site; modifications may then be called <strong>2-transfors</strong>.</p> <p>In any case, given 2-categories <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>, there is a 2-category of 2-functors, strong transformations and modifications from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>; this will be denoted <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Hom</mi> <mi>s</mi></msub><mo stretchy="false">(</mo><mi>B</mi><mo>,</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Hom_s(B, C)</annotation></semantics></math>. We have also the 2-category of 2-functors, transformations, and modifications; this will be denoted <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Hom</mi> <mi>l</mi></msub><mo stretchy="false">(</mo><mi>B</mi><mo>,</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Hom_l(B, C)</annotation></semantics></math>.</p> <h3 id="2adjunctions_between_2categories">2-adjunctions between 2-categories</h3> <p>A <strong>2-adjunction</strong> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo>⊣</mo><mi>G</mi></mrow><annotation encoding="application/x-tex">F \dashv G</annotation></semantics></math> consists of 2-functors <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo>:</mo><mi>B</mi><mo>→</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">F: B \to C</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo>:</mo><mi>C</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">G: C \to B</annotation></semantics></math>, and an adjoint equivalence</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo stretchy="false">(</mo><mi>F</mi><mo>−</mo><mo>,</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo><mo>≃</mo><mi>B</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>G</mi><mo>−</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">C(F -, -) \simeq B(-, G -)</annotation></semantics></math></div> <p>in the 2-category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Hom</mi> <mi>s</mi></msub><mo stretchy="false">(</mo><msup><mi>B</mi> <mi>op</mi></msup><mo>×</mo><mi>C</mi><mo>,</mo><mi>Cat</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Hom_s(B^{op} \times C, Cat)</annotation></semantics></math>. In more elementary terms, the data of a 2-adjunction is given by strong transformations</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>η</mi><mo>:</mo><msub><mn>1</mn> <mi>B</mi></msub><mo>→</mo><mi>G</mi><mi>F</mi><mspace width="2em"></mspace><mi>ε</mi><mo>:</mo><mi>F</mi><mi>G</mi><mo>→</mo><msub><mn>1</mn> <mi>C</mi></msub></mrow><annotation encoding="application/x-tex">\eta: 1_B \to G F \qquad \varepsilon: F G \to 1_C</annotation></semantics></math></div> <p>and invertible modifications (called <em>triangulators</em>)</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>G</mi></mtd> <mtd><mover><mo>→</mo><mrow><mi>η</mi><mi>G</mi></mrow></mover></mtd> <mtd><mi>G</mi><mi>F</mi><mi>G</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>F</mi></mtd> <mtd><mover><mo>→</mo><mrow><mi>F</mi><mi>η</mi></mrow></mover></mtd> <mtd><mi>F</mi><mi>G</mi><mi>F</mi></mtd></mtr> <mtr><mtd><msub><mn>1</mn> <mi>G</mi></msub><mo stretchy="false">↓</mo></mtd> <mtd><mover><mo>⇒</mo><mi>s</mi></mover></mtd> <mtd><mo stretchy="false">↓</mo><mi>G</mi><mi>ε</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><msub><mn>1</mn> <mi>F</mi></msub><mo stretchy="false">↓</mo></mtd> <mtd><mover><mo>⇐</mo><mi>t</mi></mover></mtd> <mtd><mo stretchy="false">↓</mo><mi>ε</mi><mi>F</mi></mtd></mtr> <mtr><mtd><mi>G</mi></mtd> <mtd><munder><mo>→</mo><mrow><msub><mn>1</mn> <mi>G</mi></msub></mrow></munder></mtd> <mtd><mi>G</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>F</mi></mtd> <mtd><munder><mo>→</mo><mrow><msub><mn>1</mn> <mi>F</mi></msub></mrow></munder></mtd> <mtd><mi>F</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ G & \overset{\eta G}{\to} & G F G & & & & F & \overset{F\eta}{\to} & F G F\\ 1_G \downarrow & \overset{s}{\Rightarrow} & \downarrow G \varepsilon & & & & 1_F \downarrow & \overset{t}{\Leftarrow} & \downarrow \varepsilon F\\ G & \underset{1_G}{\to} & G & & & & F & \underset{1_F}{\to} & F } </annotation></semantics></math></div> <p>such that the <em>triangulator coherence conditions</em> hold: there are pasting diagram equalities</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><msub><mn>1</mn> <mi>B</mi></msub></mtd> <mtd><mover><mo>→</mo><mi>η</mi></mover></mtd> <mtd><mi>G</mi><mi>F</mi></mtd> <mtd><mover><mo>→</mo><mrow><msub><mn>1</mn> <mrow><mi>G</mi><mi>F</mi></mrow></msub></mrow></mover></mtd> <mtd><mi>G</mi><mi>F</mi></mtd></mtr> <mtr><mtd><mi>η</mi><mo stretchy="false">↓</mo></mtd> <mtd><mover><mo>⇒</mo><mrow><mi>η</mi><mo>⋅</mo><mi>η</mi></mrow></mover></mtd> <mtd><mo stretchy="false">↓</mo><mi>G</mi><mi>F</mi><mi>η</mi></mtd> <mtd></mtd> <mtd><mo stretchy="false">↓</mo><msub><mn>1</mn> <mrow><mi>G</mi><mi>F</mi></mrow></msub></mtd></mtr> <mtr><mtd><mi>G</mi><mi>F</mi></mtd> <mtd><munder><mo>→</mo><mrow><mi>η</mi><mi>G</mi><mi>F</mi></mrow></munder></mtd> <mtd><mi>G</mi><mi>F</mi><mi>G</mi><mi>F</mi></mtd> <mtd><mover><mo>⇒</mo><mrow><mi>G</mi><mi>t</mi></mrow></mover></mtd> <mtd><mi>G</mi><mi>F</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd><mo>=</mo></mtd> <mtd><msub><mn>1</mn> <mi>η</mi></msub></mtd></mtr> <mtr><mtd><msub><mn>1</mn> <mrow><mi>G</mi><mi>F</mi></mrow></msub><mo stretchy="false">↓</mo></mtd> <mtd></mtd> <mtd><mover><mo>⇒</mo><mrow><mi>s</mi><mi>F</mi></mrow></mover></mtd> <mtd><mi>G</mi><mi>ε</mi><mi>F</mi><mo>↘</mo></mtd> <mtd><mo stretchy="false">↓</mo><msub><mn>1</mn> <mrow><mi>G</mi><mi>F</mi></mrow></msub></mtd></mtr> <mtr><mtd><mi>G</mi><mi>F</mi></mtd> <mtd><munder><mo>→</mo><mrow><msub><mn>1</mn> <mrow><mi>G</mi><mi>F</mi></mrow></msub></mrow></munder></mtd> <mtd><mi>G</mi><mi>F</mi></mtd> <mtd><munder><mo>→</mo><mrow><msub><mn>1</mn> <mrow><mi>G</mi><mi>F</mi></mrow></msub></mrow></munder></mtd> <mtd><mi>G</mi><mi>F</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ 1_B & \overset{\eta}{\to} & G F & \overset{1_{G F}}{\to} & G F\\ \eta \downarrow & \overset{\eta \cdot \eta}{\Rightarrow} & \downarrow G F \eta & & \downarrow 1_{G F}\\ G F & \underset{\eta G F}{\to} & G F G F & \overset{G t}{\Rightarrow} & G F & & & = & 1_{\eta}\\ 1_{G F} \downarrow & & \overset{s F}{\Rightarrow} & G \varepsilon F \searrow & \downarrow 1_{G F} \\ G F & \underset{1_{G F}}{\to} & G F & \underset{1_{G F}}{\to} & G F } </annotation></semantics></math></div> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mspace width="thinmathspace"></mspace></mrow><annotation encoding="application/x-tex">\, </annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>F</mi><mi>G</mi></mtd> <mtd><mover><mo>→</mo><mrow><msub><mn>1</mn> <mrow><mi>F</mi><mi>G</mi></mrow></msub></mrow></mover></mtd> <mtd><mi>F</mi><mi>G</mi></mtd> <mtd><mover><mo>→</mo><mrow><msub><mn>1</mn> <mrow><mi>F</mi><mi>G</mi></mrow></msub></mrow></mover></mtd> <mtd><mi>F</mi><mi>G</mi></mtd></mtr> <mtr><mtd><msub><mn>1</mn> <mrow><mi>F</mi><mi>G</mi></mrow></msub><mo stretchy="false">↓</mo></mtd> <mtd><mi>F</mi><mi>η</mi><mi>G</mi><mo>↘</mo></mtd> <mtd><mover><mo>⇒</mo><mrow><mi>t</mi><mi>G</mi></mrow></mover></mtd> <mtd></mtd> <mtd><mo stretchy="false">↓</mo><msub><mn>1</mn> <mrow><mi>F</mi><mi>G</mi></mrow></msub></mtd></mtr> <mtr><mtd><mi>F</mi><mi>G</mi></mtd> <mtd><mover><mo>⇒</mo><mrow><mi>F</mi><mi>s</mi></mrow></mover></mtd> <mtd><mi>F</mi><mi>G</mi><mi>F</mi><mi>G</mi></mtd> <mtd><mover><mo>→</mo><mrow><mi>ε</mi><mi>F</mi><mi>G</mi></mrow></mover></mtd> <mtd><mi>F</mi><mi>G</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd><mo>=</mo></mtd> <mtd><msub><mn>1</mn> <mi>ε</mi></msub></mtd></mtr> <mtr><mtd><msub><mn>1</mn> <mrow><mi>F</mi><mi>G</mi></mrow></msub><mo stretchy="false">↓</mo></mtd> <mtd></mtd> <mtd><mi>F</mi><mi>G</mi><mi>ε</mi><mo stretchy="false">↓</mo></mtd> <mtd><mover><mo>⇒</mo><mrow><mi>ε</mi><mo>⋅</mo><mi>ε</mi></mrow></mover></mtd> <mtd><mo stretchy="false">↓</mo><mi>ε</mi></mtd></mtr> <mtr><mtd><mi>F</mi><mi>G</mi></mtd> <mtd><munder><mo>→</mo><mrow><msub><mn>1</mn> <mrow><mi>F</mi><mi>G</mi></mrow></msub></mrow></munder></mtd> <mtd><mi>F</mi><mi>G</mi></mtd> <mtd><munder><mo>→</mo><mi>ε</mi></munder></mtd> <mtd><mn>1</mn></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ F G & \overset{1_{F G}}{\to} & F G & \overset{1_{F G}}{\to} & F G\\ 1_{F G} \downarrow & F \eta G \searrow & \overset{t G}{\Rightarrow} & & \downarrow 1_{F G}\\ F G & \overset{F s}{\Rightarrow} & F G F G & \overset{\varepsilon F G}{\to} & F G & & & = & 1_{\varepsilon}\\ 1_{F G} \downarrow & & F G \varepsilon \downarrow & \overset{\varepsilon \cdot \varepsilon}{\Rightarrow} & \downarrow \varepsilon\\ F G & \underset{1_{F G}}{\to} & F G & \underset{\varepsilon}{\to} & 1 } </annotation></semantics></math></div> <h3 id="lax_adjunctions_between_2categories">Lax adjunctions between 2-categories</h3> <p>A <strong>lax</strong> adjunction is defined in the same way as a 2-adjunction, except that we relax (remove) the assumptions that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>η</mi></mrow><annotation encoding="application/x-tex">\eta</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ε</mi></mrow><annotation encoding="application/x-tex">\varepsilon</annotation></semantics></math> are strong and that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi></mrow><annotation encoding="application/x-tex">s</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi></mrow><annotation encoding="application/x-tex">t</annotation></semantics></math> are invertible; the triangulator coherence conditions are still in effect. In that case, for objects <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi></mrow><annotation encoding="application/x-tex">b</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi></mrow><annotation encoding="application/x-tex">c</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>, there is a local adjunction between hom-categories</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>L</mi><mo>:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>b</mi><mo>,</mo><mi>G</mi><mi>c</mi><mo stretchy="false">)</mo><mo>→</mo><mi>C</mi><mo stretchy="false">(</mo><mi>F</mi><mi>b</mi><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>⊣</mo><mo stretchy="false">(</mo><mi>R</mi><mo>:</mo><mi>C</mi><mo stretchy="false">(</mo><mi>F</mi><mi>b</mi><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo><mo>→</mo><mi>B</mi><mo stretchy="false">(</mo><mi>b</mi><mo>,</mo><mi>G</mi><mi>c</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(L: B(b, G c) \to C(F b, c)) \dashv (R: C(F b, c) \to B(b, G c))</annotation></semantics></math></div> <p>given by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi><mo stretchy="false">(</mo><mi>g</mi><mo>:</mo><mi>b</mi><mo>→</mo><mi>G</mi><mi>c</mi><mo stretchy="false">)</mo><mo>=</mo><mo stretchy="false">(</mo><mi>F</mi><mi>b</mi><mover><mo>→</mo><mrow><mi>F</mi><mi>g</mi></mrow></mover><mi>F</mi><mi>G</mi><mi>c</mi><mover><mo>→</mo><mrow><mi>ε</mi><mi>c</mi></mrow></mover><mi>c</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">L(g: b \to G c) = (F b \overset{F g}{\to} F G c \overset{\varepsilon c}{\to} c)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo stretchy="false">(</mo><mi>f</mi><mo>:</mo><mi>F</mi><mi>b</mi><mo>→</mo><mi>c</mi><mo stretchy="false">)</mo><mo>=</mo><mo stretchy="false">(</mo><mi>b</mi><mover><mo>→</mo><mrow><mi>η</mi><mi>b</mi></mrow></mover><mi>G</mi><mi>F</mi><mi>b</mi><mover><mo>→</mo><mrow><mi>G</mi><mi>f</mi></mrow></mover><mi>G</mi><mi>c</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">R(f: F b \to c) = (b \overset{\eta b}{\to} G F b \overset{G f}{\to} G c)</annotation></semantics></math>. The unit of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi><mo>⊣</mo><mi>R</mi></mrow><annotation encoding="application/x-tex">L \dashv R</annotation></semantics></math> at <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo>:</mo><mi>b</mi><mo>→</mo><mi>G</mi><mi>c</mi></mrow><annotation encoding="application/x-tex">g: b \to G c</annotation></semantics></math> is given by the pasting</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>b</mi></mtd> <mtd><mover><mo>→</mo><mi>g</mi></mover></mtd> <mtd><mi>G</mi><mi>c</mi></mtd> <mtd><mover><mo>→</mo><mrow><msub><mn>1</mn> <mrow><mi>G</mi><mi>c</mi></mrow></msub></mrow></mover></mtd> <mtd><mi>G</mi><mi>c</mi></mtd></mtr> <mtr><mtd><mi>η</mi><mi>b</mi><mo stretchy="false">↓</mo></mtd> <mtd><mover><mo>⇐</mo><mrow><mi>η</mi><mo>⋅</mo><mi>g</mi></mrow></mover></mtd> <mtd><mo stretchy="false">↓</mo><mi>η</mi><mi>G</mi><mi>c</mi></mtd> <mtd><mover><mo>⇐</mo><mrow><mi>s</mi><mi>c</mi></mrow></mover></mtd> <mtd><mo stretchy="false">↓</mo><msub><mn>1</mn> <mrow><mi>G</mi><mi>c</mi></mrow></msub></mtd></mtr> <mtr><mtd><mi>G</mi><mi>F</mi><mi>b</mi></mtd> <mtd><munder><mo>→</mo><mrow><mi>G</mi><mi>F</mi><mi>g</mi></mrow></munder></mtd> <mtd><mi>G</mi><mi>F</mi><mi>G</mi><mi>c</mi></mtd> <mtd><munder><mo>→</mo><mrow><mi>G</mi><mi>ε</mi></mrow></munder></mtd> <mtd><mi>G</mi><mi>c</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ b & \overset{g}{\to} & G c & \overset{1_{G c}}{\to} & G c\\ \eta b \downarrow & \overset{\eta \cdot g}{\Leftarrow} & \downarrow \eta G c & \overset{s c}{\Leftarrow} & \downarrow 1_{G c}\\ G F b & \underset{G F g}{\to} & G F G c & \underset{G \varepsilon}{\to} & G c } </annotation></semantics></math></div> <p>and the counit of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi><mo>⊣</mo><mi>R</mi></mrow><annotation encoding="application/x-tex">L \dashv R</annotation></semantics></math> at <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>F</mi><mi>b</mi><mo>→</mo><mi>c</mi></mrow><annotation encoding="application/x-tex">f: F b \to c</annotation></semantics></math> is given by the pasting</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>F</mi><mi>b</mi></mtd> <mtd><mover><mo>→</mo><mrow><mi>F</mi><mi>η</mi><mi>b</mi></mrow></mover></mtd> <mtd><mi>F</mi><mi>G</mi><mi>F</mi><mi>b</mi></mtd> <mtd><mover><mo>→</mo><mrow><mi>F</mi><mi>G</mi><mi>f</mi></mrow></mover></mtd> <mtd><mi>F</mi><mi>G</mi><mi>c</mi></mtd></mtr> <mtr><mtd><msub><mn>1</mn> <mrow><mi>F</mi><mi>b</mi></mrow></msub><mo stretchy="false">↓</mo></mtd> <mtd><mover><mo>⇐</mo><mrow><mi>t</mi><mi>b</mi></mrow></mover></mtd> <mtd><mo stretchy="false">↓</mo><mi>ε</mi><mi>F</mi><mi>b</mi></mtd> <mtd><mover><mo>⇐</mo><mrow><mi>ε</mi><mo>⋅</mo><mi>f</mi></mrow></mover></mtd> <mtd><mo stretchy="false">↓</mo><mi>ε</mi><mi>c</mi></mtd></mtr> <mtr><mtd><mi>F</mi><mi>b</mi></mtd> <mtd><munder><mo>→</mo><mrow><msub><mn>1</mn> <mrow><mi>F</mi><mi>b</mi></mrow></msub></mrow></munder></mtd> <mtd><mi>F</mi><mi>b</mi></mtd> <mtd><munder><mo>→</mo><mi>f</mi></munder></mtd> <mtd><mi>c</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ F b & \overset{F \eta b}{\to} & F G F b & \overset{F G f}{\to} & F G c\\ 1_{F b} \downarrow & \overset{t b}{\Leftarrow} & \downarrow \varepsilon F b & \overset{\varepsilon \cdot f}{\Leftarrow} & \downarrow \varepsilon c\\ F b & \underset{1_{F b}}{\to} & F b & \underset{f}{\to} & c } </annotation></semantics></math></div> <p>The triangular equations for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi><mo>⊣</mo><mi>R</mi></mrow><annotation encoding="application/x-tex">L \dashv R</annotation></semantics></math> follow from the triangulator coherence conditions. (Warning: it is not generally true that a lax adjunction induces an adjoint pair in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Hom</mi> <mi>l</mi></msub><mo stretchy="false">(</mo><msup><mi>B</mi> <mi>op</mi></msup><mo>×</mo><mi>C</mi><mo>,</mo><mi>Cat</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Hom_l(B^{op} \times C, Cat)</annotation></semantics></math>. Cf. lemma 1 below.)</p> <h3 id="the_2category_">The 2-category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math></h3> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> be a 2-category. Following Carboni and Walters, we define a <em>map</em> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> to be a 1-cell in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> that possesses a right adjoint. It is useful to think of them as playing the role of “functional relations” in an ambient 2-category of relations. We let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math> be the locally full sub-2-category whose 0-cells are those of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> and whose 1-cells are the maps in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>. We observe that every 2-functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo>:</mo><mi>B</mi><mo>→</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">F: B \to C</annotation></semantics></math> restricts to a 2-functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo stretchy="false">|</mo><mo>:</mo><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mo>→</mo><mi>Map</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">F|: Map(B) \to Map(C)</annotation></semantics></math>, and by the following proposition, every transformation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>θ</mi><mo>:</mo><mi>F</mi><mo>→</mo><mi>G</mi></mrow><annotation encoding="application/x-tex">\theta: F \to G</annotation></semantics></math> restricts to a strong transformation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>θ</mi></mrow><annotation encoding="application/x-tex">\theta</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Hom</mi> <mi>s</mi></msub><mo stretchy="false">(</mo><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mo>,</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Hom_s(Map(B), C)</annotation></semantics></math>:</p> <p><strong>Proposition 1:</strong> If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>b</mi><mo>→</mo><mi>c</mi></mrow><annotation encoding="application/x-tex">f: b \to c</annotation></semantics></math> is a map in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>θ</mi><mo>⋅</mo><mi>f</mi></mrow><annotation encoding="application/x-tex">\theta \cdot f</annotation></semantics></math> is invertible.</p> <p><strong>Proof:</strong> Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>f</mi> <mo>*</mo></msup></mrow><annotation encoding="application/x-tex">f^*</annotation></semantics></math> denote a right adjoint of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math>. It is easily verified that the diagram</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>F</mi><mi>b</mi></mtd> <mtd><mover><mo>→</mo><mrow><mi>F</mi><mi>f</mi></mrow></mover></mtd> <mtd><mi>F</mi><mi>c</mi></mtd> <mtd><mover><mo>→</mo><mrow><mi>θ</mi><mi>c</mi></mrow></mover></mtd> <mtd><mi>G</mi><mi>c</mi></mtd> <mtd><mover><mo>→</mo><mrow><msub><mn>1</mn> <mrow><mi>G</mi><mi>c</mi></mrow></msub></mrow></mover></mtd> <mtd><mi>G</mi><mi>c</mi></mtd></mtr> <mtr><mtd><msub><mn>1</mn> <mrow><mi>F</mi><mi>b</mi></mrow></msub><mo stretchy="false">↓</mo></mtd> <mtd><mo>⇒</mo></mtd> <mtd><mi>F</mi><msup><mi>f</mi> <mo>*</mo></msup><mo stretchy="false">↓</mo></mtd> <mtd><mover><mo>⇒</mo><mrow><mi>θ</mi><mo>⋅</mo><msup><mi>f</mi> <mo>*</mo></msup></mrow></mover></mtd> <mtd><mo stretchy="false">↓</mo><mi>G</mi><msup><mi>f</mi> <mo>*</mo></msup></mtd> <mtd><mo>⇒</mo></mtd> <mtd><mo stretchy="false">↓</mo><msub><mn>1</mn> <mrow><mi>G</mi><mi>c</mi></mrow></msub></mtd></mtr> <mtr><mtd><mi>F</mi><mi>b</mi></mtd> <mtd><munder><mo>→</mo><mrow><msub><mn>1</mn> <mrow><mi>F</mi><mi>b</mi></mrow></msub></mrow></munder></mtd> <mtd><mi>F</mi><mi>b</mi></mtd> <mtd><munder><mo>→</mo><mrow><mi>θ</mi><mi>b</mi></mrow></munder></mtd> <mtd><mi>G</mi><mi>b</mi></mtd> <mtd><munder><mo>→</mo><mrow><mi>G</mi><mi>f</mi></mrow></munder></mtd> <mtd><mi>G</mi><mi>c</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ F b & \overset{F f}{\to} & F c & \overset{\theta c}{\to} & G c & \overset{1_{G c}}{\to} & G c\\ 1_{F b} \downarrow & \Rightarrow & F f^* \downarrow & \overset{\theta \cdot f^*}{\Rightarrow} & \downarrow G f^* & \Rightarrow & \downarrow 1_{G c}\\ F b & \underset{1_{F b}}{\to} & F b & \underset{\theta b}{\to} & G b & \underset{G f}{\to} & G c } </annotation></semantics></math></div> <p>pastes to give the inverse <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>θ</mi><mo>⋅</mo><mi>f</mi><msup><mo stretchy="false">)</mo> <mrow><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn></mrow></msup></mrow><annotation encoding="application/x-tex">(\theta \cdot f)^{-1}</annotation></semantics></math>, where the left and right squares are the unit and counit of adjunctions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mi>f</mi><mo>⊣</mo><mi>F</mi><msup><mi>f</mi> <mo>*</mo></msup></mrow><annotation encoding="application/x-tex">F f \dashv F f^*</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mi>f</mi><mo>⊣</mo><mi>G</mi><msup><mi>f</mi> <mo>*</mo></msup></mrow><annotation encoding="application/x-tex">G f \dashv G f^*</annotation></semantics></math>.</p> <p>A transformation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>θ</mi><mo>:</mo><mi>F</mi><mo>→</mo><mi>G</mi><mo>:</mo><mi>B</mi><mo>→</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">\theta: F \to G: B \to C</annotation></semantics></math> is <strong>map-valued</strong> if each 1-cell <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>θ</mi><mi>b</mi></mrow><annotation encoding="application/x-tex">\theta b</annotation></semantics></math> is a map in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>. By the previous proposition, a map-valued transformation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>θ</mi></mrow><annotation encoding="application/x-tex">\theta</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Hom</mi> <mi>l</mi></msub><mo stretchy="false">(</mo><mi>B</mi><mo>,</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Hom_l(B, C)</annotation></semantics></math> restricts to a strong transformation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>θ</mi><mo stretchy="false">|</mo><mo>:</mo><mi>F</mi><mo stretchy="false">|</mo><mo>→</mo><mi>G</mi><mo stretchy="false">|</mo></mrow><annotation encoding="application/x-tex">\theta|: F| \to G|</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Hom</mi> <mi>s</mi></msub><mo stretchy="false">(</mo><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mo>,</mo><mi>Map</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Hom_s(Map(B), Map(C))</annotation></semantics></math>.</p> <ul> <li><strong>Warning:</strong> In general it is imprecise to identify maps in a 2-category with the “functional relations”. That is, for some of the standard examples of cartesian bicategories, such as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo>=</mo><mi>Prof</mi></mrow><annotation encoding="application/x-tex">B = Prof</annotation></semantics></math>, we cannot simply identify <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Cat</annotation></semantics></math>: 1-cell equivalences are only Morita equivalences, not <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Cat</annotation></semantics></math>-equivalences. A better adapted framework is one of a bicategory with a proarrow equipment, or a <a class="existingWikiWord" href="/nlab/show/framed+bicategory">framed bicategory</a>. Eventually this article will be rewritten with this remark in mind…</li> </ul> <h2 id="definition_of_cartesian_structure_and_basic_results">Definition of cartesian structure and basic results</h2> <p>A <strong>cartesian structure</strong> on a bicategory <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> consists of the following data:</p> <ul> <li> <p>2-functors <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊗</mo><mo>:</mo><mi>B</mi><mo>×</mo><mi>B</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\otimes: B \times B \to B</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi><mo>:</mo><mstyle mathvariant="bold"><mn>1</mn></mstyle><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">I: \mathbf{1} \to B</annotation></semantics></math>, where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>1</mn></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{1}</annotation></semantics></math> is the terminal 2-category;</p> </li> <li> <p>Map-valued transformations</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>δ</mi><mo>:</mo><msub><mn>1</mn> <mi>B</mi></msub><mo>→</mo><mo>⊗</mo><mi>Δ</mi><mo>,</mo><mspace width="2em"></mspace><mi>π</mi><mo>:</mo><mi>Δ</mi><mo>⊗</mo><mo>→</mo><msub><mn>1</mn> <mrow><mi>B</mi><mo>×</mo><mi>B</mi></mrow></msub><mo>,</mo><mspace width="2em"></mspace><mi>ε</mi><mo>:</mo><msub><mn>1</mn> <mi>B</mi></msub><mo>→</mo><mi>I</mi><mo>!</mo></mrow><annotation encoding="application/x-tex">\delta: 1_B \to \otimes \Delta, \qquad \pi: \Delta \otimes \to 1_{B \times B}, \qquad \varepsilon: 1_B \to I !</annotation></semantics></math></div> <p>where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Δ</mi><mo>:</mo><mi>B</mi><mo>→</mo><mi>B</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\Delta: B \to B \times B</annotation></semantics></math> is the diagonal 2-functor and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mo>:</mo><mi>B</mi><mo>→</mo><mstyle mathvariant="bold"><mn>1</mn></mstyle></mrow><annotation encoding="application/x-tex">!: B \to \mathbf{1}</annotation></semantics></math> is the unique 2-functor;</p> </li> <li> <p>Invertible modifications</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mo>⊗</mo></mtd> <mtd><mover><mo>→</mo><mrow><mi>δ</mi><mo>⊗</mo></mrow></mover></mtd> <mtd><mo>⊗</mo><mi>Δ</mi><mo>⊗</mo></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>Δ</mi></mtd> <mtd><mover><mo>→</mo><mrow><mi>Δ</mi><mi>δ</mi></mrow></mover></mtd> <mtd><mi>Δ</mi><mo>⊗</mo><mi>Δ</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>I</mi></mtd> <mtd><mover><mo>→</mo><mrow><mi>ε</mi><mi>I</mi></mrow></mover></mtd> <mtd><mi>I</mi><mo>!</mo><mi>I</mi></mtd></mtr> <mtr><mtd><mpadded width="0" lspace="-100%width"><mrow><msub><mn>1</mn> <mo>⊗</mo></msub></mrow></mpadded><mo stretchy="false">↓</mo></mtd> <mtd><mover><mo>⇒</mo><mi>s</mi></mover></mtd> <mtd><mo stretchy="false">↓</mo><mpadded width="0"><mrow><mo>⊗</mo><mi>π</mi></mrow></mpadded></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mpadded width="0" lspace="-100%width"><mrow><msub><mn>1</mn> <mi>Δ</mi></msub></mrow></mpadded><mo stretchy="false">↓</mo></mtd> <mtd><mover><mo>⇐</mo><mi>t</mi></mover></mtd> <mtd><mo stretchy="false">↓</mo><mpadded width="0"><mrow><mi>π</mi><mi>Δ</mi></mrow></mpadded></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mpadded width="0" lspace="-100%width"><mrow><msub><mn>1</mn> <mi>I</mi></msub></mrow></mpadded><mo stretchy="false">↓</mo></mtd> <mtd><mover><mo>⇒</mo><mi>u</mi></mover></mtd> <mtd><mo stretchy="false">↓</mo><mpadded width="0"><mrow><mi>I</mi><mo>⋅</mo><mi>id</mi></mrow></mpadded></mtd></mtr> <mtr><mtd><mo>⊗</mo></mtd> <mtd><munder><mo>→</mo><mrow><msub><mn>1</mn> <mo>⊗</mo></msub></mrow></munder></mtd> <mtd><mo>⊗</mo></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>Δ</mi></mtd> <mtd><munder><mo>→</mo><mrow><msub><mn>1</mn> <mi>Δ</mi></msub></mrow></munder></mtd> <mtd><mi>Δ</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>I</mi></mtd> <mtd><munder><mo>→</mo><mrow><msub><mn>1</mn> <mi>I</mi></msub></mrow></munder></mtd> <mtd><mi>I</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ \otimes & \overset{\delta \otimes}{\to} & \otimes \Delta \otimes & & & & \Delta & \overset{\Delta \delta}{\to} & \Delta \otimes \Delta & & & & I & \overset{\varepsilon I}{\to} & I ! I\\ \mathllap{1_{\otimes}} \downarrow & \overset{s}{\Rightarrow} & \downarrow \mathrlap{\otimes \pi} & & & & \mathllap{1_{\Delta}} \downarrow & \overset{t}{\Leftarrow} & \downarrow \mathrlap{\pi \Delta} & & & & \mathllap{1_{I}} \downarrow & \overset{u}{\Rightarrow} & \downarrow \mathrlap{I \cdot id}\\ \otimes & \underset{1_{\otimes}}{\to} & \otimes & & & & \Delta & \underset{1_{\Delta}}{\to} & \Delta & & & & I & \underset{1_I}{\to} & I } </annotation></semantics></math></div> <p>satisfying the triangulator coherence conditions. <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>□</mo></mrow><annotation encoding="application/x-tex">\Box</annotation></semantics></math></p> </li> </ul> <p>The crucial observation is that, by proposition 1, this data restricts to give 2-adjunctions</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mover><mo>→</mo><mi>Δ</mi></mover><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mo>×</mo><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>⊣</mo><mo stretchy="false">(</mo><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mo>×</mo><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mover><mo>→</mo><mo>⊗</mo></mover><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(Map(B) \overset{\Delta}{\to} Map(B) \times Map(B)) \dashv (Map(B) \times Map(B) \overset{\otimes}{\to} Map(B))</annotation></semantics></math></div> <p><br /></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mover><mo>→</mo><mo>!</mo></mover><mstyle mathvariant="bold"><mn>1</mn></mstyle><mo stretchy="false">)</mo><mo>⊣</mo><mo stretchy="false">(</mo><mstyle mathvariant="bold"><mn>1</mn></mstyle><mover><mo>→</mo><mi>I</mi></mover><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(Map(B) \overset{!}{\to} \mathbf{1}) \dashv (\mathbf{1} \overset{I}{\to} Map(B))</annotation></semantics></math></div> <p>making the restriction of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊗</mo></mrow><annotation encoding="application/x-tex">\otimes</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math> a <em>2-product</em> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math> with 2-terminal object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi></mrow><annotation encoding="application/x-tex">I</annotation></semantics></math>. Naturally this finite 2-product structure on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math> is property-like: is uniquely determined up to equivalence which is uniquely specified up to unique isomorphism.</p> <p>A little later we will argue that cartesian structure on the full bicategory <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> is also property-like; the main thing is to see that the way in which <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊗</mo></mrow><annotation encoding="application/x-tex">\otimes</annotation></semantics></math> acts on 1-cells is essentially uniquely determined.</p> <h3 id="symmetric_monoidal_structure_via_cartesian_structure">Symmetric monoidal structure via cartesian structure</h3> <p>We now argue that a cartesian bicategory <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> carries a symmetric monoidal structure whose tensor product is</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊗</mo><mo>:</mo><mi>B</mi><mo>×</mo><mi>B</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\otimes: B \times B \to B</annotation></semantics></math></div> <p>The proof is pretty easy to sketch, once the fact is admitted that the induced 2-product structure makes <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math> a symmetric monoidal bicategory. This fact about 2-products, while never in dispute, was given a complete proof only in the past few years by the late Max Kelly, and we freely take advantage of it below.</p> <p>First, given objects <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>c</mi></mrow><annotation encoding="application/x-tex">a, b, c</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, we may regard them as objects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math>, where there is an associativity constraint</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>α</mi> <mrow><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>c</mi></mrow></msub><mo>:</mo><mo stretchy="false">(</mo><mi>a</mi><mo>⊗</mo><mi>b</mi><mo stretchy="false">)</mo><mo>⊗</mo><mi>c</mi><mo>→</mo><mi>a</mi><mo>⊗</mo><mo stretchy="false">(</mo><mi>b</mi><mo>⊗</mo><mi>c</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\alpha_{a, b, c}: (a \otimes b) \otimes c \to a \otimes (b \otimes c)</annotation></semantics></math></div> <p>on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math> which is definable by exploiting 2-universal properties of the 2-product. The associativity thus has an expression in terms of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊗</mo></mrow><annotation encoding="application/x-tex">\otimes</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>δ</mi></mrow><annotation encoding="application/x-tex">\delta</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>π</mi></mrow><annotation encoding="application/x-tex">\pi</annotation></semantics></math> which are globally defined on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, hence <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math> is globally defined as a transformation on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>. By similar considerations, the symmetry and unit constraints on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math> also extend to globally defined transformations on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>. We argue in a moment that these constraints are strong (adjoint) equivalences.</p> <p>Symmetric monoidal structure on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> also demands various structural modifications (such as a Yang-Baxter modification <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>R</mi> <mrow><mo>•</mo><mo stretchy="false">|</mo><mo>•</mo><mo>,</mo><mo>•</mo></mrow></msub></mrow><annotation encoding="application/x-tex">R_{\bullet |\bullet, \bullet}</annotation></semantics></math>) satisfying various coherence conditions, but the components of such modifications (<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>R</mi> <mrow><mi>a</mi><mo stretchy="false">|</mo><mi>b</mi><mo>,</mo><mi>c</mi></mrow></msub></mrow><annotation encoding="application/x-tex">R_{a|b, c}</annotation></semantics></math>, say) are defined by regarding their components <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>c</mi></mrow><annotation encoding="application/x-tex">a, b, c</annotation></semantics></math> as objects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math> and using the corresponding modifications there. Again, each such modification on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math> is defined in terms of 2-adjunction data <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊗</mo></mrow><annotation encoding="application/x-tex">\otimes</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi></mrow><annotation encoding="application/x-tex">I</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>δ</mi></mrow><annotation encoding="application/x-tex">\delta</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>π</mi></mrow><annotation encoding="application/x-tex">\pi</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ε</mi></mrow><annotation encoding="application/x-tex">\varepsilon</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi></mrow><annotation encoding="application/x-tex">s</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi></mrow><annotation encoding="application/x-tex">t</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>u</mi></mrow><annotation encoding="application/x-tex">u</annotation></semantics></math> which are globally defined on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, so each such structure is a modification on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>. Various coherence conditions on the modifications must be checked, but the conditions hold at every choice of objects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> by regarding them as objects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math> and using the symmetric monoidal structure there, so the conditions hold on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>.</p> <p>Now we check that the structural transformations <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math> are strong adjoint equivalences. Indeed, when regarded as being defined on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math>, the constraint <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math> is an equivalence and so has a left adjoint (with invertible unit and counit) <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>α</mi> <mo>−</mo></msup></mrow><annotation encoding="application/x-tex">\alpha^-</annotation></semantics></math> with components</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msubsup><mi>α</mi> <mrow><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>c</mi></mrow> <mo lspace="verythinmathspace" rspace="0em">−</mo></msubsup><mo>:</mo><mi>a</mi><mo>⊗</mo><mo stretchy="false">(</mo><mi>b</mi><mo>⊗</mo><mi>c</mi><mo stretchy="false">)</mo><mo>→</mo><mo stretchy="false">(</mo><mi>a</mi><mo>⊗</mo><mi>b</mi><mo stretchy="false">)</mo><mo>⊗</mo><mi>c</mi></mrow><annotation encoding="application/x-tex">\alpha_{a, b, c}^{-}: a \otimes (b \otimes c) \to (a \otimes b) \otimes c</annotation></semantics></math></div> <p>and just like <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>α</mi> <mo>−</mo></msup></mrow><annotation encoding="application/x-tex">\alpha^-</annotation></semantics></math> is definable in terms of global structure on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, making <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>α</mi> <mo>−</mo></msup></mrow><annotation encoding="application/x-tex">\alpha^-</annotation></semantics></math> a transformation on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>. Then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math>, and by similar reasoning the symmetry and unit constraints, are strong transformations on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> by the following lemma:</p> <p><strong>Lemma 1:</strong> If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math> is a right adjoint in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Hom</mi> <mi>l</mi></msub><mo stretchy="false">(</mo><mi>C</mi><mo>,</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Hom_l(C, B)</annotation></semantics></math>, then the transformation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math> is strong. Consequently, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>α</mi> <mo>−</mo></msup><mo>⊣</mo><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha^- \dashv \alpha</annotation></semantics></math> is an adjoint equivalence, so that both <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>α</mi> <mo>−</mo></msup><mo>⊣</mo><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha^- \dashv \alpha</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi><mo>⊣</mo><msup><mi>α</mi> <mo>−</mo></msup></mrow><annotation encoding="application/x-tex">\alpha \dashv \alpha^-</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>α</mi> <mo>−</mo></msup><mo>⊣</mo><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha^- \dashv \alpha</annotation></semantics></math> is a strong adjoint equivalence in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Hom</mi> <mi>s</mi></msub><mo stretchy="false">(</mo><mi>C</mi><mo>,</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Hom_s(C, B)</annotation></semantics></math>.</p> <p><strong>Proof:</strong> Only the first statement requires proof. Given <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>:</mo><mi>c</mi><mo>→</mo><mi>d</mi></mrow><annotation encoding="application/x-tex">r: c \to d</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>ev</mi> <mi>c</mi></msub><mo>:</mo><msub><mi>Hom</mi> <mi>l</mi></msub><mo stretchy="false">(</mo><mi>C</mi><mo>,</mo><mi>B</mi><mo stretchy="false">)</mo><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">ev_c: Hom_l(C, B) \to B</annotation></semantics></math> denote the 2-functor which evaluates at <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi></mrow><annotation encoding="application/x-tex">c</annotation></semantics></math> (keep in mind that the 1-cells in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Hom</mi> <mi>l</mi></msub><mo stretchy="false">(</mo><mi>C</mi><mo>,</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Hom_l(C, B)</annotation></semantics></math> are transformations which are oplax in the sense of Bénabou), and let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>ev</mi> <mi>r</mi></msub><mo>:</mo><msub><mi>ev</mi> <mi>c</mi></msub><mo>→</mo><msub><mi>ev</mi> <mi>d</mi></msub></mrow><annotation encoding="application/x-tex">ev_r: ev_c \to ev_d</annotation></semantics></math> denote the evident transformation; this is <em>lax</em> in the sense of Bénabou. Then, by dualizing proposition 1, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>ev</mi> <mi>r</mi></msub><mo stretchy="false">(</mo><mi>α</mi><mo stretchy="false">)</mo><mo>=</mo><mi>α</mi><mo>⋅</mo><mi>r</mi></mrow><annotation encoding="application/x-tex">ev_r(\alpha) = \alpha \cdot r</annotation></semantics></math> is an isomorphism if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math> is a <em>right</em> adjoint. Since <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi><mo>⋅</mo><mi>r</mi></mrow><annotation encoding="application/x-tex">\alpha \cdot r</annotation></semantics></math> is an isomorphism for all 1-cells <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi></mrow><annotation encoding="application/x-tex">r</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>, it follows that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math> is strong. <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>□</mo></mrow><annotation encoding="application/x-tex">\Box</annotation></semantics></math></p> <p>This completes the argument that the symmetric monoidal structure on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math> extends to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>.</p> <h3 id="comparison_with_carboniwalters">Comparison with Carboni-Walters</h3> <p>Let us begin unpacking the terse definition of cartesian bicategory so that it becomes more recognizable. For the sake of notational convenience, we use the fact that as a monoidal bicategory, a cartesian bicategory may be strictified and replaced by a (monoidally biequivalent) <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Gray</mi></mrow><annotation encoding="application/x-tex">Gray</annotation></semantics></math> monoid <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>. That is to say, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo>⊗</mo> <mi>G</mi></msub></mrow><annotation encoding="application/x-tex">\otimes_G</annotation></semantics></math> denotes the tensor product of the symmetric monoidal closed category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Gray</mi></mrow><annotation encoding="application/x-tex">Gray</annotation></semantics></math>, then there is firstly a biequivalence <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo>×</mo><mi>B</mi><mo>≃</mo><mi>B</mi><msub><mo>⊗</mo> <mi>G</mi></msub><mi>B</mi></mrow><annotation encoding="application/x-tex">B \times B \simeq B \otimes_G B</annotation></semantics></math>, and we may transfer the data of the cartesian structure across this biequivalence to get a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Gray</mi></mrow><annotation encoding="application/x-tex">Gray</annotation></semantics></math> monoid multiplication</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊗</mo><mo>:</mo><mi>B</mi><msub><mo>⊗</mo> <mi>G</mi></msub><mi>B</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\otimes: B \otimes_G B \to B</annotation></semantics></math></div> <p>together with a corresponding diagonal</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>B</mi><mover><mo>→</mo><mi>Δ</mi></mover><mi>B</mi><mo>×</mo><mi>B</mi><mo>≃</mo><mi>B</mi><msub><mo>⊗</mo> <mi>G</mi></msub><mi>B</mi></mrow><annotation encoding="application/x-tex">B \overset{\Delta}{\to} B \times B \simeq B \otimes_G B</annotation></semantics></math></div> <p>which we again denote by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Δ</mi></mrow><annotation encoding="application/x-tex">\Delta</annotation></semantics></math>. In that case, given a 1-cell <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>:</mo><mi>a</mi><mo>→</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">r: a \to b</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, we may write structure cells <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>δ</mi><mo>⋅</mo><mi>r</mi></mrow><annotation encoding="application/x-tex">\delta \cdot r</annotation></semantics></math> for the transformation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>δ</mi><mo>:</mo><msub><mn>1</mn> <mi>B</mi></msub><mo>→</mo><mo>⊗</mo><mi>Δ</mi></mrow><annotation encoding="application/x-tex">\delta: 1_B \to \otimes \Delta</annotation></semantics></math> in the form</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>a</mi></mtd> <mtd><mover><mo>→</mo><mrow><mi>δ</mi><mi>a</mi></mrow></mover></mtd> <mtd><mi>a</mi><mo>⊗</mo><mi>a</mi></mtd></mtr> <mtr><mtd><mi>r</mi><mo stretchy="false">↓</mo></mtd> <mtd><mover><mo>⇒</mo><mrow><mi>δ</mi><mo>⋅</mo><mi>r</mi></mrow></mover></mtd> <mtd><mo stretchy="false">↓</mo><mi>r</mi><mo>⊗</mo><mi>r</mi></mtd></mtr> <mtr><mtd><mi>b</mi></mtd> <mtd><munder><mo>→</mo><mrow><mi>δ</mi><mi>b</mi></mrow></munder></mtd> <mtd><mi>b</mi><mo>⊗</mo><mi>b</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ a & \overset{\delta a}{\to} & a \otimes a\\ r \downarrow & \overset{\delta \cdot r}{\Rightarrow} & \downarrow r \otimes r\\ b & \underset{\delta b}{\to} & b \otimes b } </annotation></semantics></math></div> <p>where to be definite we make the convention that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>⊗</mo><mi>r</mi><mo>:</mo><mo>=</mo><mo stretchy="false">(</mo><mi>r</mi><mo>⊗</mo><mn>1</mn><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mn>1</mn><mo>⊗</mo><mi>r</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">r \otimes r := (r \otimes 1)(1 \otimes r)</annotation></semantics></math>.</p> <p>An object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi></mrow><annotation encoding="application/x-tex">c</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, viewed as an object of a 2-category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math> with 2-products, naturally carries a 2-comonoid (or pseudocomonoid) structure; the unit of the 2-adjunction <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Δ</mi><mo>⊣</mo><mo>⊗</mo></mrow><annotation encoding="application/x-tex">\Delta \dashv \otimes</annotation></semantics></math> is the diagonal map</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>δ</mi><mi>c</mi><mo>:</mo><mi>c</mi><mo>→</mo><mi>c</mi><mo>⊗</mo><mi>c</mi><mo>,</mo></mrow><annotation encoding="application/x-tex">\delta c: c \to c \otimes c,</annotation></semantics></math></div> <p>i.e., the 2-comonoid comultiplication. The unit of the 2-adjunction <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mo>⊣</mo><mi>I</mi></mrow><annotation encoding="application/x-tex">! \dashv I</annotation></semantics></math> is the projection to the 2-terminal object</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>ε</mi><mi>c</mi><mo>:</mo><mi>c</mi><mo>→</mo><mi>I</mi><mo>,</mo></mrow><annotation encoding="application/x-tex">\varepsilon c: c \to I,</annotation></semantics></math></div> <p>i.e., the 2-comonoid counit. (It is more usual to denote a (2-)terminal object by the symbol <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math>, and from here on we will follow that practice, writing the projection as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ε</mi><mi>c</mi><mo>:</mo><mi>c</mi><mo>→</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">\varepsilon c: c \to 1</annotation></semantics></math>, and forget <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi></mrow><annotation encoding="application/x-tex">I</annotation></semantics></math>.)</p> <p>Spelling this out a little further, let us turn attention to the transformation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>π</mi><mo>:</mo><mi>Δ</mi><mo>⊗</mo><mo>→</mo><msub><mn>1</mn> <mrow><mi>B</mi><msub><mo>⊗</mo> <mi>G</mi></msub><mi>B</mi></mrow></msub></mrow><annotation encoding="application/x-tex">\pi: \Delta \otimes \to 1_{B \otimes_G B}</annotation></semantics></math>. The components of the transformation take the form</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>π</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo>=</mo><mo stretchy="false">⟨</mo><msub><mi>π</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>π</mi> <mn>2</mn></msub><mo stretchy="false">⟩</mo><mo>:</mo><mo stretchy="false">(</mo><mi>a</mi><mo>⊗</mo><mi>b</mi><mo>,</mo><mi>a</mi><mo>⊗</mo><mi>b</mi><mo stretchy="false">)</mo><mo>→</mo><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\pi (a, b) = \langle \pi_1, \pi_2 \rangle: (a \otimes b, a \otimes b) \to (a, b)</annotation></semantics></math></div> <p>where, as a consequence of how the 2-product <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊗</mo></mrow><annotation encoding="application/x-tex">\otimes</annotation></semantics></math> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math> is defined, we have the following formulas for the projections <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>π</mi> <mn>1</mn></msub></mrow><annotation encoding="application/x-tex">\pi_1</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>π</mi> <mn>2</mn></msub></mrow><annotation encoding="application/x-tex">\pi_2</annotation></semantics></math>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>π</mi> <mn>1</mn></msub><mo>=</mo><mo stretchy="false">(</mo><mi>a</mi><mo>⊗</mo><mi>b</mi><mover><mo>→</mo><mrow><msub><mn>1</mn> <mi>a</mi></msub><mo>⊗</mo><mi>ε</mi></mrow></mover><mi>a</mi><mo>⊗</mo><mn>1</mn><mo>≅</mo><mi>a</mi><mo stretchy="false">)</mo><mo>;</mo><mspace width="2em"></mspace><msub><mi>π</mi> <mn>2</mn></msub><mo>=</mo><mo stretchy="false">(</mo><mi>a</mi><mo>⊗</mo><mi>b</mi><mover><mo>→</mo><mrow><mi>ε</mi><mo>⊗</mo><msub><mn>1</mn> <mi>b</mi></msub></mrow></mover><mn>1</mn><mo>⊗</mo><mi>b</mi><mo>≅</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">\pi_1 = (a \otimes b \overset{1_a \otimes \varepsilon}{\to} a \otimes 1 \cong a); \qquad \pi_2 = (a \otimes b \overset{\varepsilon \otimes 1_b}{\to} 1 \otimes b \cong b</annotation></semantics></math></div> <p>Thus, the unit and counit data <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>δ</mi></mrow><annotation encoding="application/x-tex">\delta</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>π</mi></mrow><annotation encoding="application/x-tex">\pi</annotation></semantics></math> are expressible in terms of the symmetric monoidal 2-category structure and the comonoid structures on the objects therein.</p> <p>Finally, for a given 1-cell <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>:</mo><mi>c</mi><mo>→</mo><mi>d</mi></mrow><annotation encoding="application/x-tex">r: c \to d</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, the structure cells</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>c</mi></mtd> <mtd><mover><mo>→</mo><mrow><mi>δ</mi><mi>c</mi></mrow></mover></mtd> <mtd><mi>c</mi><mo>⊗</mo><mi>c</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>c</mi></mtd> <mtd><mover><mo>→</mo><mrow><mi>ε</mi><mi>c</mi></mrow></mover></mtd> <mtd><mn>1</mn></mtd></mtr> <mtr><mtd><mi>r</mi><mo stretchy="false">↓</mo></mtd> <mtd><mover><mo>⇒</mo><mrow><mi>δ</mi><mo>⋅</mo><mi>r</mi></mrow></mover></mtd> <mtd><mo stretchy="false">↓</mo><mi>r</mi><mo>⊗</mo><mi>r</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>r</mi><mo stretchy="false">↓</mo></mtd> <mtd><mover><mo>⇒</mo><mrow><mi>ε</mi><mo>⋅</mo><mi>r</mi></mrow></mover></mtd> <mtd><mo stretchy="false">↓</mo><msub><mi>id</mi> <mn>1</mn></msub></mtd></mtr> <mtr><mtd><mi>d</mi></mtd> <mtd><munder><mo>→</mo><mrow><mi>δ</mi><mi>d</mi></mrow></munder></mtd> <mtd><mi>d</mi><mo>⊗</mo><mi>d</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>d</mi></mtd> <mtd><munder><mo>→</mo><mrow><mi>ε</mi><mi>d</mi></mrow></munder></mtd> <mtd><mn>1</mn></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ c & \overset{\delta c}{\to} & c \otimes c & & & & c & \overset{\varepsilon c}{\to} & 1\\ r \downarrow & \overset{\delta \cdot r}{\Rightarrow} & \downarrow r \otimes r & & & & r \downarrow & \overset{\varepsilon \cdot r}{\Rightarrow} & \downarrow id_1\\ d & \underset{\delta d}{\to} & d \otimes d & & & & d & \underset{\varepsilon d}{\to} & 1 } </annotation></semantics></math></div> <p>exhibit <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>:</mo><mi>c</mi><mo>→</mo><mi>d</mi></mrow><annotation encoding="application/x-tex">r: c \to d</annotation></semantics></math> as a colax morphism of 2-comonoids; if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi></mrow><annotation encoding="application/x-tex">r</annotation></semantics></math> is a map, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>δ</mi><mo>⋅</mo><mi>r</mi></mrow><annotation encoding="application/x-tex">\delta \cdot r</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ε</mi><mo>⋅</mo><mi>r</mi></mrow><annotation encoding="application/x-tex">\varepsilon \cdot r</annotation></semantics></math> are isomorphisms and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi></mrow><annotation encoding="application/x-tex">r</annotation></semantics></math> becomes a strong morphism of 2-comonoids. This may be appreciated more fully by considering specific examples such as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo>=</mo><mi>Rel</mi></mrow><annotation encoding="application/x-tex">B = Rel</annotation></semantics></math> (where maps are functions, which become comonoid morphisms by virtue of naturality of diagonal and projection maps), and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo>=</mo><mi>Mod</mi></mrow><annotation encoding="application/x-tex">B = Mod</annotation></semantics></math>.</p> <p>Carboni and Walters define a cartesian bicategory to be a symmetric monoidal bicategory in which each object carries a 2-comonoid structure (for which the comultiplication and counit are <em>maps</em>), and each 1-cell is a colax morphism between the corresponding comonoid structures. However, spelling this approach out in full detail leads to a rather largish definition; it seems more efficient to approach the definition by taking advantage of some high-level 2-categorical algebra as we have done here, and deriving the structures envisaged by Carboni and Walters as a consequence.</p> <h3 id="local_cartesian_products">Local cartesian products</h3> <p>The definition of cartesian structure <em>a fortiori</em> involves <em>lax</em> adjunctions (in the sense explained earlier)</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Δ</mi><msub><mo>⊣</mo> <mi>lax</mi></msub><mo>⊗</mo><mo>:</mo><mi>B</mi><mo>×</mo><mi>B</mi><mo>→</mo><mi>B</mi><mspace width="2em"></mspace><mo>!</mo><msub><mo>⊣</mo> <mi>lax</mi></msub><mi>I</mi><mo>:</mo><mstyle mathvariant="bold"><mn>1</mn></mstyle><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\Delta \dashv_{lax} \otimes: B \times B \to B \qquad ! \dashv_{lax} I: \mathbf{1} \to B</annotation></semantics></math></div> <p>and by our earlier discussion of lax adjunctions, this means we have local 1-adjunctions of the form</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>⊗</mo><mi>c</mi><mo stretchy="false">)</mo><mover><mo>→</mo><mi>λ</mi></mover><mo stretchy="false">(</mo><mi>B</mi><mo>×</mo><mi>B</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mo stretchy="false">⟨</mo><mi>a</mi><mo>,</mo><mi>a</mi><mo stretchy="false">⟩</mo><mo>,</mo><mo stretchy="false">⟨</mo><mi>b</mi><mo>,</mo><mi>c</mi><mo stretchy="false">⟩</mo><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>⊣</mo><mo stretchy="false">(</mo><mi>B</mi><mo>×</mo><mi>B</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mo stretchy="false">⟨</mo><mi>a</mi><mo>,</mo><mi>a</mi><mo stretchy="false">⟩</mo><mo>,</mo><mo stretchy="false">⟨</mo><mi>b</mi><mo>,</mo><mi>c</mi><mo stretchy="false">⟩</mo><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mover><mo>→</mo><mi>ρ</mi></mover><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>⊗</mo><mi>c</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(B(a, b \otimes c) \stackrel{\lambda}{\to} (B \times B)(\langle a, a \rangle, \langle b, c \rangle)) \dashv (B \times B)(\langle a, a \rangle, \langle b, c \rangle)) \stackrel{\rho}{\to} B(a, b \otimes c))</annotation></semantics></math></div> <p>Now let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>=</mo><mi>c</mi></mrow><annotation encoding="application/x-tex">b = c</annotation></semantics></math>, and use the fact that we have an adjunction</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>b</mi><mover><mo>→</mo><mrow><mi>δ</mi><mi>b</mi></mrow></mover><mi>b</mi><mo>⊗</mo><mi>b</mi><mo stretchy="false">)</mo><mo>⊣</mo><mo stretchy="false">(</mo><mi>b</mi><mo>⊗</mo><mi>b</mi><mover><mo>→</mo><mrow><mi>δ</mi><msup><mi>b</mi> <mo>*</mo></msup></mrow></mover><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(b \stackrel{\delta b}{\to} b \otimes b) \dashv (b \otimes b \stackrel{\delta b^{\ast}}{\to} b)</annotation></semantics></math></div> <p>to obtain an adjoint pair where</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mover><mo>→</mo><mrow><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>δ</mi><mi>b</mi><mo stretchy="false">)</mo></mrow></mover><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>⊗</mo><mi>b</mi><mo stretchy="false">)</mo><mover><mo>→</mo><mi>λ</mi></mover><mi>B</mi><mo>×</mo><mi>B</mi><mo stretchy="false">(</mo><mo stretchy="false">⟨</mo><mi>a</mi><mo>,</mo><mi>a</mi><mo stretchy="false">⟩</mo><mo>,</mo><mo stretchy="false">⟨</mo><mi>b</mi><mo>,</mo><mi>b</mi><mo stretchy="false">⟩</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">B(a, b) \stackrel{B(a, \delta b)}{\to} B(a, b \otimes b) \stackrel{\lambda}{\to} B \times B(\langle a, a \rangle, \langle b, b \rangle)</annotation></semantics></math></div> <p>is left adjoint to</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo>×</mo><mi>B</mi><mo stretchy="false">(</mo><mo stretchy="false">⟨</mo><mi>a</mi><mo>,</mo><mi>a</mi><mo stretchy="false">⟩</mo><mo>,</mo><mo stretchy="false">⟨</mo><mi>b</mi><mo>,</mo><mi>b</mi><mo stretchy="false">⟩</mo><mo stretchy="false">)</mo><mover><mo>→</mo><mi>ρ</mi></mover><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>⊗</mo><mi>b</mi><mo stretchy="false">)</mo><mover><mo>→</mo><mrow><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>δ</mi><msup><mi>b</mi> <mo>*</mo></msup><mo stretchy="false">)</mo></mrow></mover><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo>.</mo></mrow><annotation encoding="application/x-tex">B \times B(\langle a, a \rangle, \langle b, b \rangle) \stackrel{\rho}{\to} B(a, b \otimes b) \stackrel{B(a, \delta b^\ast)}{\to} B(a, b).</annotation></semantics></math></div> <p>The first of these arrows is just the diagonal functor</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mover><mo>→</mo><mrow><msub><mi>δ</mi> <mi>loc</mi></msub></mrow></mover><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo>×</mo><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">B(a, b) \stackrel{\delta_{loc}}{\to} B(a, b) \times B(a, b)</annotation></semantics></math></div> <p>on the local hom-category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">B(a, b)</annotation></semantics></math>. Therefore the second arrow, being right adjoint to the first, provides a product functor on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">B(a, b)</annotation></semantics></math>. Similarly, each local hom-category carries a terminal object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn><mo>→</mo><mi>hom</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">1 \to \hom(a, b)</annotation></semantics></math>. We may summarize this by saying that cartesian bicategories are <em>locally cartesian</em>.</p> <h3 id="essential_uniqueness_of_cartesian_structure">Essential uniqueness of cartesian structure</h3> <p>So far we have seen that for a cartesian bicategory <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>,</p> <ul> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math> carries 2-products,</p> </li> <li> <p>Local hom-categories carry products.</p> </li> </ul> <p>It is clear that 2-product data on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math> and local product data on local hom-categories are uniquely determined up to appropriate notions of equivalence, since they are determined by appropriate universal properties. Now we show that these data actually determine the whole of the cartesian structure. We may therefore conclude that a cartesian structure on a bicategory must be essentially unique, if it exists.</p> <p>To explain how this works, it helps to consider some simple examples of cartesian bicategories such as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Rel</mi></mrow><annotation encoding="application/x-tex">Rel</annotation></semantics></math>. First, let us reconstruct</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊗</mo><mo>:</mo><mi>B</mi><mo>×</mo><mi>B</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\otimes: B \times B \to B</annotation></semantics></math></div> <p>from the data above. Suppose given two 1-cells <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>:</mo><mi>a</mi><mo>→</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">r: a \to b</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo>:</mo><mi>c</mi><mo>→</mo><mi>d</mi></mrow><annotation encoding="application/x-tex">s: c \to d</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, e.g., relations between sets, or even just subsets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>⊆</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">r \subseteq b</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo>⊆</mo><mi>d</mi></mrow><annotation encoding="application/x-tex">s \subseteq d</annotation></semantics></math>. The tensor product <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>⊗</mo><mi>s</mi></mrow><annotation encoding="application/x-tex">r \otimes s</annotation></semantics></math> is intuitively a “rectangle”, like <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>×</mo><mi>s</mi><mo>⊆</mo><mi>b</mi><mo>×</mo><mi>d</mi></mrow><annotation encoding="application/x-tex">r \times s \subseteq b \times d</annotation></semantics></math> in the case of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Rel</mi></mrow><annotation encoding="application/x-tex">Rel</annotation></semantics></math>, obtained by “pulling back” <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi></mrow><annotation encoding="application/x-tex">r</annotation></semantics></math> along the projection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>π</mi> <mn>1</mn></msub><mo>:</mo><mi>b</mi><mo>×</mo><mi>d</mi><mo>→</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">\pi_1: b \times d \to b</annotation></semantics></math>, pulling back <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi></mrow><annotation encoding="application/x-tex">s</annotation></semantics></math> along the projection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>π</mi> <mn>2</mn></msub><mo>:</mo><mi>b</mi><mo>×</mo><mi>d</mi><mo>→</mo><mi>d</mi></mrow><annotation encoding="application/x-tex">\pi_2: b \times d \to d</annotation></semantics></math>, and taking the intersection – more generally, taking a local product. By formalizing this procedure, we are led to the general formula</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>⊗</mo><mi>s</mi><mo>≅</mo><mo stretchy="false">(</mo><msubsup><mi>π</mi> <mrow><mn>1</mn><mo>,</mo><mi>b</mi><mo>,</mo><mi>d</mi></mrow> <mo>*</mo></msubsup><mi>r</mi><msub><mi>π</mi> <mrow><mn>1</mn><mo>,</mo><mi>a</mi><mo>,</mo><mi>c</mi></mrow></msub><mo stretchy="false">)</mo><msub><mo>×</mo> <mi>loc</mi></msub><mo stretchy="false">(</mo><msubsup><mi>π</mi> <mrow><mn>2</mn><mo>,</mo><mi>b</mi><mo>,</mo><mi>d</mi></mrow> <mo>*</mo></msubsup><mi>s</mi><msub><mi>π</mi> <mrow><mn>2</mn><mo>,</mo><mi>a</mi><mo>,</mo><mi>c</mi></mrow></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">r \otimes s \cong (\pi_{1, b, d}^{\ast} r \pi_{1, a, c}) \times_{loc} (\pi_{2, b, d}^{\ast} s \pi_{2, a, c})</annotation></semantics></math></div> <p>where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi></mrow><annotation encoding="application/x-tex">r</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi></mrow><annotation encoding="application/x-tex">s</annotation></semantics></math> play the role of mere placeholders.</p> <p>It is a theorem (whose proof we defer) is that in a cartesian bicategory, we may reconstruct the functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>⊗</mo><mo lspace="verythinmathspace" rspace="0em">−</mo></mrow><annotation encoding="application/x-tex">- \otimes -</annotation></semantics></math> by the formula</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msubsup><mi>π</mi> <mn>1</mn> <mo>*</mo></msubsup><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo><msub><mi>π</mi> <mn>1</mn></msub><mo stretchy="false">)</mo><msub><mo>×</mo> <mi>loc</mi></msub><mo stretchy="false">(</mo><msubsup><mi>π</mi> <mn>2</mn> <mo>*</mo></msubsup><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo><msub><mi>π</mi> <mn>2</mn></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(\pi_{1}^{\ast} (-) \pi_{1}) \times_{loc} (\pi_{2}^{\ast} (-) \pi_{2})</annotation></semantics></math></div> <p>where each of the displayed data is manifestly part of the 2-product structure on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(B)</annotation></semantics></math> or the local cartesian structure.</p> <p>The other data we are required to reconstruct are structure cells like <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>δ</mi><mi>r</mi></mrow><annotation encoding="application/x-tex">\delta r</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>π</mi><mo stretchy="false">⟨</mo><mi>r</mi><mo>,</mo><mi>s</mi><mo stretchy="false">⟩</mo></mrow><annotation encoding="application/x-tex">\pi \langle r, s\rangle</annotation></semantics></math> which pertain to the transformations <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>δ</mi></mrow><annotation encoding="application/x-tex">\delta</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>π</mi></mrow><annotation encoding="application/x-tex">\pi</annotation></semantics></math>. As an example, consider <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>δ</mi><mi>r</mi></mrow><annotation encoding="application/x-tex">\delta r</annotation></semantics></math>. This is a 2-cell</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>δ</mi><mi>r</mi><mo>:</mo><mo stretchy="false">(</mo><mi>δ</mi><mi>b</mi><mo stretchy="false">)</mo><mi>r</mi><mo>→</mo><mo stretchy="false">(</mo><mi>r</mi><mo>⊗</mo><mi>r</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>δ</mi><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\delta r: (\delta b)r \to (r \otimes r)(\delta a)</annotation></semantics></math></div> <p>which is mated to a 2-cell</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>→</mo><mo stretchy="false">(</mo><mi>δ</mi><mi>b</mi><msup><mo stretchy="false">)</mo> <mo>*</mo></msup><mo stretchy="false">(</mo><mi>r</mi><mo>⊗</mo><mi>r</mi><mo stretchy="false">)</mo><mi>δ</mi><mo>=</mo><mi>r</mi><msub><mo>×</mo> <mi>loc</mi></msub><mi>r</mi><mo>.</mo></mrow><annotation encoding="application/x-tex">r \to (\delta b)^\ast (r \otimes r) \delta = r \times_{loc} r.</annotation></semantics></math></div> <p>This 2-cell is precisely the local diagonal <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>→</mo><mi>r</mi><mo>×</mo><mi>r</mi></mrow><annotation encoding="application/x-tex">r \to r \times r</annotation></semantics></math>, manifestly part of the local cartesian structure. Thus the structure cells for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>δ</mi></mrow><annotation encoding="application/x-tex">\delta</annotation></semantics></math> are uniquely determined, and similarly for the transformations <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>π</mi></mrow><annotation encoding="application/x-tex">\pi</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ε</mi></mrow><annotation encoding="application/x-tex">\varepsilon</annotation></semantics></math>.</p> <p>This completes the sketched proof of essential uniqueness.</p> <h2 id="cartesian_bicategories_and_hyperdoctrines">Cartesian bicategories and hyperdoctrines</h2> <p>Each cartesian bicategory <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{B}</annotation></semantics></math> gives rise to a bifibration, or in other language a (weak) 2-functor</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mo stretchy="false">(</mo><mi>i</mi><mo>−</mo><mo>,</mo><mi>i</mi><mo>−</mo><mo stretchy="false">)</mo><mo>:</mo><mi>Map</mi><mo stretchy="false">(</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><msup><mo stretchy="false">)</mo> <mi>op</mi></msup><mo>×</mo><mi>Map</mi><mo stretchy="false">(</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mo stretchy="false">)</mo><mo>→</mo><mi>Cat</mi></mrow><annotation encoding="application/x-tex">\mathbf{B}(i-, i-): Map(\mathbf{B})^{op} \times Map(\mathbf{B}) \to Cat</annotation></semantics></math></div> <p>or in other words a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Cat</annotation></semantics></math>-valued bimodule over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(\mathbf{B})</annotation></semantics></math>, for which each <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mo stretchy="false">(</mo><mi>i</mi><mi>f</mi><mo>,</mo><mi>i</mi><mi>c</mi><mo stretchy="false">)</mo><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mo stretchy="false">(</mo><mi>i</mi><mi>b</mi><mo>,</mo><mi>i</mi><mi>c</mi><mo stretchy="false">)</mo><mo>→</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mo stretchy="false">(</mo><mi>i</mi><mi>a</mi><mo>,</mo><mi>i</mi><mi>c</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{B}(i f, i c): \mathbf{B}(i b, i c) \to \mathbf{B}(i a, i c)</annotation></semantics></math> has a left adjoint</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mo stretchy="false">(</mo><msup><mi>f</mi> <mo>*</mo></msup><mo>,</mo><mi>i</mi><mi>c</mi><mo stretchy="false">)</mo><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mo stretchy="false">(</mo><mi>i</mi><mi>a</mi><mo>,</mo><mi>i</mi><mi>c</mi><mo stretchy="false">)</mo><mo>→</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mo stretchy="false">(</mo><mi>i</mi><mi>b</mi><mo>,</mo><mi>i</mi><mi>c</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{B}(f^\ast, i c): \mathbf{B}(i a, i c) \to \mathbf{B}(i b, i c)</annotation></semantics></math></div> <p>and similarly each <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mo stretchy="false">(</mo><mi>i</mi><mi>c</mi><mo>,</mo><mi>i</mi><mi>f</mi><mo stretchy="false">)</mo><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mo stretchy="false">(</mo><mi>i</mi><mi>c</mi><mo>,</mo><mi>i</mi><mi>a</mi><mo stretchy="false">)</mo><mo>→</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mo stretchy="false">(</mo><mi>i</mi><mi>c</mi><mo>,</mo><mi>i</mi><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{B}(i c, i f): \mathbf{B}(i c, i a) \to \mathbf{B}(i c, i b)</annotation></semantics></math> has a right adjoint <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mo stretchy="false">(</mo><mi>i</mi><mi>c</mi><mo>,</mo><msup><mi>f</mi> <mo>*</mo></msup><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{B}(i c, f^\ast)</annotation></semantics></math>.</p> <p>Thus, each cartesian bicategory gives rise to an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ob</mi><mo stretchy="false">(</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Ob(\mathbf{B})</annotation></semantics></math>-indexed family <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mo stretchy="false">(</mo><mi>i</mi><mo>−</mo><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{B}(i-, c)</annotation></semantics></math> of what we shall call ([faute de mieux]) generalized coherent hyperdoctrines:</p> <div class="un_def"> <h6 id="definition">Definition</h6> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> be a 2-category with 2-products. A <strong>generalized coherent hyperdoctrine</strong> over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> is a 2-functor</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>:</mo><msup><mi>C</mi> <mi>op</mi></msup><mo>→</mo><mi>FPCat</mi></mrow><annotation encoding="application/x-tex">P: C^{op} \to FPCat</annotation></semantics></math></div> <p>to the 2-category of categories with finite products, such that for each 1-cell <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>, the functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(f)</annotation></semantics></math> has a left adjoint.</p> </div> <p>This is called a generalized coherent hyperdoctrine because it deals with a generalized form of coherent logic (involving finite “conjunctions”, i.e., local finite cartesian products and existential quantifiers <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo>∃</mo> <mi>f</mi></msub><mo>⊣</mo><mi>P</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\exists_f \dashv P(f)</annotation></semantics></math>). It is actually a weak form of coherent logic because we have not included finite “disjunctions”, and we have said nothing yet about appropriate Beck-Chevalley conditions. (More will be said on this in a <a href="#frobenius">section to follow</a>.) It is generalized in the sense that the base category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> is actually a 2-category.</p> <p>If the symmetric monoidal bicategory <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{B}</annotation></semantics></math> is <em>compact</em> (e.g., if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{B}</annotation></semantics></math> is of type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Rel</mi> <mi>C</mi></msub></mrow><annotation encoding="application/x-tex">Rel_C</annotation></semantics></math> for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> a regular category, or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Span</mi> <mi>C</mi></msub></mrow><annotation encoding="application/x-tex">Span_C</annotation></semantics></math> for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> a finitely complete category, or the bicategory of small categories and profunctors between them), then without loss of generality, we may restrict attention to the single hyperdoctrine</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mo stretchy="false">(</mo><mi>i</mi><mo>−</mo><mo>,</mo><mn>1</mn><mo stretchy="false">)</mo><mo>:</mo><mi>Map</mi><mo stretchy="false">(</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><msup><mo stretchy="false">)</mo> <mi>op</mi></msup><mo>→</mo><mi>FPCat</mi></mrow><annotation encoding="application/x-tex">\mathbf{B}(i-, 1): Map(\mathbf{B})^{op} \to FPCat</annotation></semantics></math></div> <h2 id="frobenius">Frobenius conditions</h2> <p>A major class of examples of cartesian bicategories, including <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Rel</mi></mrow><annotation encoding="application/x-tex">Rel</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Span</mi></mrow><annotation encoding="application/x-tex">Span</annotation></semantics></math>, and the bicategory of profunctors between groupoids, have the properties that</p> <ul> <li> <p>Each object is self-dual (in the sense of compact closed bicategories),</p> </li> <li> <p>The bicategory of maps is locally groupoidal.</p> </li> </ul> <p>These arise as follows. In any cartesian bicategory and for each object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi></mrow><annotation encoding="application/x-tex">b</annotation></semantics></math>, there is a canonical 2-cell</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>Frob</mi> <mi>b</mi></msub><mo>:</mo><mo stretchy="false">(</mo><mi>δ</mi><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>δ</mi><mi>b</mi><msup><mo stretchy="false">)</mo> <mo>*</mo></msup><mo>→</mo><mo stretchy="false">(</mo><msub><mn>1</mn> <mi>b</mi></msub><mo>⊗</mo><mi>δ</mi><msup><mi>b</mi> <mo>*</mo></msup><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>δ</mi><mi>b</mi><mo>⊗</mo><msub><mn>1</mn> <mi>b</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Frob_b: (\delta b)(\delta b)^\ast \to (1_b \otimes \delta b^\ast)(\delta b \otimes 1_b)</annotation></semantics></math></div> <p>mated to the coassociativity isomorphism for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>δ</mi></mrow><annotation encoding="application/x-tex">\delta</annotation></semantics></math>. We say the <strong>Frobenius condition</strong> holds if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Frob</mi> <mi>b</mi></msub></mrow><annotation encoding="application/x-tex">Frob_b</annotation></semantics></math> is an isomorphism for each <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi></mrow><annotation encoding="application/x-tex">b</annotation></semantics></math>. This is equivalent to demanding that a similar canonical 2-cell</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>Frob</mi> <mi>b</mi></msub><mo>′</mo><mo>:</mo><mo stretchy="false">(</mo><mi>δ</mi><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>δ</mi><mi>b</mi><msup><mo stretchy="false">)</mo> <mo>*</mo></msup><mo>→</mo><mo stretchy="false">(</mo><mi>δ</mi><msup><mi>b</mi> <mo>*</mo></msup><mo>⊗</mo><msub><mn>1</mn> <mi>b</mi></msub><mo stretchy="false">)</mo><mo stretchy="false">(</mo><msub><mn>1</mn> <mi>b</mi></msub><mo>⊗</mo><mi>δ</mi><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Frob_{b}': (\delta b)(\delta b)^\ast \to (\delta b^\ast \otimes 1_b)(1_b \otimes \delta b)</annotation></semantics></math></div> <p>be an isomorphism for each <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi></mrow><annotation encoding="application/x-tex">b</annotation></semantics></math>.</p> <h2 id="references">References</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Aurelio+Carboni">Aurelio Carboni</a>, <a class="existingWikiWord" href="/nlab/show/Bob+Walters">Bob Walters</a>, <em>Cartesian Bicategories, I</em>, Journal of Pure and Applied Algebra, Volume 49, Issues 1–2, November 1987, (<a href="https://doi.org/10.1016/0022-4049(87)90121-6">doi:10.1016/0022-4049(87)90121-6</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Aurelio+Carboni">Aurelio Carboni</a>, <a class="existingWikiWord" href="/nlab/show/Max+Kelly">Max Kelly</a>, <a class="existingWikiWord" href="/nlab/show/Bob+Walters">Bob Walters</a>, <a class="existingWikiWord" href="/nlab/show/Richard+Wood">Richard Wood</a>, <em>Cartesian Bicategories II</em>, Theory and Applications of Categories, Vol. 19, 2008, No. 6, pp 93-124. (<a href="https://arxiv.org/abs/0708.1921">arXiv:0708.1921</a>, <a href="http://www.tac.mta.ca/tac/volumes/19/6/19-06abs.html">tac:19-06</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Evan+Patterson">Evan Patterson</a>, <em>Transposing cartesian and other structure in double categories</em>, <a href="https://arxiv.org/abs/2404.08835">arXiv</a>, 2024</p> </li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on April 16, 2024 at 05:45:41. See the <a href="/nlab/history/cartesian+bicategory" style="color: #005c19">history</a> of this page for a list of all contributions to it. </p> </div> <div class="navigation navfoot"> <a href="/nlab/edit/cartesian+bicategory" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/11463/#Item_4">Discuss</a><span class="backintime"><a href="/nlab/revision/cartesian+bicategory/26" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/cartesian+bicategory" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/cartesian+bicategory" accesskey="S" class="navlink" id="history" rel="nofollow">History (26 revisions)</a> <a href="/nlab/show/cartesian+bicategory/cite" style="color: black">Cite</a> <a href="/nlab/print/cartesian+bicategory" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/cartesian+bicategory" id="view_source" rel="nofollow">Source</a> </div> </div> <!-- Content --> </div> <!-- Container --> </body> </html>