cartesian bicategory


2-Category theory

Monoidal categories



A cartesian bicategory is a bicategory with properties that make it behave like a bicategory of generalized relations.

Examples of cartesian bicategories include

  • the bicategory Rel of sets and relations,
  • more generally, the bicategory of relations of a regular category,
  • the bicategory Span of sets and spans,
  • more generally, the bicategory of spans in a finitely complete category,
  • the bicategory Prof of (small) categories and profunctors,
  • more generally, the bicategory of internal categories and modules (profunctors) in a finitely complete category CC,
  • as an alternative generalization, the bicategory of enriched categories and modules over a cartesian monoidal category VV.
  • ??(This is a guess) the bicategory of bialgebroids and modules in a general symmetric monoidal category VV.

Non-examples include

  • the locally-discrete bicategory Set of sets and functions,
  • the bicategory Prof of categories and profunctors,
  • the bicategory of profunctors and enriched in a noncartesian monoidal category VV.

Consider for example the bicategory Rel. This bicategory admits a symmetric monoidal structure given by the cartesian product. Because the cartesian product is not the categorical product, this symmetric monoidal structure is not cartesian monoidal. However, the cartesian product restricts to the locally-discrete sub-bicategory Set of sets and functions, on which it is the categorical product. Note that a relation is the graph of a function if and only if it possesses a right adjoint (which is given by the opposite relation). In a general bicategory, a 1-cell is called map-like if it possesses a right adjoint, and these are the 1-cells playing the role that functions play in RelRel.

Generalizing this situation, a cartesian bicategory BB is a symmetric monoidal bicategory for which the monoidal product restricts to the categorical product on the sub-bicategory of map-like 1-cells, subject to natural compatibility conditions. Remarkably, the structure of such a tensor is property-like (is essentially unique when it exists). Thus the definition can be formulated directly in terms of the bicategory BB without mentioning a symmetric monoidal structure at all. Not only is this technically convenient (as the precise definition of a symmetric monoidal bicategory is quite technical), but it is moreover a very natural perspective to take.

Like allegories, cartesian bicategories provide a convenient abstract setting in which to study the calculus of relations, but unlike allegories they embrace higher examples like SpanSpan and ModMod. The original idea, as explained by Carboni and Walters in their paper, clearly had these various examples in mind but was initially confined to the locally posetal case; in part this was due to the lack at the time (circa 1987) of a complete definition of symmetric monoidal bicategories. In more recent years a full bicategorical treatment has emerged, due principally to Carboni, Kelly, Verity, and Wood. The alternative treatment we give below has not yet appeared in the literature as far as this author (Todd Trimble) is aware.

Technical preliminaries

Note: All compositions will be written in the traditional order, in which application proceeds from right to left.

We work with familiar notions of the theory of bicategories (which, for reasons of consonance with 2-terminology, we also call 2-categories) but in some cases under new names. We calculate with pasting diagrams in 2-categories as if they were strict 2-categories.

Our notion of morphism between 2-categories has gone under various names: “homomorphism” in the sense of Bénabou, also known as “pseudofunctor” or weak 2-functor, where the structural constraints are isomorphisms. Here they are simply called 2-functors.

Each 2-category BB gives rise to a hom 2-functor hom:B op×BCathom: B^{op} \times B \to Cat, which we denote by B(,)B(-, -), with the contravariant argument in the first place as is customary.

Given 2-functors F,G:BCF, G: B \to C, it is for our purposes convenient to use the lax notion of morphism θ:FG\theta: F \to G between 2-functors for which the structural cells θf\theta \cdot f (for 1-cells f:abf: a \to b in BB) point in the direction

Fa θa Ga Ff θf Gf Fb θb Gb\array{ F a & \overset{\theta a}{\to} & G a\\ F f \downarrow & \overset{\theta \cdot f}{\Rightarrow} & \downarrow G f\\ F b & \underset{\theta b}{\to} & G b }

These are called “oplax transformations” by some authors such as Bénabou and “lax transformations” by other authors such as Johnstone; on this page we will simply call them (2-)transformations. A transformation is strong if the structural cells θf\theta \cdot f are isomorphisms.

