Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

December 4, 2017

The 2-Dialectica Construction: A Definition in Search of Examples

Posted by Mike Shulman

An adjunction is a pair of functors f:ABf:A\to B and g:BAg:B\to A along with a natural isomorphism

A(a,gb)B(fa,b). A(a,g b) \cong B(f a,b).

Question 1: Do we get any interesting things if we replace “isomorphism” in this definition by something else?

  • If we replace it by “function”, then the Yoneda lemma tells us we get just a natural transformation fg1 Bf g \to 1_B.
  • If we replace it by “retraction” then we get a unit and counit, as in an adjunction, satisfying one triangle identity but not the other.
  • If AA and BB are 2-categories and we replace it by “equivalence”, we get a biadjunction.
  • If AA and BB are 2-categories and we replace it by “adjunction”, we get a sort of lax 2-adjunction (a.k.a. “local adjunction”)

Are there other examples?

Question 2: What if we do the same thing for multivariable adjunctions?

A two-variable adjunction is a triple of functors f:A×BCf:A\times B\to C and g:A op×CBg:A^{op}\times C\to B and h:B op×CAh:B^{op}\times C\to A along with natural isomorphisms

C(f(a,b),c)B(b,g(a,c))A(a,h(b,c)). C(f(a,b),c) \cong B(b,g(a,c)) \cong A(a,h(b,c)).

What does it mean to “replace ‘isomorphism’ by something else” here? It could mean different things, but one thing it might mean is to ask instead for a function

A(a,h(b,c))×B(b,g(a,c))C(f(a,b),c). A(a,h(b,c)) \times B(b,g(a,c)) \to C(f(a,b),c).

Even more intriguingly, if A,B,CA,B,C are 2-categories, we could ask for an ordinary two-variable adjunction between these three hom-categories; this would give a certain notion of “lax two-variable 2-adjunction”. Question 2 is, are notions like this good for anything? Are there any natural examples?

Now, you may, instead, be wondering about

Question 3: In what sense is a function A(a,h(b,c))×B(b,g(a,c))C(f(a,b),c) A(a,h(b,c)) \times B(b,g(a,c)) \to C(f(a,b),c) a “replacement” for isomorphisms C(f(a,b),c)B(b,g(a,c))A(a,h(b,c)) C(f(a,b),c) \cong B(b,g(a,c)) \cong A(a,h(b,c)) ?

But that question, I can answer; it has to do with comparing the Chu construction and the Dialectica construction.

Last month I told you about how multivariable adjunctions form a polycategory that sits naturally inside the 2-categorical Chu construction Chu(Cat,Set)Chu(Cat,Set).

Now the classical Chu construction is, among other things, a way to produce *\ast-autonomous categories, which are otherwise in somewhat short supply. At first, I found that rather disincentivizing to study either one: why would I be interested in a contrived way to construct things that don’t occur naturally? But then I realized that the same sentence would make sense if you replaced “Chu construction” with “sheaves on a site” and “*\ast-autonomous categories” with “toposes”, and I certainly think those are interesting. So now it doesn’t bother me as much.

Anyway, there is also another general construction of *\ast-autonomous categories (and, in fact, more general things), which goes by the odd name of the “Dialectica construction”. The categorical Dialectica construction is an abstraction, due to Valeria de Paiva, of a syntactic construction due to Gödel, which in turn is referred to as the “Dialectica interpretation” apparently because it was published in the journal Dialectica. I must say that I cannot subscribe to this as a general principle for the naming of mathematical definitions; fortunately it does not seem to have been very widely adopted.

Anyway, however execrable its name, the Dialectica construction appears quite similar to the Chu construction. Both start from a closed symmetric monoidal category 𝒞\mathcal{C} equipped with a chosen object, which in this post I’ll call Ω\Omega. (Actually, there are various versions of both, but here I’m going to describe two versions that are maximally similar, as de Paiva did in her paper Dialectica and Chu constructions: Cousins?.) Moreover, both Chu(𝒞,Ω)Chu(\mathcal{C},\Omega) and Dial(𝒞,Ω)Dial(\mathcal{C},\Omega) have the same objects: triples A=(A +,A ,A̲)A=(A^+,A^-,\underline{A}) where A +,A A^+,A^- are objects of 𝒞\mathcal{C} and A̲:A +A Ω\underline{A} : A^+ \otimes A^- \to \Omega is a morphism in 𝒞\mathcal{C}. Finally, the morphisms f:ABf:A\to B in both Chu(𝒞,Ω)Chu(\mathcal{C},\Omega) and Dial(𝒞,Ω)Dial(\mathcal{C},\Omega) consist of a pair of morphisms f +:A +B +f^+ : A^+ \to B^+ and f :B A f^- : B^- \to A^- (note the different directions) subject to some condition.

