## 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:A\to B$ and $g:B\to A$ along with a natural isomorphism

$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 $f 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 $A$ and $B$ are 2-categories and we replace it by “equivalence”, we get a biadjunction.
• If $A$ and $B$ 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\times B\to C$ and $g:A^{op}\times C\to B$ and $h:B^{op}\times C\to A$ along with natural isomorphisms

$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)) \times B(b,g(a,c)) \to C(f(a,b),c).$

Even more intriguingly, if $A,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)) \times B(b,g(a,c)) \to C(f(a,b),c)$ a “replacement” for isomorphisms $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)$.

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(\mathcal{C},\Omega)$ and $Dial(\mathcal{C},\Omega)$ have the same objects: triples $A=(A^+,A^-,\underline{A})$ where $A^+,A^-$ are objects of $\mathcal{C}$ and $\underline{A} : A^+ \otimes A^- \to \Omega$ is a morphism in $\mathcal{C}$. Finally, the morphisms $f:A\to B$ in both $Chu(\mathcal{C},\Omega)$ and $Dial(\mathcal{C},\Omega)$ consist of a pair of morphisms $f^+ : A^+ \to B^+$ and $f^- : B^- \to A^-$ (note the different directions) subject to some condition.

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

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

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

are equal. But in $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)$ as the objects of the form $(A,A^{op},hom_A)$. The analogous category sitting inside $Dial(Cat,Set)$, where $Set$ is regarded as an internal category in $Cat$ in the obvious way, would consist of “generalized adjunctions” of the first sort, with simple functions $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(\mathcal{C},\Omega)$ is clearly the special case of $Dial(\mathcal{C},\Omega)$ where $\Omega$ has a discrete preorder (i.e. $x\le y$ iff $x=y$). But $Chu(\mathcal{C},\Omega)$ is always $\ast$-autonomous, as long as $\mathcal{C}$ has pullbacks; whereas for $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(\mathcal{C},\Omega)$ does not coincide with that of $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(\mathcal{C},\Omega)$ and $Dial(\mathcal{C},\Omega)$, we should compare the functors that they represent. A morphism $A\otimes B\to C$ in $Chu(\mathcal{C},\Omega)$ consists of three mophisms $f:A^+\otimes B^+\to C^+$ and $g:A^+ \otimes C^- \to B^-$ and $h:B^+ \otimes C^- \to A^-$ such that a certain three morphisms $A^+ \otimes B^+ \otimes C^- \to \Omega$ are equal. In terms of “formal elements” $a:A^+, b:B^+,c:C^-$ in the internal type theory of $\mathcal{C}$, these certain three morphisms can be written as

$\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 $A\otimes B\to C$ in $Dial(\mathcal{C},\Omega)$ consists of three morphisms $f,g,h$ of the same sorts, but such that

$\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)$ we equip $Set$ with its usual monoidal structure, we get generalized 2-variable adjunctions with a function $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,\dots,x_m) \to (y_1,\dots,y_n)$ is the assertion that $x_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(\mathcal{C},\Omega)$ and $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:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2999

### 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