There is a well-known notion of morphism between transformation which has been called modification. We retain this usage, but as an aside we counsel against inventing a new term (e.g., “perturbation” between modifications) every time a new level of morphism is reached – a more uniform terminology is called for. The term “transfor” (due to Sjoerd Crans) has been tentatively adopted elsewhere on this site; modifications may then be called 2-transfors.

In any case, given 2-categories BB and CC, there is a 2-category of 2-functors, strong transformations and modifications from BB to CC; this will be denoted Hom s(B,C)Hom_s(B, C). We have also the 2-category of 2-functors, transformations, and modifications; this will be denoted Hom l(B,C)Hom_l(B, C).

2-adjunctions between 2-categories

A 2-adjunction FGF \dashv G consists of 2-functors F:BCF: B \to C, G:CBG: C \to B, and an adjoint equivalence

C(F,)B(,G)C(F -, -) \simeq B(-, G -)

in the 2-category Hom s(B op×C,Cat)Hom_s(B^{op} \times C, Cat). In more elementary terms, the data of a 2-adjunction is given by strong transformations

η:1 BGFε:FG1 C\eta: 1_B \to G F \qquad \varepsilon: F G \to 1_C

and invertible modifications (called triangulators)

G ηG GFG F Fη FGF 1 G s Gε 1 F t εF G 1 G G F 1 F F\array{ G & \overset{\eta G}{\to} & G F G & & & & F & \overset{F\eta}{\to} & F G F\\ 1_G \downarrow & \overset{s}{\Rightarrow} & \downarrow G \varepsilon & & & & 1_F \downarrow & \overset{t}{\Leftarrow} & \downarrow \varepsilon F\\ G & \underset{1_G}{\to} & G & & & & F & \underset{1_F}{\to} & F }

such that the triangulator coherence conditions hold: there are pasting diagram equalities

1 B η GF 1 GF GF η ηη GFη 1 GF GF ηGF GFGF Gt GF = 1 η 1 GF sF GεF 1 GF GF 1 GF GF 1 GF GF\array{ 1_B & \overset{\eta}{\to} & G F & \overset{1_{G F}}{\to} & G F\\ \eta \downarrow & \overset{\eta \cdot \eta}{\Rightarrow} & \downarrow G F \eta & & \downarrow 1_{G F}\\ G F & \underset{\eta G F}{\to} & G F G F & \overset{G t}{\Rightarrow} & G F & & & = & 1_{\eta}\\ 1_{G F} \downarrow & & \overset{s F}{\Rightarrow} & G \varepsilon F \searrow & \downarrow 1_{G F} \\ G F & \underset{1_{G F}}{\to} & G F & \underset{1_{G F}}{\to} & G F }


FG 1 FG FG 1 FG FG 1 FG FηG tG 1 FG FG Fs FGFG εFG FG = 1 ε 1 FG FGε εε ε FG 1 FG FG ε 1\array{ F G & \overset{1_{F G}}{\to} & F G & \overset{1_{F G}}{\to} & F G\\ 1_{F G} \downarrow & F \eta G \searrow & \overset{t G}{\Rightarrow} & & \downarrow 1_{F G}\\ F G & \overset{F s}{\Rightarrow} & F G F G & \overset{\varepsilon F G}{\to} & F G & & & = & 1_{\varepsilon}\\ 1_{F G} \downarrow & & F G \varepsilon \downarrow & \overset{\varepsilon \cdot \varepsilon}{\Rightarrow} & \downarrow \varepsilon\\ F G & \underset{1_{F G}}{\to} & F G & \underset{\varepsilon}{\to} & 1 }

Lax adjunctions between 2-categories

A lax adjunction is defined in the same way as a 2-adjunction, except that we relax (remove) the assumptions that η\eta and ε\varepsilon are strong and that ss, tt are invertible; the triangulator coherence conditions are still in effect. In that case, for objects bb of BB and cc of CC, there is a local adjunction between hom-categories

