CINXE.COM

<!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> span 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[/*></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[//><!]]> </script> <script type="text/javascript"> <![CDATA[//><!]]> </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> span </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/13612/#Item_9" 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> <blockquote> <p>This entry is about the notion of spans/correspondences which generalizes that of <em><a class="existingWikiWord" href="/nlab/show/relations">relations</a></em>. For spans in <a class="existingWikiWord" href="/nlab/show/vector+spaces">vector spaces</a> or <a class="existingWikiWord" href="/nlab/show/modules">modules</a>, see <em><a class="existingWikiWord" href="/nlab/show/linear+span">linear span</a></em>.</p> </blockquote> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <h4 id="relations">Relations</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/relation">relation</a></strong>, <a class="existingWikiWord" href="/nlab/show/internal+relation">internal relation</a></p> <p><strong><a class="existingWikiWord" href="/nlab/show/Rel">Rel</a></strong>, <a class="existingWikiWord" href="/nlab/show/bicategory+of+relations">bicategory of relations</a>, <a class="existingWikiWord" href="/nlab/show/allegory">allegory</a></p> <h2 id="types_of_binary_relation">Types of Binary relation</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/reflexive+relation">reflexive</a>, <a class="existingWikiWord" href="/nlab/show/irreflexive+relation">irreflexive</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/symmetric+relation">symmetric</a>, <a class="existingWikiWord" href="/nlab/show/antisymmetric+relation">antisymmetric</a> <a class="existingWikiWord" href="/nlab/show/asymmetric+relation">asymmetric</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/transitive+relation">transitive</a>, <a class="existingWikiWord" href="/nlab/show/comparison">comparison</a>;</p> </li> <li> <p>left and right <a class="existingWikiWord" href="/nlab/show/euclidean+relation">euclidean</a>;</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/total+relation">total</a>, <a class="existingWikiWord" href="/nlab/show/connected+relation">connected</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/extensional+relation">extensional</a>, <a class="existingWikiWord" href="/nlab/show/well-founded+relation">well-founded</a> relations.</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/functional+relations">functional relations</a>,</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/entire+relations">entire relations</a>,</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/equivalence+relations">equivalence relations</a>, <a class="existingWikiWord" href="/nlab/show/congruence">congruence</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/apartness+relations">apartness relations</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/simple+graph">simple graph</a></p> </li> </ul> <h2 id="in_higher_category_theory">In higher category theory</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/2-congruence">2-congruence</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28n%2Cr%29-congruence">(n,r)-congruence</a></p> </li> </ul> <div> <p> <a href="/nlab/edit/relations+-+contents">Edit this sidebar</a> </p> </div></div></div> <h4 id="set_theory">Set theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a></strong></p> <ul> <li>fundamentals of set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/propositional+logic">propositional logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/first-order+logic">first-order logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/typed+predicate+logic">typed predicate logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a></li> <li><a class="existingWikiWord" href="/nlab/show/set">set</a>, <a class="existingWikiWord" href="/nlab/show/element">element</a>, <a class="existingWikiWord" href="/nlab/show/function">function</a>, <a class="existingWikiWord" href="/nlab/show/relation">relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/universe">universe</a>, <a class="existingWikiWord" href="/nlab/show/small+set">small set</a>, <a class="existingWikiWord" href="/nlab/show/large+set">large set</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a>, <a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a></li> <li><a class="existingWikiWord" href="/nlab/show/pairing+structure">pairing structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+pairing">axiom of pairing</a></li> <li><a class="existingWikiWord" href="/nlab/show/union+structure">union structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+union">axiom of union</a></li> <li><a class="existingWikiWord" href="/nlab/show/powerset+structure">powerset structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+power+sets">axiom of power sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/natural+numbers+structure">natural numbers structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a></li> </ul> </li> <li>presentations of set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/first-order+set+theory">first-order set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/unsorted+set+theory">unsorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/simply+sorted+set+theory">simply sorted set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/one-sorted+set+theory">one-sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/two-sorted+set+theory">two-sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/three-sorted+set+theory">three-sorted set theory</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/dependently+sorted+set+theory">dependently sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/structurally+presented+set+theory">structurally presented set theory</a></li> </ul> </li> <li>structuralism in set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a></li> <li><a class="existingWikiWord" href="/nlab/show/ZFA">ZFA</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski+set+theory">Mostowski set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/New+Foundations">New Foundations</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/categorical+set+theory">categorical set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/fully+formal+ETCS">fully formal ETCS</a></li> <li><a class="existingWikiWord" href="/nlab/show/ETCS+with+elements">ETCS with elements</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+I">Trimble on ETCS I</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+II">Trimble on ETCS II</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+III">Trimble on ETCS III</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/structural+ZFC">structural ZFC</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/allegorical+set+theory">allegorical set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/SEAR">SEAR</a></li> </ul> </li> </ul> </li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/class-set+theory">class-set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/class">class</a>, <a class="existingWikiWord" href="/nlab/show/proper+class">proper class</a></li> <li><a class="existingWikiWord" href="/nlab/show/universal+class">universal class</a>, <a class="existingWikiWord" href="/nlab/show/universe">universe</a></li> <li><a class="existingWikiWord" href="/nlab/show/category+of+classes">category of classes</a></li> <li><a class="existingWikiWord" href="/nlab/show/category+with+class+structure">category with class structure</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/constructive+set+theory">constructive set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/algebraic+set+theory">algebraic set theory</a></li> </ul> </div></div> <h4 id="type_theory">Type theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/natural+deduction">natural deduction</a></strong> <a class="existingWikiWord" href="/nlab/show/metalanguage">metalanguage</a>, <a class="existingWikiWord" href="/nlab/show/practical+foundations">practical foundations</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/judgement">judgement</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/hypothetical+judgement">hypothetical judgement</a>, <a class="existingWikiWord" href="/nlab/show/sequent">sequent</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/antecedents">antecedents</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊢</mo></mrow><annotation encoding="application/x-tex">\vdash</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/consequent">consequent</a>, <a class="existingWikiWord" href="/nlab/show/succedents">succedents</a></li> </ul> </li> </ul> <ol> <li><a class="existingWikiWord" href="/nlab/show/type+formation+rule">type formation rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/term+introduction+rule">term introduction rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/term+elimination+rule">term elimination rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/computation+rule">computation rule</a></li> </ol> <p><strong><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></strong> (<a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent</a>, <a class="existingWikiWord" href="/nlab/show/intensional+type+theory">intensional</a>, <a class="existingWikiWord" href="/nlab/show/observational+type+theory">observational type theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>)</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/calculus+of+constructions">calculus of constructions</a></li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/syntax">syntax</a></strong> <a class="existingWikiWord" href="/nlab/show/object+language">object language</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/theory">theory</a>, <a class="existingWikiWord" href="/nlab/show/axiom">axiom</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a>/<a class="existingWikiWord" href="/nlab/show/type">type</a> (<a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/definition">definition</a>/<a class="existingWikiWord" href="/nlab/show/proof">proof</a>/<a class="existingWikiWord" href="/nlab/show/program">program</a> (<a class="existingWikiWord" href="/nlab/show/proofs+as+programs">proofs as programs</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/theorem">theorem</a></p> </li> </ul> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/computational+trinitarianism">computational trinitarianism</a></strong> = <br /> <strong><a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a></strong> +<strong><a class="existingWikiWord" href="/nlab/show/programs+as+proofs">programs as proofs</a></strong> +<strong><a class="existingWikiWord" href="/nlab/show/relation+between+type+theory+and+category+theory">relation type theory/category theory</a></strong></p> <table><thead><tr><th><a class="existingWikiWord" href="/nlab/show/logic">logic</a></th><th><a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> (<a class="existingWikiWord" href="/nlab/show/internal+logic+of+set+theory">internal logic</a> of)</th><th><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></th><th><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></th></tr></thead><tbody><tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object">object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type">type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/predicate">predicate</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/family+of+sets">family of sets</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/display+morphism">display morphism</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+type">dependent type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proof">proof</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/element">element</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/generalized+element">generalized element</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/term">term</a>/<a class="existingWikiWord" href="/nlab/show/program">program</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cut+rule">cut rule</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/composition">composition</a> of <a class="existingWikiWord" href="/nlab/show/classifying+morphisms">classifying morphisms</a> / <a class="existingWikiWord" href="/nlab/show/pullback">pullback</a> of <a class="existingWikiWord" href="/nlab/show/display+maps">display maps</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/substitution">substitution</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/introduction+rule">introduction rule</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/counit">counit</a> for hom-tensor adjunction</td><td style="text-align: left;">lambda</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/elimination+rule">elimination rule</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/unit">unit</a> for hom-tensor adjunction</td><td style="text-align: left;">application</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cut+elimination">cut elimination</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;">one of the <a class="existingWikiWord" href="/nlab/show/zigzag+identities">zigzag identities</a> for hom-tensor adjunction</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/beta+reduction">beta reduction</a></td></tr> <tr><td style="text-align: left;">identity elimination for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;">the other <a class="existingWikiWord" href="/nlab/show/zigzag+identity">zigzag identity</a> for hom-tensor adjunction</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/eta+conversion">eta conversion</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/true">true</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/singleton">singleton</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a>/<a class="existingWikiWord" href="/nlab/show/%28-2%29-truncated+object">(-2)-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-level+0">h-level 0</a>-<a class="existingWikiWord" href="/nlab/show/type">type</a>/<a class="existingWikiWord" href="/nlab/show/unit+type">unit type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/false">false</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/empty+set">empty set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/initial+object">initial object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/empty+type">empty type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a>, <a class="existingWikiWord" href="/nlab/show/truth+value">truth value</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subterminal+object">subterminal object</a>/<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncated+object">(-1)-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>, <a class="existingWikiWord" href="/nlab/show/mere+proposition">mere proposition</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/logical+conjunction">logical conjunction</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cartesian+product">cartesian product</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/product">product</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/product+type">product type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/disjunction">disjunction</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> (<a class="existingWikiWord" href="/nlab/show/support">support</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coproduct">coproduct</a> (<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/sum+type">sum type</a> (<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a> of)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+set">function set</a> (into <a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> (into <a class="existingWikiWord" href="/nlab/show/subterminal+object">subterminal object</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+type">function type</a> (into <a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/negation">negation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+set">function set</a> into <a class="existingWikiWord" href="/nlab/show/empty+set">empty set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> into <a class="existingWikiWord" href="/nlab/show/initial+object">initial object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+type">function type</a> into <a class="existingWikiWord" href="/nlab/show/empty+type">empty type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/universal+quantification">universal quantification</a></td><td style="text-align: left;">indexed <a class="existingWikiWord" href="/nlab/show/cartesian+product">cartesian product</a> (of family of <a class="existingWikiWord" href="/nlab/show/subsingletons">subsingletons</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+product">dependent product</a> (of family of <a class="existingWikiWord" href="/nlab/show/subterminal+objects">subterminal objects</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+product+type">dependent product type</a> (of family of <a class="existingWikiWord" href="/nlab/show/h-propositions">h-propositions</a>)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/existential+quantification">existential quantification</a></td><td style="text-align: left;">indexed <a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> (<a class="existingWikiWord" href="/nlab/show/support">support</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+sum">dependent sum</a> (<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+sum+type">dependent sum type</a> (<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a> of)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/logical+equivalence">logical equivalence</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/bijection+set">bijection set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object+of+isomorphisms">object of isomorphisms</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equivalence+type">equivalence type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/support+set">support set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/support+object">support object</a>/<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/propositional+truncation">propositional truncation</a>/<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/n-image">n-image</a> of <a class="existingWikiWord" href="/nlab/show/morphism">morphism</a> into <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a>/<a class="existingWikiWord" href="/nlab/show/n-truncation">n-truncation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/n-truncation+modality">n-truncation modality</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equality">equality</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/diagonal+function">diagonal function</a>/<a class="existingWikiWord" href="/nlab/show/diagonal+subset">diagonal subset</a>/<a class="existingWikiWord" href="/nlab/show/diagonal+relation">diagonal relation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/path+space+object">path space object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/identity+type">identity type</a>/<a class="existingWikiWord" href="/nlab/show/path+type">path type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/completely+presented+set">completely presented set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/discrete+object">discrete object</a>/<a class="existingWikiWord" href="/nlab/show/0-truncated+object">0-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-level+2">h-level 2</a>-<a class="existingWikiWord" href="/nlab/show/type">type</a>/<a class="existingWikiWord" href="/nlab/show/set">set</a>/<a class="existingWikiWord" href="/nlab/show/h-set">h-set</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a> with <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/groupoid+object+in+an+%28infinity%2C1%29-category">internal 0-groupoid</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Bishop+set">Bishop set</a>/<a class="existingWikiWord" href="/nlab/show/setoid">setoid</a> with its <a class="existingWikiWord" href="/nlab/show/pseudo-equivalence+relation">pseudo-equivalence relation</a> an actual <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equivalence+class">equivalence class</a>/<a class="existingWikiWord" href="/nlab/show/quotient+set">quotient set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient">quotient</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient+type">quotient type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/induction">induction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/colimit">colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/inductive+type">inductive type</a>, <a class="existingWikiWord" href="/nlab/show/W-type">W-type</a>, <a class="existingWikiWord" href="/nlab/show/M-type">M-type</a></td></tr> <tr><td style="text-align: left;">higher <a class="existingWikiWord" href="/nlab/show/induction">induction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-colimit">higher colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/higher+inductive+type">higher inductive type</a></td></tr> <tr><td style="text-align: left;">-</td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/0-truncated">0-truncated</a> <a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-colimit">higher colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient+inductive+type">quotient inductive type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coinduction">coinduction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/limit">limit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coinductive+type">coinductive type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/preset">preset</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type">type</a> without <a class="existingWikiWord" href="/nlab/show/identity+types">identity types</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a> of <a class="existingWikiWord" href="/nlab/show/truth+values">truth values</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subobject+classifier">subobject classifier</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type+of+propositions">type of propositions</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/domain+of+discourse">domain of discourse</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/universe">universe</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object+classifier">object classifier</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type+universe">type universe</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/modality">modality</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/closure+operator">closure operator</a>, (<a class="existingWikiWord" href="/nlab/show/idempotent+monad">idempotent</a>) <a class="existingWikiWord" href="/nlab/show/monad">monad</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/modal+type+theory">modal type theory</a>, <a class="existingWikiWord" href="/nlab/show/monad+%28in+computer+science%29">monad (in computer science)</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+logic">linear logic</a></td><td style="text-align: left;"></td><td style="text-align: left;">(<a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+category">symmetric</a>, <a class="existingWikiWord" href="/nlab/show/closed+monoidal+category">closed</a>) <a class="existingWikiWord" href="/nlab/show/monoidal+category">monoidal category</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+type+theory">linear type theory</a>/<a class="existingWikiWord" href="/nlab/show/quantum+computation">quantum computation</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proof+net">proof net</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/string+diagram">string diagram</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quantum+circuit">quantum circuit</a></td></tr> <tr><td style="text-align: left;">(absence of) <a class="existingWikiWord" href="/nlab/show/contraction+rule">contraction rule</a></td><td style="text-align: left;"></td><td style="text-align: left;">(absence of) <a class="existingWikiWord" href="/nlab/show/diagonal">diagonal</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/no-cloning+theorem">no-cloning theorem</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/synthetic+mathematics">synthetic mathematics</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/domain+specific+embedded+programming+language">domain specific embedded programming language</a></td></tr> </tbody></table> </div> <p><strong><a class="existingWikiWord" href="/nlab/show/homotopy+levels">homotopy levels</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/2-type+theory">2-type theory</a>, <a class="existingWikiWord" href="/michaelshulman/show/2-categorical+logic">2-categorical logic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory+-+contents">homotopy type theory - contents</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+type">homotopy type</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/univalence">univalence</a>, <a class="existingWikiWord" href="/nlab/show/function+extensionality">function extensionality</a>, <a class="existingWikiWord" href="/nlab/show/internal+logic+of+an+%28%E2%88%9E%2C1%29-topos">internal logic of an (∞,1)-topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cohesive+homotopy+type+theory">cohesive homotopy type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/directed+homotopy+type+theory">directed homotopy type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/HoTT+methods+for+homotopy+theorists">HoTT methods for homotopy theorists</a></p> </li> </ul> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/semantics">semantics</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a>, <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/display+map">display map</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic+of+a+topos">internal logic of a topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Mitchell-Benabou+language">Mitchell-Benabou language</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kripke-Joyal+semantics">Kripke-Joyal semantics</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic+of+an+%28%E2%88%9E%2C1%29-topos">internal logic of an (∞,1)-topos</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/type-theoretic+model+category">type-theoretic model category</a></li> </ul> </li> </ul> <div> <p> <a href="/nlab/edit/type+theory+-+contents">Edit this sidebar</a> </p> </div></div></div> <h4 id="category_theory">Category theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></strong></p> <h2 id="sidebar_concepts">Concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/category">category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/functor">functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/natural+transformation">natural transformation</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Cat">Cat</a></p> </li> </ul> <h2 id="sidebar_universal_constructions">Universal constructions</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/universal+construction">universal construction</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/representable+functor">representable functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/adjoint+functor">adjoint functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/limit">limit</a>/<a class="existingWikiWord" href="/nlab/show/colimit">colimit</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/weighted+limit">weighted limit</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/end">end</a>/<a class="existingWikiWord" href="/nlab/show/coend">coend</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kan+extension">Kan extension</a></p> </li> </ul> </li> </ul> <h2 id="sidebar_theorems">Theorems</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Yoneda+lemma">Yoneda lemma</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Isbell+duality">Isbell duality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Grothendieck+construction">Grothendieck construction</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/adjoint+functor+theorem">adjoint functor theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/monadicity+theorem">monadicity theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/adjoint+lifting+theorem">adjoint lifting theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Tannaka+duality">Tannaka duality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Gabriel-Ulmer+duality">Gabriel-Ulmer duality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/small+object+argument">small object argument</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Freyd-Mitchell+embedding+theorem">Freyd-Mitchell embedding theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/relation+between+type+theory+and+category+theory">relation between type theory and category theory</a></p> </li> </ul> <h2 id="sidebar_extensions">Extensions</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/sheaf+and+topos+theory">sheaf and topos theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/enriched+category+theory">enriched category theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher+category+theory">higher category theory</a></p> </li> </ul> <h2 id="sidebar_applications">Applications</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/applications+of+%28higher%29+category+theory">applications of (higher) category theory</a></li> </ul> <div> <p> <a href="/nlab/edit/category+theory+-+contents">Edit this sidebar</a> </p> </div></div></div> <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> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#definition'>Definition</a></li> <ul> <li><a href='#in_set_theory'>In set theory</a></li> <li><a href='#in_dependent_type_theory'>In dependent type theory</a></li> <li><a href='#in_category_theory'>In category theory</a></li> <li><a href='#categories_of_spans'>Categories of spans</a></li> </ul> <li><a href='#properties'>Properties</a></li> <ul> <li><a href='#the_1category_of_spans'>The 1-category of spans</a></li> <li><a href='#UniversalPropertyOfTheBicategoryOfSpans'>Universal property of the bicategory of spans</a></li> <li><a href='#LimitsAndColimits'>Limits and colimits</a></li> <li><a href='#RelationToRelations'>Relation to relations</a></li> </ul> <li><a href='#examples'>Examples</a></li> <li><a href='#related_concepts'>Related concepts</a></li> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="definition">Definition</h2> <h3 id="in_set_theory">In set theory</h3> <p>In <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a>, a <strong>span</strong> or <strong>correspondence</strong> between <a class="existingWikiWord" href="/nlab/show/sets">sets</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <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 set <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> with a <a class="existingWikiWord" href="/nlab/show/function">function</a> <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>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">R:C \to A \times B</annotation></semantics></math> to the <a class="existingWikiWord" href="/nlab/show/product+set">product set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A \times B</annotation></semantics></math>. A span between a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> itself is a <a class="existingWikiWord" href="/nlab/show/directed+pseudograph">directed pseudograph</a>, which is used to define <a class="existingWikiWord" href="/nlab/show/categories">categories</a> in set theory.</p> <h3 id="in_dependent_type_theory">In dependent type theory</h3> <p>In <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a>, there is a distinction between a <em>span</em>, a <em>multivalued partial function</em>, and a <em>correspondence</em>:</p> <ul> <li> <p>A <strong>span</strong> between types <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <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 type <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> with families of elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>C</mi><mo>⊢</mo><mi>g</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x:C \vdash g(x):A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>C</mi><mo>⊢</mo><mi>h</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>:</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">x:C \vdash h(x):B</annotation></semantics></math></p> </li> <li> <p>A <strong><a class="existingWikiWord" href="/nlab/show/multivalued+partial+function">multivalued partial function</a></strong> from type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> to type <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 type family <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:A \vdash P(x)</annotation></semantics></math> with a family of elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>p</mi><mo>:</mo><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>p</mi><mo stretchy="false">)</mo><mo>:</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">x:A, p:P(x) \vdash f(x, p):B</annotation></semantics></math></p> </li> <li> <p>A <strong>correspondence</strong> between types <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <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 type family <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>B</mi><mo>⊢</mo><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:A, y:B \vdash R(x, y)</annotation></semantics></math>.</p> </li> </ul> <p>However, from any one of the above structures, one could get the other two structures, provided one has <a class="existingWikiWord" href="/nlab/show/identity+types">identity types</a> and <a class="existingWikiWord" href="/nlab/show/dependent+pair+types">dependent pair types</a> in the dependent type theory. Given a type family <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:A \vdash P(x)</annotation></semantics></math>, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi><mo>:</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></msub><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⊢</mo><msub><mi>π</mi> <mn>1</mn></msub><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">z:\sum_{x:A} P(x) \vdash \pi_1(z):A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi><mo>:</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></msub><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⊢</mo><msub><mi>π</mi> <mn>2</mn></msub><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo>:</mo><mi>P</mi><mo stretchy="false">(</mo><msub><mi>π</mi> <mn>1</mn></msub><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">z:\sum_{x:A} P(x) \vdash \pi_2(z):P(\pi_1(z))</annotation></semantics></math> be the dependent pair projections for the <a class="existingWikiWord" href="/nlab/show/dependent+pair+type">dependent pair type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></msub><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\sum_{x:A} P(x)</annotation></semantics></math>.</p> <ul> <li> <p>From every span one could get a multivalued partial function by defining the type family <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:A \vdash P(x)</annotation></semantics></math> as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>≔</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>y</mi><mo>:</mo><mi>C</mi></mrow></msub><mi>g</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>A</mi></msub><mi>x</mi></mrow><annotation encoding="application/x-tex">P(x) \coloneqq \sum_{y:C} g(y) =_A x</annotation></semantics></math> and the family of elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>p</mi><mo>:</mo><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>p</mi><mo stretchy="false">)</mo><mo>:</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">x:A, p:P(x) \vdash f(x, p):B</annotation></semantics></math> as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>p</mi><mo stretchy="false">)</mo><mo>≔</mo><mi>h</mi><mo stretchy="false">(</mo><msub><mi>π</mi> <mn>1</mn></msub><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f(x, p) \coloneqq h(\pi_1(x))</annotation></semantics></math>.</p> </li> <li> <p>From every multivalued partial function one could get a span by defining the type <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> as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo>≔</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></msub><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">C \coloneqq \sum_{x:A} P(x)</annotation></semantics></math> and the family of elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>C</mi><mo>⊢</mo><mi>g</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x:C \vdash g(x):A</annotation></semantics></math> as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>≔</mo><msub><mi>π</mi> <mn>1</mn></msub><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">g(x) \coloneqq \pi_1(x)</annotation></semantics></math>.</p> </li> <li> <p>From every multivalued partial function one could get a correspondence by defining the type family <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>B</mi><mo>⊢</mo><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:A, y:B \vdash R(x, y)</annotation></semantics></math> as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>≔</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>p</mi><mo>:</mo><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow></msub><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>p</mi><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>B</mi></msub><mi>y</mi></mrow><annotation encoding="application/x-tex">R(x, y) \coloneqq \sum_{p:P(x)} f(x, p) =_B y</annotation></semantics></math>.</p> </li> <li> <p>From every correspondence one could get a multivalued partial function by defining the type family <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:A \vdash P(x)</annotation></semantics></math> as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>≔</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>y</mi><mo>:</mo><mi>B</mi></mrow></msub><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(x) \coloneqq \sum_{y:B} R(x, y)</annotation></semantics></math>, and the family of elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>p</mi><mo>:</mo><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>h</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>p</mi><mo stretchy="false">)</mo><mo>:</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">x:A, p:P(x) \vdash h(x, p):B</annotation></semantics></math> as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>h</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>p</mi><mo stretchy="false">)</mo><mo>≔</mo><msub><mi>π</mi> <mn>1</mn></msub><mo stretchy="false">(</mo><mi>p</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">h(x, p) \coloneqq \pi_1(p)</annotation></semantics></math></p> </li> <li> <p>From every span one could get a correspondence by defining the type family <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>B</mi><mo>⊢</mo><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:A, y:B \vdash R(x, y)</annotation></semantics></math> as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>≔</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>z</mi><mo>:</mo><mi>C</mi></mrow></msub><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>A</mi></msub><mi>x</mi><mo stretchy="false">)</mo><mo>×</mo><mo stretchy="false">(</mo><mi>h</mi><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>B</mi></msub><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">R(x, y) \coloneqq \sum_{z:C} (g(z) =_A x) \times (h(z) =_B y)</annotation></semantics></math>.</p> </li> <li> <p>From every correspondence one could get a span by defining the type <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> as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo>≔</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></msub><msub><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>y</mi><mo>:</mo><mi>B</mi></mrow></msub><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">C \coloneqq \sum_{x:A} \sum_{y:B} R(x, y)</annotation></semantics></math>, the family of elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi><mo>:</mo><mi>C</mi><mo>⊢</mo><mi>g</mi><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">z:C \vdash g(z):A</annotation></semantics></math> as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo>≔</mo><msub><mi>π</mi> <mn>1</mn></msub><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">g(z) \coloneqq \pi_1(z)</annotation></semantics></math>, and the function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi><mo>:</mo><mi>C</mi><mo>⊢</mo><mi>h</mi><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo>:</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">z:C \vdash h(z):B</annotation></semantics></math> as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>h</mi><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo>≔</mo><msub><mi>π</mi> <mn>1</mn></msub><mo stretchy="false">(</mo><msub><mi>π</mi> <mn>2</mn></msub><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">h(z) \coloneqq \pi_1(\pi_2(z))</annotation></semantics></math></p> </li> </ul> <p>Given types <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, <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> and spans <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>D</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>D</mi><mo>⊢</mo><msub><mi>g</mi> <mi>D</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>:</mo><mi>A</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>D</mi><mo>⊢</mo><msub><mi>h</mi> <mi>D</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>:</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(D, x:D \vdash g_D(x):A, x:D \vdash h_D(x):B)</annotation></semantics></math> between <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <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><mo stretchy="false">(</mo><mi>E</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>E</mi><mo>⊢</mo><msub><mi>g</mi> <mi>E</mi></msub><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo>:</mo><mi>B</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>E</mi><mo>⊢</mo><msub><mi>h</mi> <mi>E</mi></msub><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo>:</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(E, y:E \vdash g_E(y):B, y:E \vdash h_E(y):C)</annotation></semantics></math> between <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 span</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>E</mi><mo>∘</mo><mi>D</mi><mo>,</mo><mi>z</mi><mo>:</mo><mi>E</mi><mo>∘</mo><mi>D</mi><mo>⊢</mo><msub><mi>g</mi> <mrow><mi>E</mi><mo>∘</mo><mi>D</mi></mrow></msub><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo>:</mo><mi>A</mi><mo>,</mo><mi>z</mi><mo>:</mo><mi>E</mi><mo>∘</mo><mi>D</mi><mo>⊢</mo><msub><mi>h</mi> <mrow><mi>E</mi><mo>∘</mo><mi>D</mi></mrow></msub><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo>:</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(E \circ D, z:E \circ D \vdash g_{E \circ D}(z):A, z:E \circ D \vdash h_{E \circ D}(z):C)</annotation></semantics></math></div> <p>defined by</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>E</mi><mo>∘</mo><mi>D</mi><mo>≔</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>D</mi></mrow></munder><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>y</mi><mo>:</mo><mi>E</mi></mrow></munder><msub><mi>h</mi> <mi>D</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>B</mi></msub><msub><mi>g</mi> <mi>E</mi></msub><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">E \circ D \coloneqq \sum_{x:D} \sum_{y:E} h_D(x) =_B g_E(y)</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>z</mi><mo>:</mo><mi>E</mi><mo>∘</mo><mi>D</mi><mo>⊢</mo><msub><mi>g</mi> <mrow><mi>E</mi><mo>∘</mo><mi>D</mi></mrow></msub><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo>≔</mo><msub><mi>g</mi> <mi>D</mi></msub><mo stretchy="false">(</mo><msub><mi>π</mi> <mn>1</mn></msub><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">z:E \circ D \vdash g_{E \circ D}(z) \coloneqq g_D(\pi_1(z))</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>z</mi><mo>:</mo><mi>E</mi><mo>∘</mo><mi>D</mi><mo>⊢</mo><msub><mi>h</mi> <mrow><mi>E</mi><mo>∘</mo><mi>D</mi></mrow></msub><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo>≔</mo><msub><mi>h</mi> <mi>E</mi></msub><mo stretchy="false">(</mo><msub><mi>π</mi> <mn>1</mn></msub><mo stretchy="false">(</mo><msub><mi>π</mi> <mn>2</mn></msub><mo stretchy="false">(</mo><msub><mi>π</mi> <mn>1</mn></msub><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">z:E \circ D \vdash h_{E \circ D}(z) \coloneqq h_E(\pi_1(\pi_2(\pi_1(z))(z)))</annotation></semantics></math></div> <p>Given types <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, <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> and correspondences <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>B</mi><mo>⊢</mo><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:A, y:B \vdash R(x, y)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>:</mo><mi>B</mi><mo>,</mo><mi>z</mi><mo>:</mo><mi>C</mi><mo>⊢</mo><mi>S</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">y:B, z:C \vdash S(y, z)</annotation></semantics></math>, there is a correspondence <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>z</mi><mo>:</mo><mi>C</mi><mo>⊢</mo><mo stretchy="false">(</mo><mi>S</mi><mo>∘</mo><mi>R</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:A, z:C \vdash (S \circ R)(x, z)</annotation></semantics></math> defined by</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>S</mi><mo>∘</mo><mi>R</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo><mo>≔</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>y</mi><mo>:</mo><mi>B</mi></mrow></munder><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>×</mo><mi>S</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(S \circ R)(x, z) \coloneqq \sum_{y:B} R(x, y) \times S(y, z)</annotation></semantics></math></div> <h3 id="in_category_theory">In category theory</h3> <p>In any <a class="existingWikiWord" href="/nlab/show/category">category</a> <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 <strong>span</strong>, or <strong>roof</strong>, or <strong>correspondence</strong>, from an <a class="existingWikiWord" href="/nlab/show/object">object</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> to an object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/diagram">diagram</a> of 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></mtd> <mtd></mtd> <mtd><mi>s</mi></mtd></mtr> <mtr><mtd></mtd> <mtd><msup><mrow></mrow> <mi>f</mi></msup><mo>↙</mo></mtd> <mtd></mtd> <mtd><msup><mo>↘</mo> <mi>g</mi></msup></mtd></mtr> <mtr><mtd><mi>x</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>y</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array{ && s \\ & {}^{f}\swarrow && \searrow^{g} \\ x &&&& y } </annotation></semantics></math></div> <p>where <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> is some other object of the category. (The word “correspondence” is also sometimes used for a <a class="existingWikiWord" href="/nlab/show/profunctor">profunctor</a>.)</p> <p>This <a class="existingWikiWord" href="/nlab/show/diagram">diagram</a> is also called a ‘span’ because it looks like a little bridge; ‘roof’ is similar. The term ‘correspondence’ is prevalent in geometry and related areas; it comes about because a correspondence is a generalisation of a binary <a class="existingWikiWord" href="/nlab/show/relation">relation</a>.</p> <p>Note that a span with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>=</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">f = 1</annotation></semantics></math> is just a morphism from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math>, while a span with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo>=</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">g = 1</annotation></semantics></math> is a morphism from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>. So, a span can be thought of as a generalization of a morphism in which there is no longer any asymmetry between source and target.</p> <p>A span in the <a class="existingWikiWord" href="/nlab/show/opposite+category">opposite category</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>C</mi> <mi>op</mi></msup></mrow><annotation encoding="application/x-tex">C^op</annotation></semantics></math> is called a <a class="existingWikiWord" href="/nlab/show/co-span">co-span</a> 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>.</p> <p>A span that has a <a class="existingWikiWord" href="/nlab/show/cocone">cocone</a> is called a <a class="existingWikiWord" href="/nlab/show/coquadrable+span">coquadrable span</a>.</p> <h3 id="categories_of_spans">Categories of spans</h3> <p>If the 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> has <a class="existingWikiWord" href="/nlab/show/pullback">pullbacks</a>, we can compose spans. Namely, given a span from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> and a span from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi></mrow><annotation encoding="application/x-tex">z</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></mtd> <mtd></mtd> <mtd><mi>s</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>t</mi></mtd></mtr> <mtr><mtd></mtd> <mtd><msup><mrow></mrow> <mi>f</mi></msup><mo>↙</mo></mtd> <mtd></mtd> <mtd><msup><mo>↘</mo> <mi>g</mi></msup></mtd> <mtd></mtd> <mtd><msup><mrow></mrow> <mi>h</mi></msup><mo>↙</mo></mtd> <mtd></mtd> <mtd><msup><mo>↘</mo> <mi>i</mi></msup></mtd></mtr> <mtr><mtd><mi>x</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>y</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>z</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array{ && s &&&& t \\ & {}^{f}\swarrow && \searrow^{g} & & {}^{h}\swarrow && \searrow^{i} \\ x &&&& y &&&& z } </annotation></semantics></math></div> <p>we can take a pullback in the middle:</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></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>s</mi><msub><mo>×</mo> <mi>y</mi></msub><mi>t</mi></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><msup><mrow></mrow> <mrow><msub><mi>p</mi> <mi>s</mi></msub></mrow></msup><mo>↙</mo></mtd> <mtd></mtd> <mtd><msup><mo>↘</mo> <mrow><msub><mi>p</mi> <mi>t</mi></msub></mrow></msup></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd><mi>s</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>t</mi></mtd></mtr> <mtr><mtd></mtd> <mtd><msup><mrow></mrow> <mi>f</mi></msup><mo>↙</mo></mtd> <mtd></mtd> <mtd><msup><mo>↘</mo> <mi>g</mi></msup></mtd> <mtd></mtd> <mtd><msup><mrow></mrow> <mi>h</mi></msup><mo>↙</mo></mtd> <mtd></mtd> <mtd><msup><mo>↘</mo> <mi>i</mi></msup></mtd></mtr> <mtr><mtd><mi>x</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>y</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>z</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array{ &&&& s \times_y t \\& && {}^{p_s}\swarrow && \searrow^{p_t} \\ && s &&&& t \\ & {}^{f}\swarrow && \searrow^{g} & & {}^{h}\swarrow && \searrow^{i} \\ x &&&& y &&&& z } </annotation></semantics></math></div> <p>and obtain a span from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi></mrow><annotation encoding="application/x-tex">z</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></mtd> <mtd></mtd> <mtd><mi>s</mi><msub><mo>×</mo> <mi>y</mi></msub><mi>t</mi></mtd></mtr> <mtr><mtd></mtd> <mtd><msup><mrow></mrow> <mrow><mi>f</mi><msub><mi>p</mi> <mi>s</mi></msub></mrow></msup><mo>↙</mo></mtd> <mtd></mtd> <mtd><msup><mo>↘</mo> <mrow><mi>i</mi><msub><mi>p</mi> <mi>t</mi></msub></mrow></msup></mtd></mtr> <mtr><mtd><mi>x</mi></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mi>z</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array{ && s \times_y t \\ & {}^{f p_s}\swarrow && \searrow^{i p_t} \\ x &&&& z } </annotation></semantics></math></div> <p>This way of composing spans lets us define a <a class="existingWikiWord" href="/nlab/show/bicategory">bicategory</a> <a class="existingWikiWord" href="/nlab/show/Span">Span</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(C)</annotation></semantics></math> with:</p> <ul> <li>objects 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> as objects</li> <li>spans as morphisms</li> <li>maps between spans as 2-morphisms</li> </ul> <p>This is a weak 2-category: it has a nontrivial <a class="existingWikiWord" href="/nlab/show/associator">associator</a>: composition of spans is not strictly associative, because pullbacks are defined only up to canonical isomorphism. A <a class="existingWikiWord" href="/nlab/show/Lack%27s+coherence+theorem">naturally defined</a> <a class="existingWikiWord" href="/nlab/show/strict+2-category">strict 2-category</a> which is equivalent to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Span</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Span(C)</annotation></semantics></math> is the strict 2-category of <a class="existingWikiWord" href="/nlab/show/linear+polynomial+functors">linear polynomial functors</a> between <a class="existingWikiWord" href="/nlab/show/slice+categories">slice categories</a> 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>.</p> <p>(Note that we must choose a specific pullback when defining the composite of a pair of morphisms in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Span</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Span(C)</annotation></semantics></math>, if we want to obtain a <a class="existingWikiWord" href="/nlab/show/bicategory">bicategory</a> as traditionally defined; this requires the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>. Otherwise we obtain a bicategory with ‘composites of morphisms defined only up to canonical iso-2-morphism’; such a structure can be modeled by an <a class="existingWikiWord" href="/nlab/show/anabicategory">anabicategory</a> or an <span class="newWikiWord">opetopic bicategory<a href="/nlab/new/opetopic+bicategory">?</a></span>.)</p> <p>We can also obtain a <span class="newWikiWord">pseudo-double category<a href="/nlab/new/pseudo-double+category">?</a></span>, whose <a class="existingWikiWord" href="/nlab/show/loose">loose</a> structure is as above, whose <a class="existingWikiWord" href="/nlab/show/tight">tight</a> morphisms are functions, and whose cells are commuting diagrams,</p> <svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" width="194.173pt" height="93.278pt" viewBox="0 0 194.173 93.278" version="1.2"> <defs> <g> <symbol overflow="visible" id="Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph0-0"> <path style="stroke:none;" d=""></path> </symbol> <symbol overflow="visible" id="Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph0-1"> <path style="stroke:none;" d="M 2.515625 -1.640625 C 2 -0.765625 1.5 -0.46875 0.78125 -0.4375 C 0.625 -0.421875 0.5 -0.421875 0.5 -0.140625 C 0.5 -0.0625 0.578125 0 0.6875 0 C 0.953125 0 1.609375 -0.03125 1.890625 -0.03125 C 2.3125 -0.03125 2.78125 0 3.203125 0 C 3.296875 0 3.46875 0 3.46875 -0.28125 C 3.46875 -0.421875 3.34375 -0.4375 3.265625 -0.4375 C 2.921875 -0.453125 2.640625 -0.578125 2.640625 -0.9375 C 2.640625 -1.140625 2.734375 -1.3125 2.921875 -1.625 L 4.046875 -3.5 L 7.828125 -3.5 C 7.84375 -3.359375 7.84375 -3.25 7.859375 -3.109375 C 7.90625 -2.734375 8.078125 -1.1875 8.078125 -0.90625 C 8.078125 -0.453125 7.328125 -0.4375 7.09375 -0.4375 C 6.921875 -0.4375 6.765625 -0.4375 6.765625 -0.15625 C 6.765625 0 6.890625 0 6.984375 0 C 7.234375 0 7.53125 -0.03125 7.78125 -0.03125 L 8.625 -0.03125 C 9.53125 -0.03125 10.1875 0 10.203125 0 C 10.3125 0 10.46875 0 10.46875 -0.28125 C 10.46875 -0.4375 10.328125 -0.4375 10.109375 -0.4375 C 9.296875 -0.4375 9.28125 -0.5625 9.234375 -1.015625 L 8.328125 -10.265625 C 8.296875 -10.5625 8.25 -10.59375 8.078125 -10.59375 C 7.9375 -10.59375 7.84375 -10.5625 7.703125 -10.328125 Z M 4.296875 -3.921875 L 7.28125 -8.90625 L 7.78125 -3.921875 Z M 4.296875 -3.921875 "></path> </symbol> <symbol overflow="visible" id="Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph0-2"> <path style="stroke:none;" d="M 9.421875 -10.3125 C 9.421875 -10.4375 9.3125 -10.4375 9.28125 -10.4375 C 9.21875 -10.4375 9.203125 -10.421875 9.03125 -10.203125 C 8.9375 -10.09375 8.328125 -9.328125 8.3125 -9.3125 C 7.828125 -10.28125 6.84375 -10.4375 6.234375 -10.4375 C 4.34375 -10.4375 2.640625 -8.71875 2.640625 -7.046875 C 2.640625 -5.9375 3.3125 -5.28125 4.03125 -5.03125 C 4.203125 -4.96875 5.078125 -4.734375 5.515625 -4.625 C 6.265625 -4.421875 6.46875 -4.359375 6.78125 -4.03125 C 6.828125 -3.953125 7.125 -3.625 7.125 -2.921875 C 7.125 -1.546875 5.859375 -0.125 4.375 -0.125 C 3.15625 -0.125 1.8125 -0.640625 1.8125 -2.296875 C 1.8125 -2.578125 1.875 -2.9375 1.90625 -3.078125 C 1.90625 -3.125 1.921875 -3.203125 1.921875 -3.234375 C 1.921875 -3.296875 1.890625 -3.359375 1.78125 -3.359375 C 1.640625 -3.359375 1.625 -3.34375 1.578125 -3.078125 L 0.8125 -0.046875 C 0.8125 -0.03125 0.75 0.15625 0.75 0.171875 C 0.75 0.3125 0.875 0.3125 0.90625 0.3125 C 0.96875 0.3125 0.984375 0.296875 1.15625 0.078125 L 1.84375 -0.8125 C 2.1875 -0.28125 2.96875 0.3125 4.34375 0.3125 C 6.25 0.3125 8 -1.546875 8 -3.390625 C 8 -4.015625 7.859375 -4.5625 7.296875 -5.109375 C 6.984375 -5.421875 6.71875 -5.5 5.359375 -5.859375 C 4.359375 -6.125 4.21875 -6.171875 3.953125 -6.40625 C 3.703125 -6.65625 3.515625 -7.015625 3.515625 -7.515625 C 3.515625 -8.765625 4.78125 -10.03125 6.1875 -10.03125 C 7.640625 -10.03125 8.3125 -9.15625 8.3125 -7.734375 C 8.3125 -7.359375 8.25 -6.953125 8.25 -6.890625 C 8.25 -6.765625 8.359375 -6.765625 8.40625 -6.765625 C 8.546875 -6.765625 8.5625 -6.8125 8.609375 -7.046875 Z M 9.421875 -10.3125 "></path> </symbol> <symbol overflow="visible" id="Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph0-3"> <path style="stroke:none;" d="M 5.421875 -9.125 C 5.5625 -9.671875 5.625 -9.703125 6.203125 -9.703125 L 8.125 -9.703125 C 9.796875 -9.703125 9.796875 -8.28125 9.796875 -8.140625 C 9.796875 -6.9375 8.59375 -5.40625 6.640625 -5.40625 L 4.5 -5.40625 Z M 7.9375 -5.296875 C 9.546875 -5.59375 11.015625 -6.71875 11.015625 -8.078125 C 11.015625 -9.234375 10 -10.125 8.3125 -10.125 L 3.5625 -10.125 C 3.28125 -10.125 3.140625 -10.125 3.140625 -9.84375 C 3.140625 -9.703125 3.28125 -9.703125 3.5 -9.703125 C 4.40625 -9.703125 4.40625 -9.578125 4.40625 -9.421875 C 4.40625 -9.390625 4.40625 -9.296875 4.34375 -9.078125 L 2.34375 -1.09375 C 2.203125 -0.578125 2.1875 -0.4375 1.140625 -0.4375 C 0.859375 -0.4375 0.71875 -0.4375 0.71875 -0.15625 C 0.71875 0 0.796875 0 1.09375 0 L 6.1875 0 C 8.453125 0 10.203125 -1.71875 10.203125 -3.21875 C 10.203125 -4.4375 9.140625 -5.171875 7.9375 -5.296875 Z M 5.828125 -0.4375 L 3.828125 -0.4375 C 3.625 -0.4375 3.59375 -0.4375 3.5 -0.4375 C 3.34375 -0.453125 3.328125 -0.484375 3.328125 -0.609375 C 3.328125 -0.71875 3.34375 -0.796875 3.375 -0.9375 L 4.421875 -5.109375 L 7.203125 -5.109375 C 8.953125 -5.109375 8.953125 -3.484375 8.953125 -3.359375 C 8.953125 -1.9375 7.671875 -0.4375 5.828125 -0.4375 Z M 5.828125 -0.4375 "></path> </symbol> <symbol overflow="visible" id="Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph1-0"> <path style="stroke:none;" d=""></path> </symbol> <symbol overflow="visible" id="Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph1-1"> <path style="stroke:none;" d="M 2.625 -4.6875 C 2.671875 -4.8125 2.703125 -4.890625 2.703125 -4.984375 C 2.703125 -5.3125 2.40625 -5.53125 2.140625 -5.53125 C 1.734375 -5.53125 1.625 -5.1875 1.59375 -5.046875 L 0.34375 -0.78125 C 0.296875 -0.65625 0.296875 -0.640625 0.296875 -0.625 C 0.296875 -0.53125 0.359375 -0.515625 0.453125 -0.484375 C 0.640625 -0.40625 0.65625 -0.40625 0.671875 -0.40625 C 0.703125 -0.40625 0.765625 -0.40625 0.828125 -0.578125 Z M 2.625 -4.6875 "></path> </symbol> <symbol overflow="visible" id="Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph2-0"> <path style="stroke:none;" d=""></path> </symbol> <symbol overflow="visible" id="Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph2-1"> <path style="stroke:none;" d="M 0.515625 1.203125 C 0.4375 1.515625 0.421875 1.59375 0.015625 1.59375 C -0.125 1.59375 -0.234375 1.59375 -0.234375 1.78125 C -0.234375 1.875 -0.140625 1.921875 -0.09375 1.921875 C 0 1.921875 0.046875 1.890625 0.765625 1.890625 C 1.484375 1.890625 1.6875 1.921875 1.765625 1.921875 C 1.796875 1.921875 1.953125 1.921875 1.953125 1.734375 C 1.953125 1.59375 1.8125 1.59375 1.6875 1.59375 C 1.21875 1.59375 1.21875 1.53125 1.21875 1.4375 C 1.21875 1.375 1.390625 0.671875 1.6875 -0.484375 C 1.8125 -0.25 2.125 0.09375 2.65625 0.09375 C 3.875 0.09375 5.140625 -1.3125 5.140625 -2.734375 C 5.140625 -3.71875 4.515625 -4.359375 3.71875 -4.359375 C 3.125 -4.359375 2.65625 -3.953125 2.359375 -3.65625 C 2.15625 -4.359375 1.5 -4.359375 1.390625 -4.359375 C 1.03125 -4.359375 0.796875 -4.140625 0.640625 -3.828125 C 0.40625 -3.375 0.296875 -2.875 0.296875 -2.84375 C 0.296875 -2.765625 0.359375 -2.71875 0.4375 -2.71875 C 0.578125 -2.71875 0.578125 -2.765625 0.65625 -3.015625 C 0.78125 -3.515625 0.953125 -4.078125 1.359375 -4.078125 C 1.609375 -4.078125 1.6875 -3.859375 1.6875 -3.625 C 1.6875 -3.515625 1.640625 -3.28125 1.625 -3.203125 Z M 2.328125 -3.046875 C 2.390625 -3.21875 2.390625 -3.234375 2.53125 -3.40625 C 2.90625 -3.859375 3.328125 -4.078125 3.6875 -4.078125 C 4.1875 -4.078125 4.375 -3.59375 4.375 -3.15625 C 4.375 -2.796875 4.15625 -1.734375 3.859375 -1.140625 C 3.59375 -0.609375 3.125 -0.171875 2.65625 -0.171875 C 1.984375 -0.171875 1.828125 -0.953125 1.828125 -1.015625 C 1.828125 -1.03125 1.84375 -1.140625 1.859375 -1.171875 Z M 2.328125 -3.046875 "></path> </symbol> <symbol overflow="visible" id="Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph2-2"> <path style="stroke:none;" d="M 3.78125 -3.9375 L 4.703125 -3.9375 C 4.90625 -3.9375 5.03125 -3.9375 5.03125 -4.125 C 5.03125 -4.265625 4.890625 -4.265625 4.734375 -4.265625 L 3.84375 -4.265625 C 4 -5.15625 4.109375 -5.71875 4.203125 -6.15625 C 4.25 -6.328125 4.265625 -6.4375 4.421875 -6.5625 C 4.546875 -6.671875 4.625 -6.6875 4.734375 -6.6875 C 4.890625 -6.6875 5.046875 -6.65625 5.171875 -6.578125 C 5.125 -6.5625 5.0625 -6.53125 5.015625 -6.5 C 4.84375 -6.40625 4.734375 -6.234375 4.734375 -6.03125 C 4.734375 -5.8125 4.90625 -5.671875 5.125 -5.671875 C 5.40625 -5.671875 5.671875 -5.921875 5.671875 -6.265625 C 5.671875 -6.71875 5.203125 -6.96875 4.734375 -6.96875 C 4.390625 -6.96875 3.765625 -6.8125 3.453125 -5.890625 C 3.359375 -5.671875 3.359375 -5.640625 3.09375 -4.265625 L 2.359375 -4.265625 C 2.15625 -4.265625 2.03125 -4.265625 2.03125 -4.078125 C 2.03125 -3.9375 2.171875 -3.9375 2.328125 -3.9375 L 3.03125 -3.9375 L 2.328125 -0.09375 C 2.140625 0.90625 1.984375 1.734375 1.46875 1.734375 C 1.4375 1.734375 1.21875 1.734375 1.03125 1.625 C 1.5 1.515625 1.5 1.09375 1.5 1.09375 C 1.5 0.859375 1.3125 0.71875 1.09375 0.71875 C 0.828125 0.71875 0.546875 0.953125 0.546875 1.328125 C 0.546875 1.734375 0.96875 2.015625 1.46875 2.015625 C 2.0625 2.015625 2.484375 1.390625 2.609375 1.140625 C 2.96875 0.484375 3.1875 -0.75 3.21875 -0.84375 Z M 3.78125 -3.9375 "></path> </symbol> <symbol overflow="visible" id="Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph2-3"> <path style="stroke:none;" d="M 4.90625 -3.65625 C 4.9375 -3.796875 4.9375 -3.859375 4.9375 -3.875 C 4.9375 -4.09375 4.75 -4.171875 4.625 -4.171875 C 4.40625 -4.171875 4.21875 -4 4.1875 -3.78125 C 4.109375 -3.9375 3.8125 -4.359375 3.21875 -4.359375 C 2.03125 -4.359375 0.75 -3.046875 0.75 -1.609375 C 0.75 -0.53125 1.453125 0 2.1875 0 C 2.640625 0 3.046875 -0.25 3.375 -0.53125 L 3.15625 0.359375 C 3.046875 0.765625 2.984375 1.0625 2.59375 1.390625 C 2.171875 1.734375 1.796875 1.734375 1.546875 1.734375 C 1.3125 1.734375 1.0625 1.734375 0.828125 1.6875 C 1.046875 1.5625 1.140625 1.359375 1.140625 1.1875 C 1.140625 0.953125 0.96875 0.828125 0.765625 0.828125 C 0.515625 0.828125 0.203125 1.015625 0.203125 1.421875 C 0.203125 1.984375 0.984375 2.015625 1.578125 2.015625 C 2.984375 2.015625 3.671875 1.265625 3.828125 0.65625 Z M 3.578125 -1.3125 C 3.5 -1.03125 3.28125 -0.828125 3.078125 -0.640625 C 2.984375 -0.578125 2.609375 -0.28125 2.203125 -0.28125 C 1.8125 -0.28125 1.515625 -0.609375 1.515625 -1.203125 C 1.515625 -1.609375 1.765625 -2.6875 2.03125 -3.1875 C 2.359375 -3.765625 2.8125 -4.078125 3.21875 -4.078125 C 3.875 -4.078125 4.0625 -3.359375 4.0625 -3.265625 L 4.03125 -3.125 Z M 3.578125 -1.3125 "></path> </symbol> <symbol overflow="visible" id="Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph2-4"> <path style="stroke:none;" d="M 4.703125 -4.078125 C 4.71875 -4.109375 4.734375 -4.171875 4.734375 -4.21875 C 4.734375 -4.28125 4.6875 -4.359375 4.59375 -4.359375 C 4.484375 -4.359375 4.078125 -3.96875 3.921875 -3.703125 C 3.8125 -3.921875 3.515625 -4.359375 2.890625 -4.359375 C 1.71875 -4.359375 0.421875 -2.984375 0.421875 -1.515625 C 0.421875 -0.5 1.09375 0.09375 1.84375 0.09375 C 2.34375 0.09375 2.75 -0.1875 3.046875 -0.4375 C 3.03125 -0.421875 2.734375 0.828125 2.6875 1 C 2.546875 1.578125 2.546875 1.578125 1.921875 1.59375 C 1.796875 1.59375 1.671875 1.59375 1.671875 1.78125 C 1.671875 1.84375 1.71875 1.921875 1.8125 1.921875 C 1.953125 1.921875 2.171875 1.90625 2.296875 1.890625 L 2.828125 1.890625 C 3.625 1.890625 3.796875 1.921875 3.875 1.921875 C 3.921875 1.921875 4.0625 1.921875 4.0625 1.734375 C 4.0625 1.59375 3.921875 1.59375 3.8125 1.59375 C 3.328125 1.59375 3.328125 1.53125 3.328125 1.4375 C 3.328125 1.4375 3.328125 1.390625 3.375 1.234375 Z M 3.25 -1.21875 C 3.203125 -1.078125 3.203125 -1.046875 3.03125 -0.859375 C 2.515625 -0.25 2.09375 -0.171875 1.875 -0.171875 C 1.421875 -0.171875 1.203125 -0.59375 1.203125 -1.109375 C 1.203125 -1.578125 1.46875 -2.625 1.6875 -3.0625 C 1.96875 -3.671875 2.453125 -4.078125 2.90625 -4.078125 C 3.578125 -4.078125 3.734375 -3.3125 3.734375 -3.25 C 3.734375 -3.203125 3.71875 -3.140625 3.703125 -3.078125 Z M 3.25 -1.21875 "></path> </symbol> <symbol overflow="visible" id="Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph2-5"> <path style="stroke:none;" d="M 1.90625 -1.359375 C 2.015625 -1.796875 2.125 -2.21875 2.21875 -2.65625 C 2.234375 -2.671875 2.296875 -2.953125 2.3125 -3 C 2.34375 -3.09375 2.59375 -3.5 2.84375 -3.75 C 3.171875 -4.03125 3.5 -4.078125 3.671875 -4.078125 C 3.78125 -4.078125 3.96875 -4.078125 4.109375 -3.953125 C 3.671875 -3.875 3.625 -3.5 3.625 -3.40625 C 3.625 -3.1875 3.78125 -3.046875 4 -3.046875 C 4.265625 -3.046875 4.5625 -3.265625 4.5625 -3.65625 C 4.5625 -4.015625 4.265625 -4.359375 3.703125 -4.359375 C 3.03125 -4.359375 2.578125 -3.921875 2.359375 -3.65625 C 2.171875 -4.359375 1.5 -4.359375 1.390625 -4.359375 C 1.03125 -4.359375 0.796875 -4.140625 0.640625 -3.828125 C 0.40625 -3.375 0.296875 -2.875 0.296875 -2.84375 C 0.296875 -2.765625 0.359375 -2.71875 0.4375 -2.71875 C 0.578125 -2.71875 0.578125 -2.765625 0.65625 -3.015625 C 0.765625 -3.5 0.953125 -4.078125 1.359375 -4.078125 C 1.625 -4.078125 1.6875 -3.84375 1.6875 -3.625 C 1.6875 -3.4375 1.625 -3.25 1.546875 -2.921875 C 1.53125 -2.84375 1.390625 -2.265625 1.34375 -2.125 L 0.984375 -0.640625 C 0.9375 -0.5 0.875 -0.25 0.875 -0.203125 C 0.875 0.015625 1.0625 0.09375 1.203125 0.09375 C 1.546875 0.09375 1.609375 -0.171875 1.6875 -0.515625 Z M 1.90625 -1.359375 "></path> </symbol> <symbol overflow="visible" id="Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph2-6"> <path style="stroke:none;" d="M 2.890625 -6.5625 C 2.890625 -6.59375 2.921875 -6.71875 2.921875 -6.71875 C 2.921875 -6.78125 2.890625 -6.859375 2.765625 -6.859375 C 2.734375 -6.859375 2.421875 -6.828125 2.203125 -6.8125 L 1.640625 -6.78125 C 1.421875 -6.75 1.328125 -6.75 1.328125 -6.5625 C 1.328125 -6.421875 1.46875 -6.421875 1.578125 -6.421875 C 2.0625 -6.421875 2.0625 -6.375 2.0625 -6.28125 C 2.0625 -6.25 2.0625 -6.234375 2 -6.046875 L 0.609375 -0.421875 C 0.5625 -0.28125 0.5625 -0.21875 0.5625 -0.203125 C 0.5625 -0.046875 0.703125 0.09375 0.890625 0.09375 C 1.046875 0.09375 1.1875 0 1.265625 -0.125 C 1.296875 -0.1875 1.375 -0.5 1.421875 -0.703125 L 1.65625 -1.578125 C 1.6875 -1.734375 1.78125 -2.109375 1.8125 -2.25 C 1.953125 -2.828125 1.953125 -2.84375 2.171875 -3.171875 C 2.515625 -3.65625 2.984375 -4.078125 3.640625 -4.078125 C 4 -4.078125 4.203125 -3.875 4.203125 -3.40625 C 4.203125 -2.875 3.78125 -1.734375 3.59375 -1.25 C 3.46875 -0.9375 3.46875 -0.875 3.46875 -0.734375 C 3.46875 -0.171875 3.9375 0.09375 4.359375 0.09375 C 5.328125 0.09375 5.734375 -1.28125 5.734375 -1.421875 C 5.734375 -1.515625 5.65625 -1.546875 5.59375 -1.546875 C 5.46875 -1.546875 5.453125 -1.46875 5.421875 -1.375 C 5.1875 -0.5625 4.765625 -0.171875 4.390625 -0.171875 C 4.234375 -0.171875 4.15625 -0.28125 4.15625 -0.5 C 4.15625 -0.734375 4.234375 -0.953125 4.328125 -1.203125 C 4.484375 -1.578125 4.921875 -2.703125 4.921875 -3.265625 C 4.921875 -4 4.40625 -4.359375 3.6875 -4.359375 C 3.140625 -4.359375 2.609375 -4.125 2.15625 -3.59375 Z M 2.890625 -6.5625 "></path> </symbol> <symbol overflow="visible" id="Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph2-7"> <path style="stroke:none;" d="M 2.953125 -6.171875 C 2.953125 -6.390625 2.796875 -6.546875 2.5625 -6.546875 C 2.296875 -6.546875 2.015625 -6.3125 2.015625 -6.015625 C 2.015625 -5.796875 2.171875 -5.640625 2.40625 -5.640625 C 2.65625 -5.640625 2.953125 -5.875 2.953125 -6.171875 Z M 1.5 -2.546875 L 0.96875 -1.171875 C 0.921875 -1.03125 0.875 -0.90625 0.875 -0.734375 C 0.875 -0.25 1.25 0.09375 1.765625 0.09375 C 2.734375 0.09375 3.140625 -1.28125 3.140625 -1.421875 C 3.140625 -1.515625 3.0625 -1.546875 2.984375 -1.546875 C 2.875 -1.546875 2.84375 -1.46875 2.8125 -1.375 C 2.59375 -0.578125 2.1875 -0.171875 1.796875 -0.171875 C 1.671875 -0.171875 1.546875 -0.234375 1.546875 -0.5 C 1.546875 -0.734375 1.625 -0.90625 1.75 -1.21875 C 1.84375 -1.484375 1.953125 -1.75 2.0625 -2.015625 L 2.359375 -2.8125 C 2.453125 -3.046875 2.578125 -3.359375 2.578125 -3.515625 C 2.578125 -4.015625 2.171875 -4.359375 1.671875 -4.359375 C 0.71875 -4.359375 0.296875 -2.984375 0.296875 -2.84375 C 0.296875 -2.765625 0.359375 -2.71875 0.4375 -2.71875 C 0.578125 -2.71875 0.578125 -2.78125 0.609375 -2.875 C 0.890625 -3.8125 1.34375 -4.078125 1.640625 -4.078125 C 1.78125 -4.078125 1.875 -4.03125 1.875 -3.765625 C 1.875 -3.65625 1.875 -3.515625 1.765625 -3.21875 Z M 1.5 -2.546875 "></path> </symbol> </g> </defs> <g id="Wi_lvTosyVEDnOMpO5w8TmuhSbs=-surface1"> <g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> <use xlink:href="#Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph0-1" x="8.453546" y="19.176568"></use> </g> <g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> <use xlink:href="#Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph0-2" x="91.332041" y="19.176568"></use> </g> <g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> <use xlink:href="#Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph0-3" x="173.118986" y="19.176568"></use> </g> <g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> <use xlink:href="#Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph0-1" x="6.719964" y="82.721709"></use> </g> <g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> <use xlink:href="#Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph1-1" x="17.605705" y="77.340858"></use> </g> <g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> <use xlink:href="#Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph0-2" x="89.59846" y="82.721709"></use> </g> <g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> <use xlink:href="#Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph1-1" x="99.39265" y="77.340858"></use> </g> <g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> <use xlink:href="#Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph0-3" x="171.385404" y="82.721709"></use> </g> <g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> <use xlink:href="#Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph1-1" x="183.165473" y="77.340858"></use> </g> <path style="fill:none;stroke-width:0.47818;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M -83.4219 21.194079 L -83.4219 -19.969751 " transform="matrix(0.992319,0,0,-0.992319,96.67568,45.882853)"></path> <path style="fill:none;stroke-width:0.47818;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M -2.487803 2.869388 C -2.03117 1.149144 -1.019494 0.334291 0.0000562409 -0.00030981 C -1.019494 -0.334911 -2.03117 -1.145827 -2.487803 -2.870008 " transform="matrix(0,0.992319,0.992319,0,13.894839,65.937444)"></path> <g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> <use xlink:href="#Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph2-1" x="17.385411" y="46.679685"></use> </g> <path style="fill:none;stroke-width:0.47818;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M -12.069163 30.649517 L -70.773972 30.649517 " transform="matrix(0.992319,0,0,-0.992319,96.67568,45.882853)"></path> <path style="fill:none;stroke-width:0.47818;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M -2.488422 2.869531 C -2.031789 1.149287 -1.020112 0.334434 -0.000562673 -0.000167185 C -1.020112 -0.334768 -2.031789 -1.145684 -2.488422 -2.869865 " transform="matrix(-0.992319,0,0,0.992319,26.206473,15.468916)"></path> <g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> <use xlink:href="#Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph2-2" x="52.267413" y="10.058147"></use> </g> <path style="fill:none;stroke-width:0.47818;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 11.167912 30.649517 L 69.872721 30.649517 " transform="matrix(0.992319,0,0,-0.992319,96.67568,45.882853)"></path> <path style="fill:none;stroke-width:0.47818;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M -2.488542 2.869865 C -2.03191 1.145684 -1.020233 0.334768 -0.000683541 0.000167185 C -1.020233 -0.334434 -2.03191 -1.149287 -2.488542 -2.869531 " transform="matrix(0.992319,0,0,-0.992319,166.250678,15.468916)"></path> <g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> <use xlink:href="#Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph2-3" x="134.445331" y="10.058147"></use> </g> <path style="fill:none;stroke-width:0.47818;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M -0.448657 21.194079 L -0.448657 -19.969751 " transform="matrix(0.992319,0,0,-0.992319,96.67568,45.882853)"></path> <path style="fill:none;stroke-width:0.47818;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M -2.487803 2.867464 C -2.03117 1.14722 -1.019494 0.336304 0.0000562409 0.00170281 C -1.019494 -0.332898 -2.03117 -1.147751 -2.487803 -2.867995 " transform="matrix(0,0.992319,0.992319,0,96.228779,65.937444)"></path> <g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> <use xlink:href="#Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph2-4" x="99.71813" y="46.679685"></use> </g> <path style="fill:none;stroke-width:0.47818;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 82.973345 21.194079 L 82.973345 -19.969751 " transform="matrix(0.992319,0,0,-0.992319,96.67568,45.882853)"></path> <path style="fill:none;stroke-width:0.47818;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M -2.487803 2.867716 C -2.03117 1.147472 -1.019494 0.336556 0.0000562409 0.00195478 C -1.019494 -0.336583 -2.03117 -1.147499 -2.487803 -2.867743 " transform="matrix(0,0.992319,0.992319,0,179.009779,65.937444)"></path> <g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> <use xlink:href="#Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph2-5" x="182.498386" y="47.64025"></use> </g> <path style="fill:none;stroke-width:0.47818;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M -13.816962 -33.38923 L -69.030109 -33.38923 " transform="matrix(0.992319,0,0,-0.992319,96.67568,45.882853)"></path> <path style="fill:none;stroke-width:0.47818;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M -2.485325 2.869818 C -2.032629 1.149574 -1.020952 0.334721 -0.00140226 0.000119893 C -1.020952 -0.334481 -2.032629 -1.149334 -2.485325 -2.869578 " transform="matrix(-0.992319,0,0,0.992319,27.940015,79.015506)"></path> <g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> <use xlink:href="#Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph2-6" x="52.309091" y="89.369255"></use> </g> <path style="fill:none;stroke-width:0.47818;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 12.915711 -33.38923 L 68.128858 -33.38923 " transform="matrix(0.992319,0,0,-0.992319,96.67568,45.882853)"></path> <path style="fill:none;stroke-width:0.47818;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M -2.485476 2.869578 C -2.03278 1.149334 -1.021103 0.334481 -0.00155313 -0.000119893 C -1.021103 -0.334721 -2.03278 -1.149574 -2.485476 -2.869818 " transform="matrix(0.992319,0,0,-0.992319,164.517166,79.015506)"></path> <g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> <use xlink:href="#Wi_lvTosyVEDnOMpO5w8TmuhSbs=-glyph2-7" x="135.334449" y="89.039805"></use> </g> </g> </svg> <p>Moreover, when <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 an arbitrary category, not necessarily having pullbacks, one can still obtain a <a class="existingWikiWord" href="/nlab/show/covirtual+double+category">covirtual double category</a>. More details can be found in Section 4 of <a href="#DawsonParePronk10">Dawson, Paré, Pronk</a> (where the term oplax double category is used).</p> <h2 id="properties">Properties</h2> <h3 id="the_1category_of_spans">The 1-category of spans</h3> <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 category with <a class="existingWikiWord" href="/nlab/show/pullback">pullback</a>s and let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Span</mi> <mn>1</mn></msub><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo><mo>:</mo><mo>=</mo><mo stretchy="false">(</mo><mi>Span</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo><msub><mo stretchy="false">)</mo> <mrow><mo>∼</mo><mn>1</mn></mrow></msub></mrow><annotation encoding="application/x-tex">Span_1(C) := (Span(C))_{\sim 1}</annotation></semantics></math> be the 1-category of objects 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> and isomorphism classes of spans between them as morphisms.</p> <p>Then</p> <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Span</mi> <mn>1</mn></msub><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Span_1(C)</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/dagger+category">dagger category</a>.</li> </ul> <p>Next assume that <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 <a class="existingWikiWord" href="/nlab/show/cartesian+monoidal+category">cartesian monoidal category</a>. Then clearly <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Span</mi> <mn>1</mn></msub><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Span_1(C)</annotation></semantics></math> naturally becomes a <a class="existingWikiWord" href="/nlab/show/monoidal+category">monoidal category</a> itself, but more: then</p> <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Span</mi> <mn>1</mn></msub><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Span_1(C)</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/dagger+compact+category">dagger compact category</a>.</li> </ul> <h3 id="UniversalPropertyOfTheBicategoryOfSpans">Universal property of the bicategory of spans</h3> <p>We discuss the <a class="existingWikiWord" href="/nlab/show/universal+property">universal property</a> that characterizes 2-categories of spans.</p> <p>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> be a <a class="existingWikiWord" href="/nlab/show/category">category</a> with <a class="existingWikiWord" href="/nlab/show/pullbacks">pullbacks</a>, write</p> <ol> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Span</mi> <mn>2</mn></msub><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo><mo>≔</mo><mo stretchy="false">(</mo><mi>Span</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo><msub><mo stretchy="false">)</mo> <mrow><mo>∼</mo><mn>2</mn></mrow></msub></mrow><annotation encoding="application/x-tex">Span_2(C) \coloneqq (Span(C))_{\sim2}</annotation></semantics></math> for the <a class="existingWikiWord" href="/nlab/show/weak+2-category">weak 2-category</a> of objects 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>, spans as morphisms, and maps between spans as 2-morphisms,</p> </li> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>η</mi> <mi>C</mi></msub><mo>:</mo><mi>C</mi><mo>→</mo><msub><mi>Span</mi> <mn>2</mn></msub><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\eta_C: C \rightarrow Span_2(C)</annotation></semantics></math> for the functor given by:</p> </li> </ol> <div style="text-align: center"> <svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" width="413.385" height="79.792" viewBox="0 0 413.385 79.792"> <defs> <g> <g id="uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-0-0"> </g> <g id="uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-0-1"> <path d="M 7.078125 -6.09375 C 6.609375 -6 6.421875 -5.640625 6.421875 -5.359375 C 6.421875 -5 6.703125 -4.890625 6.921875 -4.890625 C 7.359375 -4.890625 7.671875 -5.265625 7.671875 -5.671875 C 7.671875 -6.296875 6.953125 -6.59375 6.328125 -6.59375 C 5.421875 -6.59375 4.921875 -5.6875 4.78125 -5.40625 C 4.4375 -6.53125 3.515625 -6.59375 3.234375 -6.59375 C 1.71875 -6.59375 0.90625 -4.625 0.90625 -4.296875 C 0.90625 -4.25 0.96875 -4.171875 1.078125 -4.171875 C 1.1875 -4.171875 1.21875 -4.25 1.25 -4.3125 C 1.765625 -5.96875 2.765625 -6.28125 3.203125 -6.28125 C 3.875 -6.28125 4 -5.65625 4 -5.296875 C 4 -4.96875 3.90625 -4.625 3.734375 -3.90625 L 3.21875 -1.859375 C 3 -0.96875 2.5625 -0.15625 1.78125 -0.15625 C 1.703125 -0.15625 1.328125 -0.15625 1.015625 -0.34375 C 1.546875 -0.453125 1.671875 -0.890625 1.671875 -1.078125 C 1.671875 -1.375 1.453125 -1.546875 1.171875 -1.546875 C 0.8125 -1.546875 0.421875 -1.234375 0.421875 -0.765625 C 0.421875 -0.140625 1.125 0.15625 1.765625 0.15625 C 2.484375 0.15625 2.984375 -0.421875 3.296875 -1.03125 C 3.546875 -0.15625 4.28125 0.15625 4.84375 0.15625 C 6.359375 0.15625 7.171875 -1.8125 7.171875 -2.140625 C 7.171875 -2.203125 7.109375 -2.265625 7.015625 -2.265625 C 6.890625 -2.265625 6.875 -2.203125 6.828125 -2.078125 C 6.421875 -0.765625 5.5625 -0.15625 4.890625 -0.15625 C 4.359375 -0.15625 4.078125 -0.53125 4.078125 -1.15625 C 4.078125 -1.484375 4.140625 -1.71875 4.375 -2.703125 L 4.90625 -4.734375 C 5.125 -5.625 5.625 -6.28125 6.3125 -6.28125 C 6.34375 -6.28125 6.765625 -6.28125 7.078125 -6.09375 Z M 7.078125 -6.09375 "></path> </g> <g id="uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-0-2"> <path d="M 3.921875 1.671875 C 3.53125 2.234375 2.9375 2.75 2.203125 2.75 C 2.03125 2.75 1.3125 2.71875 1.09375 2.03125 C 1.140625 2.046875 1.203125 2.046875 1.234375 2.046875 C 1.6875 2.046875 1.984375 1.65625 1.984375 1.3125 C 1.984375 0.96875 1.703125 0.84375 1.484375 0.84375 C 1.234375 0.84375 0.71875 1.03125 0.71875 1.765625 C 0.71875 2.53125 1.359375 3.046875 2.203125 3.046875 C 3.703125 3.046875 5.21875 1.671875 5.625 0.015625 L 7.09375 -5.8125 C 7.109375 -5.890625 7.140625 -5.96875 7.140625 -6.0625 C 7.140625 -6.28125 6.953125 -6.4375 6.734375 -6.4375 C 6.609375 -6.4375 6.28125 -6.375 6.171875 -5.9375 L 5.0625 -1.53125 C 4.984375 -1.265625 4.984375 -1.234375 4.875 -1.078125 C 4.578125 -0.65625 4.078125 -0.15625 3.359375 -0.15625 C 2.53125 -0.15625 2.453125 -0.96875 2.453125 -1.375 C 2.453125 -2.21875 2.859375 -3.375 3.25 -4.453125 C 3.421875 -4.890625 3.515625 -5.09375 3.515625 -5.390625 C 3.515625 -6.015625 3.0625 -6.59375 2.328125 -6.59375 C 0.953125 -6.59375 0.40625 -4.421875 0.40625 -4.296875 C 0.40625 -4.25 0.46875 -4.171875 0.5625 -4.171875 C 0.703125 -4.171875 0.71875 -4.234375 0.78125 -4.4375 C 1.140625 -5.6875 1.703125 -6.28125 2.28125 -6.28125 C 2.421875 -6.28125 2.671875 -6.28125 2.671875 -5.796875 C 2.671875 -5.40625 2.515625 -4.96875 2.28125 -4.40625 C 1.546875 -2.453125 1.546875 -1.953125 1.546875 -1.59375 C 1.546875 -0.171875 2.5625 0.15625 3.3125 0.15625 C 3.75 0.15625 4.28125 0.015625 4.8125 -0.53125 L 4.828125 -0.515625 C 4.59375 0.359375 4.453125 0.9375 3.921875 1.671875 Z M 3.921875 1.671875 "></path> </g> <g id="uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-1-0"> </g> <g id="uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-1-1"> <path d="M 1.421875 -3.4375 C 1.515625 -3.4375 1.84375 -3.4375 1.84375 -3.734375 C 1.84375 -4.03125 1.515625 -4.03125 1.421875 -4.03125 L 1.421875 -5.984375 C 1.421875 -6.234375 1.421875 -6.515625 1.125 -6.515625 C 0.828125 -6.515625 0.828125 -6.234375 0.828125 -5.984375 L 0.828125 -1.484375 C 0.828125 -1.234375 0.828125 -0.953125 1.125 -0.953125 C 1.421875 -0.953125 1.421875 -1.234375 1.421875 -1.484375 Z M 1.421875 -3.4375 "></path> </g> <g id="uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-1-2"> <path d="M 12.453125 -3.4375 C 11.640625 -2.8125 11.234375 -2.203125 11.109375 -2 C 10.4375 -0.96875 10.328125 -0.03125 10.328125 -0.015625 C 10.328125 0.171875 10.5 0.171875 10.625 0.171875 C 10.875 0.171875 10.890625 0.140625 10.953125 -0.140625 C 11.296875 -1.59375 12.171875 -2.859375 13.859375 -3.546875 C 14.046875 -3.59375 14.09375 -3.625 14.09375 -3.734375 C 14.09375 -3.84375 14 -3.890625 13.96875 -3.90625 C 13.3125 -4.15625 11.5 -4.90625 10.9375 -7.40625 C 10.890625 -7.59375 10.875 -7.640625 10.625 -7.640625 C 10.5 -7.640625 10.328125 -7.640625 10.328125 -7.453125 C 10.328125 -7.421875 10.453125 -6.484375 11.078125 -5.484375 C 11.375 -5.03125 11.8125 -4.515625 12.453125 -4.03125 L 1.359375 -4.03125 C 1.09375 -4.03125 0.828125 -4.03125 0.828125 -3.734375 C 0.828125 -3.4375 1.09375 -3.4375 1.359375 -3.4375 Z M 12.453125 -3.4375 "></path> </g> <g id="uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-2-0"> </g> <g id="uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-2-1"> <path d="M 3.125 -6.34375 C 3.125 -6.625 3.109375 -6.625 2.84375 -6.625 C 2.4375 -6.234375 1.90625 -5.984375 0.953125 -5.984375 L 0.953125 -5.65625 C 1.21875 -5.65625 1.765625 -5.65625 2.34375 -5.9375 L 2.34375 -0.8125 C 2.34375 -0.453125 2.3125 -0.328125 1.359375 -0.328125 L 1.015625 -0.328125 L 1.015625 0 C 1.421875 -0.03125 2.28125 -0.03125 2.734375 -0.03125 C 3.1875 -0.03125 4.046875 -0.03125 4.453125 0 L 4.453125 -0.328125 L 4.109375 -0.328125 C 3.15625 -0.328125 3.125 -0.453125 3.125 -0.8125 Z M 3.125 -6.34375 "></path> </g> <g id="uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-3-0"> </g> <g id="uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-3-1"> <path d="M 4.203125 -2.9375 C 3.9375 -2.859375 3.890625 -2.640625 3.890625 -2.53125 C 3.890625 -2.296875 4.078125 -2.234375 4.1875 -2.234375 C 4.40625 -2.234375 4.609375 -2.421875 4.609375 -2.71875 C 4.609375 -3.109375 4.171875 -3.296875 3.796875 -3.296875 C 3.296875 -3.296875 3 -2.90625 2.921875 -2.765625 C 2.828125 -2.953125 2.546875 -3.296875 1.984375 -3.296875 C 1.125 -3.296875 0.609375 -2.40625 0.609375 -2.140625 C 0.609375 -2.109375 0.640625 -2.03125 0.75 -2.03125 C 0.84375 -2.03125 0.875 -2.078125 0.890625 -2.15625 C 1.078125 -2.75 1.59375 -3.046875 1.953125 -3.046875 C 2.328125 -3.046875 2.4375 -2.8125 2.4375 -2.5625 C 2.4375 -2.46875 2.4375 -2.40625 2.375 -2.171875 C 2.203125 -1.484375 2.03125 -0.796875 2 -0.703125 C 1.890625 -0.421875 1.625 -0.171875 1.3125 -0.171875 C 1.265625 -0.171875 1.046875 -0.171875 0.875 -0.28125 C 1.171875 -0.375 1.203125 -0.625 1.203125 -0.6875 C 1.203125 -0.875 1.046875 -0.984375 0.90625 -0.984375 C 0.6875 -0.984375 0.46875 -0.8125 0.46875 -0.515625 C 0.46875 -0.078125 0.9375 0.078125 1.296875 0.078125 C 1.71875 0.078125 2.03125 -0.21875 2.171875 -0.453125 C 2.3125 -0.140625 2.671875 0.078125 3.09375 0.078125 C 3.984375 0.078125 4.46875 -0.828125 4.46875 -1.078125 C 4.46875 -1.09375 4.46875 -1.1875 4.328125 -1.1875 C 4.234375 -1.1875 4.21875 -1.125 4.1875 -1.0625 C 3.96875 -0.40625 3.4375 -0.171875 3.125 -0.171875 C 2.84375 -0.171875 2.640625 -0.34375 2.640625 -0.65625 C 2.640625 -0.796875 2.6875 -0.953125 2.75 -1.21875 L 2.984375 -2.1875 C 3.0625 -2.484375 3.09375 -2.609375 3.25 -2.796875 C 3.359375 -2.90625 3.546875 -3.046875 3.78125 -3.046875 C 3.8125 -3.046875 4.046875 -3.046875 4.203125 -2.9375 Z M 4.203125 -2.9375 "></path> </g> <g id="uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-4-0"> </g> <g id="uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-4-1"> <path d="M 3.8125 -3.96875 L 4.75 -3.96875 C 4.9375 -3.96875 5.0625 -3.96875 5.0625 -4.15625 C 5.0625 -4.296875 4.9375 -4.296875 4.765625 -4.296875 L 3.875 -4.296875 C 4.03125 -5.1875 4.140625 -5.765625 4.234375 -6.203125 C 4.28125 -6.375 4.3125 -6.484375 4.453125 -6.609375 C 4.578125 -6.71875 4.671875 -6.734375 4.78125 -6.734375 C 4.921875 -6.734375 5.078125 -6.703125 5.21875 -6.625 C 5.15625 -6.609375 5.109375 -6.578125 5.046875 -6.546875 C 4.890625 -6.453125 4.765625 -6.28125 4.765625 -6.078125 C 4.765625 -5.859375 4.9375 -5.71875 5.15625 -5.71875 C 5.453125 -5.71875 5.71875 -5.96875 5.71875 -6.3125 C 5.71875 -6.78125 5.25 -7.015625 4.765625 -7.015625 C 4.421875 -7.015625 3.796875 -6.859375 3.484375 -5.9375 C 3.390625 -5.71875 3.390625 -5.6875 3.125 -4.296875 L 2.375 -4.296875 C 2.171875 -4.296875 2.046875 -4.296875 2.046875 -4.109375 C 2.046875 -3.96875 2.1875 -3.96875 2.359375 -3.96875 L 3.0625 -3.96875 L 2.34375 -0.09375 C 2.15625 0.90625 2 1.75 1.46875 1.75 C 1.453125 1.75 1.234375 1.75 1.046875 1.640625 C 1.5 1.53125 1.5 1.109375 1.5 1.09375 C 1.5 0.875 1.328125 0.734375 1.109375 0.734375 C 0.84375 0.734375 0.546875 0.953125 0.546875 1.328125 C 0.546875 1.75 0.984375 2.03125 1.46875 2.03125 C 2.078125 2.03125 2.5 1.390625 2.625 1.140625 C 2.984375 0.484375 3.21875 -0.75 3.234375 -0.859375 Z M 3.8125 -3.96875 "></path> </g> </g> </defs> <g fill="rgb(0%, 0%, 0%)" fill-opacity="1"> <use xlink:href="#uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-0-1" x="321.908" y="11.903"></use> </g> <g fill="rgb(0%, 0%, 0%)" fill-opacity="1"> <use xlink:href="#uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-0-1" x="6.434" y="71.417"></use> </g> <g fill="rgb(0%, 0%, 0%)" fill-opacity="1"> <use xlink:href="#uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-0-2" x="83.806" y="71.417"></use> </g> <g fill="rgb(0%, 0%, 0%)" fill-opacity="1"> <use xlink:href="#uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-1-1" x="160.534" y="71.417"></use> <use xlink:href="#uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-1-2" x="160.534" y="71.417"></use> </g> <g fill="rgb(0%, 0%, 0%)" fill-opacity="1"> <use xlink:href="#uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-0-1" x="244.535" y="71.417"></use> </g> <g fill="rgb(0%, 0%, 0%)" fill-opacity="1"> <use xlink:href="#uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-0-2" x="399.28" y="71.417"></use> </g> <path fill="none" stroke-width="0.47818" stroke-linecap="butt" stroke-linejoin="miter" stroke="rgb(0%, 0%, 0%)" stroke-opacity="1" stroke-miterlimit="10" d="M 108.534562 23.392094 L 53.222062 -19.158687 " transform="matrix(1, 0, 0, -1, 206.692, 39.896)"></path> <path fill="none" stroke-width="0.47818" stroke-linecap="round" stroke-linejoin="round" stroke="rgb(0%, 0%, 0%)" stroke-opacity="1" stroke-miterlimit="10" d="M -2.486991 2.871304 C -2.0338 1.147575 -1.019421 0.33272 0.00164625 0.000657696 C -1.021352 -0.33609 -2.029839 -1.147294 -2.487688 -2.870036 " transform="matrix(-0.79256, 0.60971, 0.60971, 0.79256, 259.72356, 59.2016)"></path> <g fill="rgb(0%, 0%, 0%)" fill-opacity="1"> <use xlink:href="#uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-2-1" x="281.814" y="33.164"></use> </g> <g fill="rgb(0%, 0%, 0%)" fill-opacity="1"> <use xlink:href="#uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-3-1" x="287.1065" y="34.409"></use> </g> <path fill="none" stroke-width="0.47818" stroke-linecap="butt" stroke-linejoin="miter" stroke="rgb(0%, 0%, 0%)" stroke-opacity="1" stroke-miterlimit="10" d="M 130.21425 23.356938 L 185.52675 -19.377437 " transform="matrix(1, 0, 0, -1, 206.692, 39.896)"></path> <path fill="none" stroke-width="0.47818" stroke-linecap="round" stroke-linejoin="round" stroke="rgb(0%, 0%, 0%)" stroke-opacity="1" stroke-miterlimit="10" d="M -2.486181 2.867808 C -2.032661 1.149789 -1.017725 0.334467 0.000490904 0.000519846 C -1.019901 -0.333641 -2.031912 -1.145103 -2.487048 -2.869071 " transform="matrix(0.7913, 0.61133, 0.61133, -0.7913, 392.40945, 59.41808)"></path> <g fill="rgb(0%, 0%, 0%)" fill-opacity="1"> <use xlink:href="#uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-4-1" x="368.267" y="32.598"></use> </g> <path fill="none" stroke-width="0.47818" stroke-linecap="butt" stroke-linejoin="miter" stroke="rgb(0%, 0%, 0%)" stroke-opacity="1" stroke-miterlimit="10" d="M -185.262313 -27.783687 L -130.047469 -27.783687 " transform="matrix(1, 0, 0, -1, 206.692, 39.896)"></path> <path fill="none" stroke-width="0.47818" stroke-linecap="round" stroke-linejoin="round" stroke="rgb(0%, 0%, 0%)" stroke-opacity="1" stroke-miterlimit="10" d="M -2.487399 2.86907 C -2.030368 1.146414 -1.018649 0.333914 0.0008825 0.0018825 C -1.018649 -0.334055 -2.030368 -1.146555 -2.487399 -2.869211 " transform="matrix(1, 0, 0, -1, 76.88193, 67.68157)"></path> <g fill="rgb(0%, 0%, 0%)" fill-opacity="1"> <use xlink:href="#uIOkUGlRREaZuF59t_ZsGLnTT2A=-glyph-4-1" x="46.186" y="62.228"></use> </g> </svg> </div> <p>Now let</p> <ol> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>K</mi></mrow><annotation encoding="application/x-tex">K</annotation></semantics></math> be any <a class="existingWikiWord" href="/nlab/show/bicategory">bicategory</a></p> </li> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo>,</mo><mi>G</mi><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace><mi>C</mi><mo>→</mo><mi>K</mi></mrow><annotation encoding="application/x-tex">F, G \,\colon\, C \rightarrow K</annotation></semantics></math> be <a class="existingWikiWord" href="/nlab/show/functors">functors</a> such that every 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> is sent to a map in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>K</mi></mrow><annotation encoding="application/x-tex">K</annotation></semantics></math> possessing a <a class="existingWikiWord" href="/nlab/show/right+adjoint">right adjoint</a> and satisfying the <a class="existingWikiWord" href="/nlab/show/Beck-Chevalley+Condition">Beck-Chevalley Condition</a> for any <a class="existingWikiWord" href="/nlab/show/commutative+square">commutative square</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>K</mi></mrow><annotation encoding="application/x-tex">K</annotation></semantics></math>,</p> </li> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace><mi>F</mi><mo>→</mo><mi>G</mi></mrow><annotation encoding="application/x-tex">\alpha \,\colon\, F \rightarrow G</annotation></semantics></math> be a <a class="existingWikiWord" href="/nlab/show/natural+transformation">natural transformation</a>.</p> </li> </ol> <p>Then:</p> <p> <div class='num_prop'> <h6>Proposition</h6> <p><strong>(universal property of the bicategory of spans)</strong> <br /> The following holds:</p> <ol> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>η</mi> <mi>C</mi></msub></mrow><annotation encoding="application/x-tex">\eta_C</annotation></semantics></math> is <a class="existingWikiWord" href="/nlab/show/universal">universal</a> among such functors <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>, i.e. <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> as above factors as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo>=</mo><mover><mi>F</mi><mo stretchy="false">^</mo></mover><mo>∘</mo><msub><mi>η</mi> <mi>C</mi></msub></mrow><annotation encoding="application/x-tex">F = \hat{F} \circ \eta_C</annotation></semantics></math> for a functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mover><mi>F</mi><mo stretchy="false">^</mo></mover><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace><msub><mi>Span</mi> <mn>2</mn></msub><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo><mo>→</mo><mi>K</mi></mrow><annotation encoding="application/x-tex">\hat{F} \,\colon\, Span_2(C) \rightarrow K</annotation></semantics></math> which is unique up to isomorphism.</p> </li> <li> <p>There exists a unique <a class="existingWikiWord" href="/nlab/show/lax+natural+transformation">lax natural transformation</a>: <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mover><mi>α</mi><mo stretchy="false">^</mo></mover><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace><mover><mi>F</mi><mo stretchy="false">^</mo></mover><mo>→</mo><mover><mi>G</mi><mo stretchy="false">^</mo></mover></mrow><annotation encoding="application/x-tex">\hat{\alpha} \,\colon\, \hat{F} \rightarrow \hat{G}</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mover><mi>α</mi><mo stretchy="false">^</mo></mover><msub><mi>η</mi> <mi>C</mi></msub><mo>=</mo><mi>α</mi></mrow><annotation encoding="application/x-tex">\hat{\alpha} \eta_C = \alpha</annotation></semantics></math>.</p> </li> <li> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>,</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x, y</annotation></semantics></math> be objects 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> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>x</mi><mo>→</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">f: x \rightarrow y</annotation></semantics></math> be a morphism 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>. If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msub><mi>α</mi> <mi>x</mi></msub><mo>,</mo><msub><mi>α</mi> <mi>y</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(\alpha_x, \alpha_y)</annotation></semantics></math> induce a pseudo-map of adjoints <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>⊣</mo><mo stretchy="false">(</mo><mi>Ff</mi><msup><mo stretchy="false">)</mo> <mo>*</mo></msup><mo>→</mo><mi>G</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>⊣</mo><mo stretchy="false">(</mo><mi>Gf</mi><msup><mo stretchy="false">)</mo> <mo>*</mo></msup></mrow><annotation encoding="application/x-tex">F(f) \dashv (Ff)^* \rightarrow G(f) \dashv (Gf)^*</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mover><mi>α</mi><mo stretchy="false">^</mo></mover></mrow><annotation encoding="application/x-tex">\hat{\alpha}</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/pseudonatural+transformation">pseudonatural transformation</a></p> </li> </ol> <p>Furthermore, if we denote <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Pbk</mi></mrow><annotation encoding="application/x-tex">Pbk</annotation></semantics></math> as the <a class="existingWikiWord" href="/nlab/show/2-category">2-category</a> of categories with pullbacks, <a class="existingWikiWord" href="/nlab/show/pullback">pullback</a>-preserving <a class="existingWikiWord" href="/nlab/show/functor">functor</a>s, and <a class="existingWikiWord" href="/nlab/show/equifibered+natural+transformation">equifibered natural transformation</a>s and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>BiCat</mi></mrow><annotation encoding="application/x-tex">BiCat</annotation></semantics></math> as the <a class="existingWikiWord" href="/nlab/show/tricategory">tricategory</a> of <a class="existingWikiWord" href="/nlab/show/bicategories">bicategories</a>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Span</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo><mo>:</mo><mi>Pbk</mi><mo>→</mo><mi>BiCat</mi></mrow><annotation encoding="application/x-tex">Span(-): Pbk \rightarrow BiCat</annotation></semantics></math> is well-defined as a functor.</p> </div> This is due to <a href="#Hermida99">Hermida 1999</a>.</p> <h3 id="LimitsAndColimits">Limits and colimits</h3> <p>Since a category of spans/correspondences <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Corr</mi><mo stretchy="false">(</mo><mi>𝒞</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Corr(\mathcal{C})</annotation></semantics></math> is evidently <a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalent</a> to its <a class="existingWikiWord" href="/nlab/show/opposite+category">opposite category</a>, it follows that to the extent that <a class="existingWikiWord" href="/nlab/show/limits">limits</a> exists they are also <a class="existingWikiWord" href="/nlab/show/colimits">colimits</a> and vice versa.</p> <p>If the underlying category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒞</mi></mrow><annotation encoding="application/x-tex">\mathcal{C}</annotation></semantics></math> is an <a class="existingWikiWord" href="/nlab/show/extensive+category">extensive category</a>, then the <a class="existingWikiWord" href="/nlab/show/coproduct">coproduct</a>/<a class="existingWikiWord" href="/nlab/show/product">product</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Corr</mi><mo stretchy="false">(</mo><mi>𝒞</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Corr(\mathcal{C})</annotation></semantics></math> is given by the <a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒞</mi></mrow><annotation encoding="application/x-tex">\mathcal{C}</annotation></semantics></math>. (See also <a href="http://mathoverflow.net/questions/32526/what-is-the-product-in-the-2-category-of-spans">this</a> MO discussion).</p> <p>More generally, every <a class="existingWikiWord" href="/nlab/show/van+Kampen+colimit">van Kampen colimit</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒞</mi></mrow><annotation encoding="application/x-tex">\mathcal{C}</annotation></semantics></math> is a (co)limit in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Corr</mi><mo stretchy="false">(</mo><mi>𝒞</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Corr(\mathcal{C})</annotation></semantics></math> — and conversely, this property characterizes van Kampen colimits. (<a href="SobocinskiHeindel11">Sobocinski-Heindel 11</a>).</p> <h3 id="RelationToRelations">Relation to relations</h3> <p>Correspondences may be seen as generalizations of <a class="existingWikiWord" href="/nlab/show/relations">relations</a>. A relation is a <a class="existingWikiWord" href="/nlab/show/correspondence">correspondence</a> which is <a class="existingWikiWord" href="/nlab/show/%28-1%29-truncated">(-1)-truncated</a> as a <a class="existingWikiWord" href="/nlab/show/morphism">morphism</a> into the <a class="existingWikiWord" href="/nlab/show/cartesian+product">cartesian product</a>. See at <em><a class="existingWikiWord" href="/nlab/show/relation">relation</a></em> and at <em><a class="existingWikiWord" href="/nlab/show/Rel">Rel</a></em> for more on this.</p> <h2 id="examples">Examples</h2> <ul> <li> <p>Spans in <a class="existingWikiWord" href="/nlab/show/FinSet">FinSet</a> behave like the <a class="existingWikiWord" href="/nlab/show/categorification">categorification</a> of <a class="existingWikiWord" href="/nlab/show/matrices">matrices</a> with entries in the <a class="existingWikiWord" href="/nlab/show/natural+number">natural number</a>s: for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>X</mi> <mn>1</mn></msub><mo>←</mo><mi>N</mi><mo>→</mo><msub><mi>X</mi> <mn>2</mn></msub></mrow><annotation encoding="application/x-tex">X_1 \leftarrow N \to X_2</annotation></semantics></math> a span of finite sets, the <a class="existingWikiWord" href="/nlab/show/cardinality">cardinality</a> of the <a class="existingWikiWord" href="/nlab/show/fiber">fiber</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>X</mi> <mrow><msub><mi>x</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>x</mi> <mn>2</mn></msub></mrow></msub></mrow><annotation encoding="application/x-tex">X_{x_1, x_2}</annotation></semantics></math> over any two elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>x</mi> <mn>1</mn></msub><mo>∈</mo><msub><mi>X</mi> <mn>1</mn></msub></mrow><annotation encoding="application/x-tex">x_1 \in X_1</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>x</mi> <mn>2</mn></msub><mo>∈</mo><msub><mi>X</mi> <mn>2</mn></msub></mrow><annotation encoding="application/x-tex">x_2 \in X_2</annotation></semantics></math> plays the role of the corresponding matrix entry. Under this identification composition of spans indeed corresponds to matrix multiplication. This implies that the category of spans of finite sets is equivalent to the <a class="existingWikiWord" href="/nlab/show/Lawvere+theory">Lawvere theory</a> of commutative monoids, that is, to the <a class="existingWikiWord" href="/nlab/show/PROP">PROP</a> for the free bicommutative <a class="existingWikiWord" href="/nlab/show/bialgebra">bialgebra</a>. Spans over finite sets is a <a class="existingWikiWord" href="/nlab/show/rig+category">rig category</a> with respect to the tensor products induced by the coproduct and product in FinSet. The coproduct in FinSet remains the coproduct, but the product becomes the bilinear <a class="existingWikiWord" href="/nlab/show/tensor+product+of+modules">tensor product of modules</a>.</p> </li> <li> <p>The <a class="existingWikiWord" href="/nlab/show/Burnside+category">Burnside category</a> is essentially the category of correspondences in <a class="existingWikiWord" href="/nlab/show/G-sets">G-sets</a> for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi></mrow><annotation encoding="application/x-tex">G</annotation></semantics></math> a <a class="existingWikiWord" href="/nlab/show/finite+group">finite group</a>.</p> </li> <li> <p>A <a class="existingWikiWord" href="/nlab/show/cobordism">cobordism</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Σ</mi> <mi>in</mi></msub></mrow><annotation encoding="application/x-tex">\Sigma_{in}</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Σ</mi> <mi>out</mi></msub></mrow><annotation encoding="application/x-tex">\Sigma_{out}</annotation></semantics></math> is an example of a cospan <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Σ</mi> <mi>in</mi></msub><mo>→</mo><mi>Σ</mi><mo>←</mo><msub><mi>Σ</mi> <mi>out</mi></msub></mrow><annotation encoding="application/x-tex">\Sigma_{in} \to \Sigma \leftarrow \Sigma_{out}</annotation></semantics></math> in the category of <a class="existingWikiWord" href="/nlab/show/smooth+manifold">smooth manifold</a>s. However, composition of cobordisms is not quite the pushout-composition of these cospans: to make the composition be a <a class="existingWikiWord" href="/nlab/show/smooth+manifold">smooth manifold</a> again some extra technical aspects must be added (“<a class="existingWikiWord" href="/nlab/show/collars">collars</a>”).</p> </li> <li> <p>In <a class="existingWikiWord" href="/nlab/show/prequantum+field+theory">prequantum field theory</a> (see there for details), spans of <a class="existingWikiWord" href="/nlab/show/stacks">stacks</a> model <a class="existingWikiWord" href="/nlab/show/trajectories">trajectories</a> of <a class="existingWikiWord" href="/nlab/show/field+%28physics%29">fields</a>.</p> </li> <li> <p>The <a class="existingWikiWord" href="/nlab/show/category+of+Chow+motives">category of Chow motives</a> has as <a class="existingWikiWord" href="/nlab/show/morphisms">morphisms</a> <a class="existingWikiWord" href="/nlab/show/equivalence+classes">equivalence classes</a> of <a class="existingWikiWord" href="/nlab/show/linear+combinations">linear combinations</a> of spans of <a class="existingWikiWord" href="/nlab/show/smooth+variety">smooth</a> <a class="existingWikiWord" href="/nlab/show/projective+varieties">projective varieties</a>.</p> </li> <li> <p>The <a class="existingWikiWord" href="/nlab/show/Weinstein+symplectic+category">Weinstein symplectic category</a> has as morphisms <a class="existingWikiWord" href="/nlab/show/Lagrangian+correspondences">Lagrangian correspondences</a> between <a class="existingWikiWord" href="/nlab/show/symplectic+manifolds">symplectic manifolds</a>.</p> <p>More generally <a class="existingWikiWord" href="/nlab/show/symplectic+dual+pairs">symplectic dual pairs</a> are correspondences between <a class="existingWikiWord" href="/nlab/show/Poisson+manifolds">Poisson manifolds</a>.</p> </li> <li> <p>Cospans of homomorphisms of <a class="existingWikiWord" href="/nlab/show/C%2A-algebras">C*-algebras</a> represent morphisms in <a class="existingWikiWord" href="/nlab/show/KK-theory">KK-theory</a> (by Cuntz’ result).</p> </li> <li> <p>Correspondences of <a class="existingWikiWord" href="/nlab/show/flag+manifolds">flag manifolds</a> play a role as <a class="existingWikiWord" href="/nlab/show/twistor+correspondences">twistor correspondences</a>, see at <em><a href="Schubert+calculus#Correspondences">Schubert calculus – Correspondences</a></em> and at <em><a class="existingWikiWord" href="/nlab/show/horocycle+correspondence">horocycle correspondence</a></em></p> </li> <li> <p>The <a class="existingWikiWord" href="/nlab/show/Fourier-Mukai+transform">Fourier-Mukai transform</a> is a pull-push operation through correspondences equipped with objects in a cocycle given by an object in a <a class="existingWikiWord" href="/nlab/show/derived+category+of+quasi-coherent+sheaves">derived category of quasi-coherent sheaves</a>.</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Hecke+correspondence">Hecke correspondence</a></p> </li> <li> <p>A <a class="existingWikiWord" href="/nlab/show/hypergraph">hypergraph</a> is a span from a set of vertices to a set of (hyper)edges.</p> </li> </ul> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2Cn%29-category+of+spans">(∞,n)-category of spans</a>.</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/sink">sink</a>, <a class="existingWikiWord" href="/nlab/show/cosink">cosink</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/product">product</a>, <a class="existingWikiWord" href="/nlab/show/coproduct">coproduct</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/multispan">multispan</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/correspondence+type">correspondence type</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/reflexive+graph">reflexive graph</a></p> </li> </ul> <p>A category of correspondences is a refinement of a category <a class="existingWikiWord" href="/nlab/show/Rel">Rel</a> of relations. See there for more.</p> <h2 id="references">References</h2> <p>The terminology “span” appears on page 533 of:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Nobuo+Yoneda">Nobuo Yoneda</a>, <em>On ext and exact sequences</em> (PhD thesis), Journal of the Faculty of Science, Section I. <strong>8</strong> University of Tokyo (1960) 507–576 [<a href="http://alpha.math.uga.edu/~lorenz/YonedaExtExactSequences.pdf">pdf</a>, <a href="https://ci.nii.ac.jp/naid/500000325773">CiNii:naid/500000325773</a>]</li> </ul> <p>The <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Span</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Span(C)</annotation></semantics></math> construction was introduced by Jean Bénabou (as an example of a bicategory) in</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Jean+B%C3%A9nabou">Jean Bénabou</a>, Introduction to Bicategories, <em>Lecture Notes in Mathematics 47</em>, Springer (1967), pp.1-77. (<a href="http://dx.doi.org/10.1007/BFb0074299">doi</a>)</li> </ul> <p>Bénabou cites an article by Yoneda (1954) for introducing the concept of span (in the category of categories).</p> <p>An exposition discussing the role of spans in <a class="existingWikiWord" href="/nlab/show/quantum+theory">quantum theory</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/John+Baez">John Baez</a>, <em>Spans in quantum Theory</em> (<a href="http://math.ucr.edu/home/baez/span/">web</a>, <a href="http://math.ucr.edu/home/baez/span/span.pdf">pdf</a>, <a href="http://golem.ph.utexas.edu/category/2007/10/spans_in_quantum_theory.html">blog</a>)</li> </ul> <p>The relationship between spans and <a class="existingWikiWord" href="/nlab/show/bimodules">bimodules</a> is briefly discussed in</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/John+Baez">John Baez</a>, <em>Bimodules versus spans</em> (<a href="http://golem.ph.utexas.edu/category/2008/08/bimodules_versus_spans.html">blog</a>)</li> </ul> <p>The relation to <a class="existingWikiWord" href="/nlab/show/van+Kampen+colimits">van Kampen colimits</a> is discussed in</p> <ul> <li id="SobocinskiHeindel11"><a class="existingWikiWord" href="/nlab/show/Pawel+Sobocinski">Pawel Sobocinski</a>, Tobias Heindel, <em>Being Van Kampen is a universal property</em>, (<a href="http://arxiv.org/abs/1101.4594">arXiv:1101.4594</a>)</li> </ul> <p>The <a class="existingWikiWord" href="/nlab/show/universal+property">universal property</a> of categories of spans is due to</p> <ul> <li id="Hermida99"><a class="existingWikiWord" href="/nlab/show/Claudio+Hermida">Claudio Hermida</a>, <em>Representable Multicategories</em>, Advances in Mathematics, <strong>151</strong> (2000), No. 2, 164-225, (<a href="https://doi.org/10.1006/aima.1999.1877">doi:10.1006/aima.1999.1877</a>)</li> </ul> <p>and further discussed in:</p> <ul> <li id="DawsonParePronk04"> <p>R. Dawson, <a class="existingWikiWord" href="/nlab/show/Robert+Par%C3%A9">Robert Paré</a>, <a class="existingWikiWord" href="/nlab/show/Dorette+Pronk">Dorette Pronk</a>, <em>Universal properties of Span</em>, Theory and Appl. of Categories <strong>13</strong>, 2004, No. 4, 61-85, <a href="http://www.tac.mta.ca/tac/volumes/13/4/13-04abs.html">TAC</a>, <a href="http://www.ams.org/mathscinet-getitem?mr=2116323">MR2005m:18002</a></p> </li> <li id="DawsonParePronk10"> <p>R. Dawson, <a class="existingWikiWord" href="/nlab/show/Robert+Par%C3%A9">Robert Paré</a>, <a class="existingWikiWord" href="/nlab/show/Dorette+Pronk">Dorette Pronk</a>, <em>The span construction</em>, Theory Appl. Categ. <strong>24</strong> (2010), No. 13, 302–377, <a href="http://www.tac.mta.ca/tac/volumes/24/13/24-13abs.html">TAC</a> <a href="http://www.ams.org/mathscinet-getitem?mr=2720187">MR2720187</a></p> </li> <li> <p><span class="newWikiWord">Charles Walker<a href="/nlab/new/Charles+Walker">?</a></span>, <em>Universal properties of bicategories of polynomials</em>, Journal of Pure and Applied Algebra 223.9 (2019): 3722-3777.</p> </li> <li> <p><span class="newWikiWord">Charles Walker<a href="/nlab/new/Charles+Walker">?</a></span>, <em>Bicategories of spans as generic bicategories</em>, <a href="https://arxiv.org/abs/2002.10334">arXiv:2002.10334</a> (2020).</p> </li> </ul> <p>See also Theorem 5.2.1 and 5.3.7 of:</p> <ul> <li>Paul Balmer, and Ivo Dell’Ambrogio. <em>Mackey 2-functors and Mackey 2-motives</em>. <a href="https://arxiv.org/abs/1808.04902">arXiv:1808.04902</a> (2018).</li> </ul> <p>The structure of a <a class="existingWikiWord" href="/nlab/show/k-tuply+monoidal+%28n%2Cr%29-category">monoidal</a> <a class="existingWikiWord" href="/nlab/show/tricategory">tricategory</a> on spans in <a class="existingWikiWord" href="/nlab/show/2-categories">2-categories</a> is discussed in</p> <ul> <li id="Hoffnung"><a class="existingWikiWord" href="/nlab/show/Alex+Hoffnung">Alex Hoffnung</a>, <em>Spans in 2-Categories: A monoidal tricategory</em> (<a href="http://arxiv.org/abs/1112.0560">arXiv:1112.0560</a>)</li> </ul> <p>Generally, an <a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2Cn%29-category+of+spans">(∞,n)-category of spans</a> is indicated in section 3.2 of</p> <ul> <li id="Lurie"><a class="existingWikiWord" href="/nlab/show/Jacob+Lurie">Jacob Lurie</a>, <em><a class="existingWikiWord" href="/nlab/show/On+the+Classification+of+Topological+Field+Theories">On the Classification of Topological Field Theories</a></em></li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on December 4, 2024 at 15:51:33. See the <a href="/nlab/history/span" 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/span" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/13612/#Item_9">Discuss</a><span class="backintime"><a href="/nlab/revision/span/69" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/span" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/span" accesskey="S" class="navlink" id="history" rel="nofollow">History (69 revisions)</a> <a href="/nlab/show/span/cite" style="color: black">Cite</a> <a href="/nlab/print/span" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/span" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>