The only difference is in the conditions. In Chu(𝒞,Ω)Chu(\mathcal{C},\Omega), the condition is that the composites

A +B 1f A +A A̲ΩA^+ \otimes B^- \xrightarrow{1\otimes f^-} A^+ \otimes A^- \xrightarrow{\underline{A}} \Omega

A +B f +1B +B B̲ΩA^+ \otimes B^- \xrightarrow{f^+\otimes 1} B^+ \otimes B^- \xrightarrow{\underline{B}} \Omega

are equal. But in Dial(𝒞,Ω)Dial(\mathcal{C},\Omega), we assume that Ω\Omega is equipped with an internal preorder, and require that the first of these composites is \le the second with respect to this preorder.

Now you can probably see where Question 1 above comes from. The 2-category of categories and adjunctions sits inside Chu(Cat,Set)Chu(Cat,Set) as the objects of the form (A,A op,hom A)(A,A^{op},hom_A). The analogous category sitting inside Dial(Cat,Set)Dial(Cat,Set), where SetSet is regarded as an internal category in CatCat in the obvious way, would consist of “generalized adjunctions” of the first sort, with simple functions A(a,gb)B(fa,b)A(a,g b) \to B(f a,b) rather than isomorphisms. Other “2-Dialectica constructions” would yield other sorts of generalized adjunction.

What about Questions 2 and 3? Well, back up a moment: the above description of the Chu and Dialectica constructions actually exaggerates their similarity, because it omits their monoidal structures. As a mere category, Chu(𝒞,Ω)Chu(\mathcal{C},\Omega) is clearly the special case of Dial(𝒞,Ω)Dial(\mathcal{C},\Omega) where Ω\Omega has a discrete preorder (i.e. xyx\le y iff x=yx=y). But Chu(𝒞,Ω)Chu(\mathcal{C},\Omega) is always *\ast-autonomous, as long as 𝒞\mathcal{C} has pullbacks; whereas for Dial(𝒞,Ω)Dial(\mathcal{C},\Omega) to be monoidal, closed, or *\ast-autonomous we require the preorder Ω\Omega to have those same properties, which a discrete preorder certainly does not always. And even when a discrete preorder Ω\Omega does have some or all those properties, the resulting monoidal structure of Dial(𝒞,Ω)Dial(\mathcal{C},\Omega) does not coincide with that of Chu(𝒞,Ω)Chu(\mathcal{C},\Omega).

As happens so often, the situation is clarified by considering universal properties. That is, rather than comparing the concrete constructions of the tensor products in Chu(𝒞,Ω)Chu(\mathcal{C},\Omega) and Dial(𝒞,Ω)Dial(\mathcal{C},\Omega), we should compare the functors that they represent. A morphism ABCA\otimes B\to C in Chu(𝒞,Ω)Chu(\mathcal{C},\Omega) consists of three mophisms f:A +B +C +f:A^+\otimes B^+\to C^+ and g:A +C B g:A^+ \otimes C^- \to B^- and h:B +C A h:B^+ \otimes C^- \to A^- such that a certain three morphisms A +B +C ΩA^+ \otimes B^+ \otimes C^- \to \Omega are equal. In terms of “formal elements” a:A +,b:B +,c:C a:A^+, b:B^+,c:C^- in the internal type theory of 𝒞\mathcal{C}, these certain three morphisms can be written as

C̲(f(a,b),c)B̲(b,g(a,c))A̲(a,h(b,c)) \underline{C}(f(a,b),c) \qquad \underline{B}(b,g(a,c)) \qquad \underline{A}(a,h(b,c))

just as in a two-variable adjunction. By contrast, a morphism ABCA\otimes B\to C in Dial(𝒞,Ω)Dial(\mathcal{C},\Omega) consists of three morphisms f,g,hf,g,h of the same sorts, but such that