(L:B(b,Gc)C(Fb,c))(R:C(Fb,c)B(b,Gc))(L: B(b, G c) \to C(F b, c)) \dashv (R: C(F b, c) \to B(b, G c))

given by L(g:bGc)=(FbFgFGcεcc)L(g: b \to G c) = (F b \overset{F g}{\to} F G c \overset{\varepsilon c}{\to} c) and R(f:Fbc)=(bηbGFbGfGc)R(f: F b \to c) = (b \overset{\eta b}{\to} G F b \overset{G f}{\to} G c). The unit of LRL \dashv R at g:bGcg: b \to G c is given by the pasting

b g Gc 1 Gc Gc ηb ηg ηGc sc 1 Gc GFb GFg GFGc Gε Gc\array{ b & \overset{g}{\to} & G c & \overset{1_{G c}}{\to} & G c\\ \eta b \downarrow & \overset{\eta \cdot g}{\Leftarrow} & \downarrow \eta G c & \overset{s c}{\Leftarrow} & \downarrow 1_{G c}\\ G F b & \underset{G F g}{\to} & G F G c & \underset{G \varepsilon}{\to} & G c }

and the counit of LRL \dashv R at f:Fbcf: F b \to c is given by the pasting

Fb Fηb FGFb FGf FGc 1 Fb tb εFb εf εc Fb 1 Fb Fb f c\array{ F b & \overset{F \eta b}{\to} & F G F b & \overset{F G f}{\to} & F G c\\ 1_{F b} \downarrow & \overset{t b}{\Leftarrow} & \downarrow \varepsilon F b & \overset{\varepsilon \cdot f}{\Leftarrow} & \downarrow \varepsilon c\\ F b & \underset{1_{F b}}{\to} & F b & \underset{f}{\to} & c }

The triangular equations for LRL \dashv R follow from the triangulator coherence conditions. (Warning: it is not generally true that a lax adjunction induces an adjoint pair in Hom l(B op×C,Cat)Hom_l(B^{op} \times C, Cat). Cf. lemma 1 below.)

The 2-category Map(B)Map(B)

Let BB be a 2-category. Following Carboni and Walters, we define a map in BB to be a 1-cell in BB that possesses a right adjoint. It is useful to think of them as playing the role of “functional relations” in an ambient 2-category of relations. We let Map(B)Map(B) be the locally full sub-2-category whose 0-cells are those of BB and whose 1-cells are the maps in BB. We observe that every 2-functor F:BCF: B \to C restricts to a 2-functor F|:Map(B)Map(C)F|: Map(B) \to Map(C), and by the following proposition, every transformation θ:FG\theta: F \to G restricts to a strong transformation θ\theta in Hom s(Map(B),C)Hom_s(Map(B), C):

Proposition 1: If f:bcf: b \to c is a map in BB, then θf\theta \cdot f is invertible.

Proof: Let f *f^* denote a right adjoint of ff. It is easily verified that the diagram

Fb Ff Fc θc Gc 1 Gc Gc 1 Fb Ff * θf * Gf * 1 Gc Fb 1 Fb Fb θb Gb Gf Gc\array{ F b & \overset{F f}{\to} & F c & \overset{\theta c}{\to} & G c & \overset{1_{G c}}{\to} & G c\\ 1_{F b} \downarrow & \Rightarrow & F f^* \downarrow & \overset{\theta \cdot f^*}{\Rightarrow} & \downarrow G f^* & \Rightarrow & \downarrow 1_{G c}\\ F b & \underset{1_{F b}}{\to} & F b & \underset{\theta b}{\to} & G b & \underset{G f}{\to} & G c }

pastes to give the inverse (θf) 1(\theta \cdot f)^{-1}, where the left and right squares are the unit and counit of adjunctions FfFf *F f \dashv F f^*, GfGf *G f \dashv G f^*.

