Wednesday, July 7, 2021

Cousins: twice removed?


 A long time ago I wrote a paper Dialectica and Chu constructions: Cousins?(Theory and Applications of Categories, Vol. 17, 2006, No. 7, pp 127-152) because I felt that the Chu construction and the Dialectica construction were similar in some ways, but still very different from each other in other ways.  I wanted some nice, explanatory result connecting the two. I didn't get the nice smooth and informative result that I wanted to get, but at least I got to write down some obvious facts I knew and this was better than nothing. (I still don't know if there are beautiful smooth results to be found. one lives in hopes.) 

Michael Shulman did produce a nice generalization of both constructions in his The 2-Chu-Dialectica construction and the polycategory of multivariable adjunctions (2018), but it is still not clear to me that this is the best that we can say. Mike is generalizing the usual 1-categorical Chu and Dialectica constructions into 2-categorical constructs. Going into a different generalization direction  Sean Moss and Tamara von Glehn, in their LiCS paper 2018 (Dialectica models of type theory), generalize the Dialectica construction to deal with dependent types, by starting with a fibration p and constructing a generalized Dial(p).

This is very interesting as their paper indicates that the first of their two models for the generalized Dialectica actually corresponds to some category of  "polynomials". In page 8 they say

We are now ready to give the first of our Dialectica constructions, the polynomial model introduced in [34]. The name, which we explain below, fits while we are considering the predicate-free Dialectica construction. 

 This observation leads us to think of  "polynomials" as a predicate-free Dialectica construction, but it is not clear (at least to me) how to make an honest mathematical statement out of this analogy. Which kind of functor should we have? Can we do it for the  'simply-typed'  original Dialectica? Or do we have to introduce fibrations into the picture? The models in von Glehn's thesis (and in the paper) are not exactly simple: it is a tour de force to provide the dependent products in the paper. 

In any case the analogy seems to be that both polynomials and Dialectica constructions seem to correspond to  a big Sigma followed by a big Pi Something, or

   

Now if the Chu construction and Dialectica looked like cousins in 2005, polynomials look much more distant from Dialectica as I know it, hence the title of this blog post. I am trying to write down the bits of mathematics that I know work. It might take a while. 

On the other hand, I just discovered "POLYNOMIALS, FIBRATIONS AND DISTRIBUTIVE LAWS". Maybe Tamara has already sorted it out everything I wanted to know and I just hadn't realized it. Will be reading it now.

No comments:

Post a Comment