Gödel Fibration?

 

A quick blog post in what I hope will be a series on papers out this year. Three of these papers are now on the arXiv and Google Scholar, yay! The Godel Fibration, Dialectica Petri nets and Kolgomorov-Veloso Problems and Dialectica Categories.

The Gödel fibration with Davide Trotta and Matteo Spadetto is very special to me, as it's my first attempt at a logical generalization of the Dialectica construction. Yes, starting with Martin Hyland in 2002 (`Proof Theory in the Abstract' for a celebration of Anne Troelstra's work)  many other people have worked on these ideas. Amongst others, Bodil Biering in her PhD thesis, Pieter Hofstra's paper in honour of Michael Makkai (The dialectica monad and its cousins) and then Tamara von Glehn and Sean Moss phd theses  (also jointly). 

In the early 90's at the Durham category theory meeting, Bart Jacobs, Thomas Streicher and myself had a long conversation about generalizing dialectica to dependent types, and this became the `famous' exercise in page 117 of Jacob's book. I knew I couldn't reproduce the result of that conversation, but was surprised when I couldn't get either Bart or Thomas to write it for me a few years later: they had moved on. 

 So it was very nice when Davide contacted me with a question about weak coproducts  in the category DC and we ended up, with Matteo's help, writing the Gödel fibration preprint. I am really excited  to pursue the ideas of categorical proof theory as we do in this paper. If you think about it, we have learned from Bill Lawvere more than 50 years ago how to model existential and universal quantifiers using a triple of functors in two adjunctions (for substitution, for all and there exists). It's surprising and interesting that we didn't know how to say categorically that a formula is universal-quantifier-free (or existential-quantifier-free, if you prefer). These notions are the crux of the argument in our paper, which we hope to develop a bit more in the next months.

Looking for Bill's website I fell once again into the delightful rabbit hole of reading his lovely commentaries on friends departed. In particular, I had not read  his tribute to  Aurelio Carboni and it's really very nice!

Lazy Days of Summer? Bah, humbug!

 Maybe this would be Dickens' reaction.  or more likely the Muppets' one. Be that as it may, when the very idea of doing the things you enjoy becomes tainted by rage and outrage, maybe it's time to think again. 

There are many situations in the kind of work that I do that remind me of AYSO under-8 football--or soccer, if you insist. One of the hardest things to pass on to the kids is the need to think like a team: all of them want to be strikers, all of them run in a messy swarm towards the ball, there's no one in the defense, no one positioned to lead a new kind of attack, they can only see where the ball is, this second. Category Theory can feel exactly like that: an awful lot of mental energy gets dissipated in the competition for a few seconds of playing ball. This is not my style, it has never been.

By the way,  the picture has nothing to do with these darker thoughts. This was just a warm and fun conversation about "Proofs and Programs", part of the Logic Colloquium session organized by Monika Seisenberg. (my contributed presentation, which was only 20 min, was the same day for me, but the next day in Poland. funny to see the consequences of a round Earth in practical life!)

Congratulations to the Polish organizers of the Logic Colloquium! A huge challenge and they did it all extremely well. Thus I'm hoping to have hybrid versions of the Logic Colloquium henceforth!  I'm also looking forward to next year's Logic Colloquium in Reykjavik, Iceland!

Organizing work

is never easy! Since the office "opened" I've been trying to get there every Friday. 

Last Friday I went by BART to see if this is easier or not. Even going by car very early, it takes at least one hour and a bit to get there and more to come back. And the stress of driving these busy roads and bridges is palpable for someone like me who doesn't like to drive.

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.