A transformation θ:FG:BC\theta: F \to G: B \to C is map-valued if each 1-cell θb\theta b is a map in CC. By the previous proposition, a map-valued transformation θ\theta in Hom l(B,C)Hom_l(B, C) restricts to a strong transformation θ|:F|G|\theta|: F| \to G| in Hom s(Map(B),Map(C))Hom_s(Map(B), Map(C)).

  • Warning: In general it is imprecise to identify maps in a 2-category with the “functional relations”. That is, for some of the standard examples of cartesian bicategories, such as B=ProfB = Prof, we cannot simply identify Map(B)Map(B) with CatCat: 1-cell equivalences are only Morita equivalences, not CatCat-equivalences. A better adapted framework is one of a bicategory with a proarrow equipment, or a framed bicategory. Eventually this article will be rewritten with this remark in mind…

Definition of cartesian structure and basic results

A cartesian structure on a bicategory BB consists of the following data:

  • 2-functors :B×BB\otimes: B \times B \to B and I:1BI: \mathbf{1} \to B, where 1\mathbf{1} is the terminal 2-category;

  • Map-valued transformations

    δ:1 BΔ,π:Δ1 B×B,ε:1 BI!\delta: 1_B \to \otimes \Delta, \qquad \pi: \Delta \otimes \to 1_{B \times B}, \qquad \varepsilon: 1_B \to I !

    where Δ:BB×B\Delta: B \to B \times B is the diagonal 2-functor and !:B1!: B \to \mathbf{1} is the unique 2-functor;

  • Invertible modifications

    δ Δ Δ Δδ ΔΔ I εI I!I 1 s π 1 Δ t πΔ 1 I u Iid 1 Δ 1 Δ Δ I 1 I I\array{ \otimes & \overset{\delta \otimes}{\to} & \otimes \Delta \otimes & & & & \Delta & \overset{\Delta \delta}{\to} & \Delta \otimes \Delta & & & & I & \overset{\varepsilon I}{\to} & I ! I\\ \mathllap{1_{\otimes}} \downarrow & \overset{s}{\Rightarrow} & \downarrow \mathrlap{\otimes \pi} & & & & \mathllap{1_{\Delta}} \downarrow & \overset{t}{\Leftarrow} & \downarrow \mathrlap{\pi \Delta} & & & & \mathllap{1_{I}} \downarrow & \overset{u}{\Rightarrow} & \downarrow \mathrlap{I \cdot id}\\ \otimes & \underset{1_{\otimes}}{\to} & \otimes & & & & \Delta & \underset{1_{\Delta}}{\to} & \Delta & & & & I & \underset{1_I}{\to} & I }

    satisfying the triangulator coherence conditions. \Box

The crucial observation is that, by proposition 1, this data restricts to give 2-adjunctions

(Map(B)ΔMap(B)×Map(B))(Map(B)×Map(B)Map(B))(Map(B) \overset{\Delta}{\to} Map(B) \times Map(B)) \dashv (Map(B) \times Map(B) \overset{\otimes}{\to} Map(B))
(Map(B)!1)(1IMap(B))(Map(B) \overset{!}{\to} \mathbf{1}) \dashv (\mathbf{1} \overset{I}{\to} Map(B))

making the restriction of \otimes to Map(B)Map(B) a 2-product on Map(B)Map(B) with 2-terminal object II. Naturally this finite 2-product structure on Map(B)Map(B) is property-like: is uniquely determined up to equivalence which is uniquely specified up to unique isomorphism.

A little later we will argue that cartesian structure on the full bicategory BB is also property-like; the main thing is to see that the way in which \otimes acts on 1-cells is essentially uniquely determined.

Symmetric monoidal structure via cartesian structure

We now argue that a cartesian bicategory BB carries a symmetric monoidal structure whose tensor product is

:B×BB\otimes: B \times B \to B

The proof is pretty easy to sketch, once the fact is admitted that the induced 2-product structure makes Map(B)Map(B) a symmetric monoidal bicategory. This fact about 2-products, while never in dispute, was given a complete proof only in the past few years by the late Max Kelly, and we freely take advantage of it below.

First, given objects a,b,ca, b, c of BB, we may regard them as objects of Map(B)Map(B), where there is an associativity constraint

α a,b,c:(ab)ca(bc)\alpha_{a, b, c}: (a \otimes b) \otimes c \to a \otimes (b \otimes c)