B̲(b,g(a,c))A̲(a,h(b,c))C̲(f(a,b),c) \underline{B}(b,g(a,c)) \boxtimes \underline{A}(a,h(b,c)) \le \underline{C}(f(a,b),c)

where \boxtimes denotes the tensor product of the monoidal preorder Ω\Omega. Now you can probably see where Question 2 comes from: if in constructing Dial(Cat,Set)Dial(Cat,Set) we equip SetSet with its usual monoidal structure, we get generalized 2-variable adjunctions with a function A(a,h(b,c))×B(b,g(a,c))C(f(a,b),c)A(a,h(b,c)) \times B(b,g(a,c)) \to C(f(a,b),c), and for other choices of Ω\Omega we get other kinds.

This is already somewhat of an answer to Question 3: the analogy between ordinary adjunctions and these “generalized adjunctions” is the same as between the Chu and Dialectica constructions. But it’s more satisfying to make both of those analogies precise, and we can do that by generalizing the Dialectica construction to allow Ω\Omega to be an internal polycategory rather than merely an internal poset (or category). If this polycategory structure is representable, then we recover the original Dialectica construction. Whereas if we give an arbitrary object Ω\Omega the (non-representable) “Frobenius-discrete” polycategory structure, in which a morphism (x 1,,x m)(y 1,,y n)(x_1,\dots,x_m) \to (y_1,\dots,y_n) is the assertion that x 1==x m=y 1==y nx_1=\cdots=x_m=y_1=\cdots=y_n, then we recover the original Chu construction.

For a general internal polycategory Ω\Omega, the resulting “Dialectica-Chu” construction will be only a polycategory. But it is representable in the Dialectica case if Ω\Omega is representable, and it is representable in the Chu case if 𝒞\mathcal{C} has pullbacks. This explains why the tensor products in Chu(𝒞,Ω)Chu(\mathcal{C},\Omega) and Dial(𝒞,Ω)Dial(\mathcal{C},\Omega) look different: they are representing two instances of the same functor, but they represent it for different reasons.

So… what about Questions 1 and 2? In other words: if the reason I care about the Chu construction is because it’s an abstraction of multivariable adjunctions, why should I care about the Dialectica construction?

Posted at December 4, 2017 10:26 PM UTC

TrackBack URL for this Entry:

4 Comments & 0 Trackbacks

Re: The 2-Dialectica Construction: A Definition in Search of Examples

For those that don’t read German, and want to look at Gödel’s original, there’s a translation in the Journal of Philosophical Logic: On a hitherto unexploited extension of the finitary standpoint (paywall).

Posted by: David Roberts on December 5, 2017 9:48 PM | Permalink | Reply to this

Re: The 2-Dialectica Construction: A Definition in Search of Examples

Hi this is interesting. Have you come across recent work on Dialectica models of type theory, e.g. by Tamara von Glehn and by Sean Moss? (stemming partly from Hyland’s “Proof theory in the abstract”.) I ask because this might give you another reason to care about the Dialectica construction (as you put it).

Posted by: Sam S on December 6, 2017 9:12 PM | Permalink | Reply to this

Re: The 2-Dialectica Construction: A Definition in Search of Examples

Possibly. I remember that in von Glehn’s thesis she constructed a model of dependent type theory that has something to do with Dialectica. Is there more published that you can point to?

I wasn’t looking for general reasons to care about the Dialectica construction, though; I accept that some people find it interesting for syntactic/computational sorts of reasons. Mainly I was curious whether this sort of “generalized multivariable adjunction” has any interesting examples.

Posted by: Mike Shulman on December 6, 2017 10:07 PM | Permalink | Reply to this

Re: The 2-Dialectica Construction: A Definition in Search of Examples

well Mike, as you said it above,

But it is representable in the Dialectica case if Ω is representable, and it is representable in the Chu case if 𝒞 has pullbacks

Now getting structure on your construction from the target you’re mapping into, is a time-honoured tradition in maths. we do it all the time, in sheaves, H-sets, B-sets, you name it.

Using pullbacks to mimick logical structural, as in Makkai-Reyes categorical model theory, is more recent. One of the possible “proofs of the pudding” is the logical generalizations a construction affords, as mentioned by Sam Staton. I, for one, am looking forward to more short publications by Tamara von Glehn and Sean Moss, as PhD theses are always heavy going.

Posted by: Valeria on December 7, 2017 2:34 PM | Permalink | Reply to this

Post a New Comment