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

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