on Map(B)Map(B) which is definable by exploiting 2-universal properties of the 2-product. The associativity thus has an expression in terms of \otimes, δ\delta, and π\pi which are globally defined on BB, hence α\alpha is globally defined as a transformation on BB. By similar considerations, the symmetry and unit constraints on Map(B)Map(B) also extend to globally defined transformations on BB. We argue in a moment that these constraints are strong (adjoint) equivalences.

Symmetric monoidal structure on BB also demands various structural modifications (such as a Yang-Baxter modification R |,R_{\bullet |\bullet, \bullet}) satisfying various coherence conditions, but the components of such modifications (R a|b,cR_{a|b, c}, say) are defined by regarding their components a,b,ca, b, c as objects of Map(B)Map(B) and using the corresponding modifications there. Again, each such modification on Map(B)Map(B) is defined in terms of 2-adjunction data \otimes, II, δ\delta, π\pi, ε\varepsilon, ss, tt, uu which are globally defined on BB, so each such structure is a modification on BB. Various coherence conditions on the modifications must be checked, but the conditions hold at every choice of objects of BB by regarding them as objects of Map(B)Map(B) and using the symmetric monoidal structure there, so the conditions hold on BB.

Now we check that the structural transformations α\alpha are strong adjoint equivalences. Indeed, when regarded as being defined on Map(B)Map(B), the constraint α\alpha is an equivalence and so has a left adjoint (with invertible unit and counit) α \alpha^- with components

α a,b,c :a(bc)(ab)c\alpha_{a, b, c}^{-}: a \otimes (b \otimes c) \to (a \otimes b) \otimes c

and just like α\alpha, α \alpha^- is definable in terms of global structure on BB, making α \alpha^- a transformation on BB. Then α\alpha, and by similar reasoning the symmetry and unit constraints, are strong transformations on BB by the following lemma:

Lemma 1: If α\alpha is a right adjoint in Hom l(C,B)Hom_l(C, B), then the transformation α\alpha is strong. Consequently, if α α\alpha^- \dashv \alpha is an adjoint equivalence, so that both α α\alpha^- \dashv \alpha and αα \alpha \dashv \alpha^-, then α α\alpha^- \dashv \alpha is a strong adjoint equivalence in Hom s(C,B)Hom_s(C, B).

Proof: Only the first statement requires proof. Given r:cdr: c \to d in CC, let ev c:Hom l(C,B)Bev_c: Hom_l(C, B) \to B denote the 2-functor which evaluates at cc (keep in mind that the 1-cells in Hom l(C,B)Hom_l(C, B) are transformations which are oplax in the sense of Bénabou), and let ev r:ev cev dev_r: ev_c \to ev_d denote the evident transformation; this is lax in the sense of Bénabou. Then, by dualizing proposition 1, ev r(α)=αrev_r(\alpha) = \alpha \cdot r is an isomorphism if α\alpha is a right adjoint. Since αr\alpha \cdot r is an isomorphism for all 1-cells rr in CC, it follows that α\alpha is strong. \Box

This completes the argument that the symmetric monoidal structure on Map(B)Map(B) extends to BB.

Comparison with Carboni-Walters

Let us begin unpacking the terse definition of cartesian bicategory so that it becomes more recognizable. For the sake of notational convenience, we use the fact that as a monoidal bicategory, a cartesian bicategory may be strictified and replaced by a (monoidally biequivalent) GrayGray monoid BB. That is to say, if G\otimes_G denotes the tensor product of the symmetric monoidal closed category GrayGray, then there is firstly a biequivalence B×BB GBB \times B \simeq B \otimes_G B, and we may transfer the data of the cartesian structure across this biequivalence to get a GrayGray monoid multiplication

:B GBB\otimes: B \otimes_G B \to B

together with a corresponding diagonal

BΔB×BB GBB \overset{\Delta}{\to} B \times B \simeq B \otimes_G B

which we again denote by Δ\Delta. In that case, given a 1-cell r:abr: a \to b in BB, we may write structure cells δr\delta \cdot r for the transformation δ:1 BΔ\delta: 1_B \to \otimes \Delta in the form

a δa aa r δr rr b δb bb\array{ a & \overset{\delta a}{\to} & a \otimes a\\ r \downarrow & \overset{\delta \cdot r}{\Rightarrow} & \downarrow r \otimes r\\ b & \underset{\delta b}{\to} & b \otimes b }

where to be definite we make the convention that rr:=(r1)(1r)r \otimes r := (r \otimes 1)(1 \otimes r).

An object cc of BB, viewed as an object of a 2-category Map(B)Map(B) with 2-products, naturally carries a 2-comonoid (or pseudocomonoid) structure; the unit of the 2-adjunction Δ\Delta \dashv \otimes is the diagonal map

δc:ccc,\delta c: c \to c \otimes c,

i.e., the 2-comonoid comultiplication. The unit of the 2-adjunction !I! \dashv I is the projection to the 2-terminal object

εc:cI,\varepsilon c: c \to I,

i.e., the 2-comonoid counit. (It is more usual to denote a (2-)terminal object by the symbol 11, and from here on we will follow that practice, writing the projection as εc:c1\varepsilon c: c \to 1, and forget II.)

Spelling this out a little further, let us turn attention to the transformation π:Δ1 B GB\pi: \Delta \otimes \to 1_{B \otimes_G B}. The components of the transformation take the form

π(a,b)=π 1,π 2:(ab,ab)(a,b)\pi (a, b) = \langle \pi_1, \pi_2 \rangle: (a \otimes b, a \otimes b) \to (a, b)

where, as a consequence of how the 2-product \otimes on Map(B)Map(B) is defined, we have the following formulas for the projections π 1\pi_1, π 2\pi_2:

π 1=(ab1 aεa1a);π 2=(abε1 b1bb\pi_1 = (a \otimes b \overset{1_a \otimes \varepsilon}{\to} a \otimes 1 \cong a); \qquad \pi_2 = (a \otimes b \overset{\varepsilon \otimes 1_b}{\to} 1 \otimes b \cong b

Thus, the unit and counit data δ\delta, π\pi are expressible in terms of the symmetric monoidal 2-category structure and the comonoid structures on the objects therein.

Finally, for a given 1-cell r:cdr: c \to d in BB, the structure cells

c δc cc c εc 1 r δr rr r εr id 1 d δd dd d εd 1\array{ c & \overset{\delta c}{\to} & c \otimes c & & & & c & \overset{\varepsilon c}{\to} & 1\\ r \downarrow & \overset{\delta \cdot r}{\Rightarrow} & \downarrow r \otimes r & & & & r \downarrow & \overset{\varepsilon \cdot r}{\Rightarrow} & \downarrow id_1\\ d & \underset{\delta d}{\to} & d \otimes d & & & & d & \underset{\varepsilon d}{\to} & 1 }

exhibit r:cdr: c \to d as a colax morphism of 2-comonoids; if rr is a map, then δr\delta \cdot r and εr\varepsilon \cdot r are isomorphisms and rr becomes a strong morphism of 2-comonoids. This may be appreciated more fully by considering specific examples such as B=RelB = Rel (where maps are functions, which become comonoid morphisms by virtue of naturality of diagonal and projection maps), and B=ModB = Mod.

Carboni and Walters define a cartesian bicategory to be a symmetric monoidal bicategory in which each object carries a 2-comonoid structure (for which the comultiplication and counit are maps), and each 1-cell is a colax morphism between the corresponding comonoid structures. However, spelling this approach out in full detail leads to a rather largish definition; it seems more efficient to approach the definition by taking advantage of some high-level 2-categorical algebra as we have done here, and deriving the structures envisaged by Carboni and Walters as a consequence.

Local cartesian products

The definition of cartesian structure a fortiori involves lax adjunctions (in the sense explained earlier)

Δ lax:B×BB! laxI:1B\Delta \dashv_{lax} \otimes: B \times B \to B \qquad ! \dashv_{lax} I: \mathbf{1} \to B

and by our earlier discussion of lax adjunctions, this means we have local 1-adjunctions of the form

(B(a,bc)λ(B×B)(a,a,b,c))(B×B)(a,a,b,c))ρB(a,bc))(B(a, b \otimes c) \stackrel{\lambda}{\to} (B \times B)(\langle a, a \rangle, \langle b, c \rangle)) \dashv (B \times B)(\langle a, a \rangle, \langle b, c \rangle)) \stackrel{\rho}{\to} B(a, b \otimes c))

Now let b=cb = c, and use the fact that we have an adjunction

(bδbbb)(bbδb *b)(b \stackrel{\delta b}{\to} b \otimes b) \dashv (b \otimes b \stackrel{\delta b^{\ast}}{\to} b)

to obtain an adjoint pair where

B(a,b)B(a,δb)B(a,bb)λB×B(a,a,b,b)B(a, b) \stackrel{B(a, \delta b)}{\to} B(a, b \otimes b) \stackrel{\lambda}{\to} B \times B(\langle a, a \rangle, \langle b, b \rangle)

is left adjoint to

B×B(a,a,b,b)ρB(a,bb)B(a,δb *)B(a,b).B \times B(\langle a, a \rangle, \langle b, b \rangle) \stackrel{\rho}{\to} B(a, b \otimes b) \stackrel{B(a, \delta b^\ast)}{\to} B(a, b).

The first of these arrows is just the diagonal functor

B(a,b)δ locB(a,b)×B(a,b)B(a, b) \stackrel{\delta_{loc}}{\to} B(a, b) \times B(a, b)

on the local hom-category B(a,b)B(a, b). Therefore the second arrow, being right adjoint to the first, provides a product functor on B(a,b)B(a, b). Similarly, each local hom-category carries a terminal object 1hom(a,b)1 \to \hom(a, b). We may summarize this by saying that cartesian bicategories are locally cartesian.

Essential uniqueness of cartesian structure

So far we have seen that for a cartesian bicategory BB,

  • Map(B)Map(B) carries 2-products,

  • Local hom-categories carry products.

It is clear that 2-product data on Map(B)Map(B) and local product data on local hom-categories are uniquely determined up to appropriate notions of equivalence, since they are determined by appropriate universal properties. Now we show that these data actually determine the whole of the cartesian structure. We may therefore conclude that a cartesian structure on a bicategory must be essentially unique, if it exists.

To explain how this works, it helps to consider some simple examples of cartesian bicategories such as RelRel. First, let us reconstruct

:B×BB\otimes: B \times B \to B

from the data above. Suppose given two 1-cells r:abr: a \to b, s:cds: c \to d in BB, e.g., relations between sets, or even just subsets rbr \subseteq b, sds \subseteq d. The tensor product rsr \otimes s is intuitively a “rectangle”, like r×sb×dr \times s \subseteq b \times d in the case of RelRel, obtained by “pulling back” rr along the projection π 1:b×db\pi_1: b \times d \to b, pulling back ss along the projection π 2:b×dd\pi_2: b \times d \to d, and taking the intersection – more generally, taking a local product. By formalizing this procedure, we are led to the general formula

rs(π 1,b,d *rπ 1,a,c)× loc(π 2,b,d *sπ 2,a,c)r \otimes s \cong (\pi_{1, b, d}^{\ast} r \pi_{1, a, c}) \times_{loc} (\pi_{2, b, d}^{\ast} s \pi_{2, a, c})

where rr and ss play the role of mere placeholders.

It is a theorem (whose proof we defer) is that in a cartesian bicategory, we may reconstruct the functor - \otimes - by the formula

(π 1 *()π 1)× loc(π 2 *()π 2)(\pi_{1}^{\ast} (-) \pi_{1}) \times_{loc} (\pi_{2}^{\ast} (-) \pi_{2})

where each of the displayed data is manifestly part of the 2-product structure on Map(B)Map(B) or the local cartesian structure.

The other data we are required to reconstruct are structure cells like δr\delta r, πr,s\pi \langle r, s\rangle which pertain to the transformations δ\delta, π\pi. As an example, consider δr\delta r. This is a 2-cell

δr:(δb)r(rr)(δa)\delta r: (\delta b)r \to (r \otimes r)(\delta a)

which is mated to a 2-cell

r(δb) *(rr)δ=r× locr.r \to (\delta b)^\ast (r \otimes r) \delta = r \times_{loc} r.

This 2-cell is precisely the local diagonal rr×rr \to r \times r, manifestly part of the local cartesian structure. Thus the structure cells for δ\delta are uniquely determined, and similarly for the transformations π\pi and ε\varepsilon.

This completes the sketched proof of essential uniqueness.

Cartesian bicategories and hyperdoctrines

Each cartesian bicategory B\mathbf{B} gives rise to a bifibration, or in other language a (weak) 2-functor

B(i,i):Map(B) op×Map(B)Cat\mathbf{B}(i-, i-): Map(\mathbf{B})^{op} \times Map(\mathbf{B}) \to Cat

or in other words a CatCat-valued bimodule over Map(B)Map(\mathbf{B}), for which each B(if,ic):B(ib,ic)B(ia,ic)\mathbf{B}(i f, i c): \mathbf{B}(i b, i c) \to \mathbf{B}(i a, i c) has a left adjoint

B(f *,ic):B(ia,ic)B(ib,ic)\mathbf{B}(f^\ast, i c): \mathbf{B}(i a, i c) \to \mathbf{B}(i b, i c)

and similarly each B(ic,if):B(ic,ia)B(ic,ib)\mathbf{B}(i c, i f): \mathbf{B}(i c, i a) \to \mathbf{B}(i c, i b) has a right adjoint B(ic,f *)\mathbf{B}(i c, f^\ast).

Thus, each cartesian bicategory gives rise to an Ob(B)Ob(\mathbf{B})-indexed family B(i,c)\mathbf{B}(i-, c) of what we shall call ([faute de mieux]) generalized coherent hyperdoctrines:


Let CC be a 2-category with 2-products. A generalized coherent hyperdoctrine over CC is a 2-functor

P:C opFPCatP: C^{op} \to FPCat

to the 2-category of categories with finite products, such that for each 1-cell ff in CC, the functor P(f)P(f) has a left adjoint.

This is called a generalized coherent hyperdoctrine because it deals with a generalized form of coherent logic (involving finite “conjunctions”, i.e., local finite cartesian products and existential quantifiers fP(f)\exists_f \dashv P(f)). It is actually a weak form of coherent logic because we have not included finite “disjunctions”, and we have said nothing yet about appropriate Beck-Chevalley conditions. (More will be said on this in a section to follow.) It is generalized in the sense that the base category CC is actually a 2-category.

If the symmetric monoidal bicategory B\mathbf{B} is compact (e.g., if B\mathbf{B} is of type Rel CRel_C for CC a regular category, or Span CSpan_C for CC a finitely complete category, or the bicategory of small categories and profunctors between them), then without loss of generality, we may restrict attention to the single hyperdoctrine

B(i,1):Map(B) opFPCat\mathbf{B}(i-, 1): Map(\mathbf{B})^{op} \to FPCat

Frobenius conditions

A major class of examples of cartesian bicategories, including RelRel, SpanSpan, and the bicategory of profunctors between groupoids, have the properties that

  • Each object is self-dual (in the sense of compact closed bicategories),

  • The bicategory of maps is locally groupoidal.

These arise as follows. In any cartesian bicategory and for each object bb, there is a canonical 2-cell

Frob b:(δb)(δb) *(1 bδb *)(δb1 b)Frob_b: (\delta b)(\delta b)^\ast \to (1_b \otimes \delta b^\ast)(\delta b \otimes 1_b)

mated to the coassociativity isomorphism for δ\delta. We say the Frobenius condition holds if Frob bFrob_b is an isomorphism for each bb. This is equivalent to demanding that a similar canonical 2-cell

Frob b:(δb)(δb) *(δb *1 b)(1 bδb)Frob_{b}': (\delta b)(\delta b)^\ast \to (\delta b^\ast \otimes 1_b)(1_b \otimes \delta b)

be an isomorphism for each bb.

Revised on September 26, 2017 14:31:45 by Mike Shulman (