Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: Dialectica

Topic: Dialectica as $$\exists\forall$$ completion

Matteo Capucci (he/him) (May 12 2022 at 16:31):

Hi everyone,
I'm loving the paper @Valeria de Paiva pointed out re the question about dialectica being monadic over lenses that Bruno relayed in his last email! Such a pity Hofstra left us so untimely :(
Here's the paper: hofstra-dialectica.pdf
Later in the week I'll write more about why and how I think this is cool :)

Valeria de Paiva (May 12 2022 at 16:43):

Great @Matteo Capucci (he/him) ! I really think you guys should add here the note @Bruno Gavranovic wrote, as it will facilitate the conversation!

And in connection to Hofstra's work I'd like to also point out my work with Davide Trotta and Matteo Spadetto in the arxiv https://arxiv.org/abs/2104.14021 and https://arxiv.org/abs/2109.08064 as well as in MFCS2021 and LFCS2022 conferences, now submitted to journals. Note that we generalize the work of Hofstra to get the coproduct-product completion corresponding to the logical Dialectica.

Valeria de Paiva (May 12 2022 at 22:02):

and indeed, you're absolutely right!
Matteo Capucci (he/him) said:

Such a pity Hofstra left us so untimely :(

Such a shame indeed! :cry:

Matteo Capucci (he/him) (May 13 2022 at 09:00):

Ha, right, I know that paper of

Matteo Capucci (he/him) (May 13 2022 at 09:01):

yours!

Matteo Capucci (he/him) (May 13 2022 at 09:01):

Sometimes you know something but don't realize what it means for a while

Matteo Capucci (he/him) (May 13 2022 at 09:02):

Coproduct completions are something we studied here in Glasgow too in order to tackle the dependent optics problem

Matteo Capucci (he/him) (May 13 2022 at 09:02):

Very suspicious...

Valeria de Paiva (May 13 2022 at 13:32):

Thanks @Matteo Capucci (he/him) but the paper is much more Davide Trotta's and Matteo Spadetto's than mine.

Anyways, I recap what @Bruno Gavranovic wrote plus my replies. Bruno wrote:

#1 Dialectica seems to be a category of lenses with extra structure: objects are endowed with a relation and lenses are asked to preserve that. Does this make Dial a category of algebras of some monad on lenses?

#2 If dialectica categories are lenses with extra structura, and lenses are cartesian version of optics, can we use this insight to obtain "monoidal Dialectica categories", i.e. a category of optics with extra structure?

#3. In compositional game theory there is a notion of "selection functions" which interplay with the underlying lenses, telling us what the Nash equilibria of agents/players in a games are. Are winning conditions of Dialectica related to selection functions? Can we obtain one from the other?

I've replied:

for #1 there is a relevant paper by Pieter Hofstra, The Dialectica Monad and its cousins
Hofstra, P in Makkai Festschrifft, 2011 The dialectica monad and its cousins, Pieter J. W. Hofstra,
http://mysite.science.uottawa.ca/phofstra/dialectica.pdf
this is probably not the answer you want, but it is a kind of answer.

for #2 I have a version of Dialectica over an smcc (symmetric monoidal closed category) described in
"Dialectica and Chu constructions: cousins?", Theory and Applications of Categories, Vol. 17, No. 7, pp 127-152, 2006.
http://www.tac.mta.ca/tac/volumes/17/7/17-07abs.html.

But this is for the second kind of Dialectica categories (chapters 3 and 4 of my thesis).
one should be able to adapt it? I don't know.

for #3 the question I asked in our first meeting was related, but slightly different.
I asked if we simply added Hedges' notion of Nash equilibrium to Dialectica what we would get?
what does the notion of Nash equilibrium buy us?

I can also ask questions and my first question is about the real applications of lenses.

#4. What are the real applications of lenses? do we have a list showing best applications and what they use of the categorical structure?

#5 One can always generalize notions beyond their utility: this is why finding the right kind of abstraction for a type of problem is hard.
Sure we can do Dial_2 (CAT) or Dial_2 (Cat) instead of Dial_2 (Set), if you prefer. but unless this generalization buys me results that I don't have for Set, I'm not very interested. What can we do with lenses over Cat that I cannot do with usual lenses? what kind of structure I am preserving and why?

#6 the same idea applies to games with bidding: what can we do with these games? could we do it with dialectica spaces instead?
if yes, why do we want to do it? if not, why not?

I think it's important for the MRC that we have a healthy/long collection of questions to work over the week.

Valeria de Paiva (May 13 2022 at 13:36):

@Matteo Capucci (he/him) wrote

Sometimes you know something but don't realize what it means for a while

so true!

Valeria de Paiva (May 17 2022 at 03:14):

@Bruno Gavranovic wrote:

#1 Dialectica seems to be a category of lenses with extra structure: objects are endowed with a relation and lenses are asked to preserve that.

well, I assume we're talking about bimorphic lenses here.

So given an object of Dial(Set) $(U, X, \alpha)$ we can `forget' $\alpha$.
Then the domain and codomain of the morphism of Dial (Set), that is a map,
$(f, F)$, $f:U\to V$, $F:U\times Y\to X$ are like the domain and codomain of lenses morphisms.

So we have a functor ${\sf{forget}}: Dial_2(Set) \to Lenses$--where the lenses here are the bimorphic ones in Spivak's paper that Bruno suggested.

One neat thing that I have not seen written (but I have not read all the stuff in Bruno's directory) is that the conditions of the Dialectica category
maps force the Law Lenses to be true. This is a small proposition that can be proved (if I remember correctly) relatively easy.

So I think the lenses are not asked to preserve the structure: if the lenses come from a dialectica category then they preserve the relations naturally and this implies they satisfy the law lenses. so "Dialectica lenses" are somewhat better behaved.

Now instead of "forgetting" via a forgetful functor the third component of a dialectica object, you can forget the $\alpha$ component by mapping objects $U\times X$ to 1 the terminal object in the category Set (i.e any singleton). Now this gives you directly an object of the construction $Dial_1(Set)$ that I mentioned in my first message about the Dialectica for friends video, namely:

If we do Dial (Set) but have objects (U,X, alpha) mapping to 1, instead of 2, what happens to the structure defined in chapter 1 of the thesis?

So now we have two ways to take an object $(U, X, \alpha)$ to an object $(U,X)$, but they're different methods and maybe we end up in different categories. do we? any insights that we can extract from this situation?

Matteo Capucci (he/him) (May 17 2022 at 09:08):

Valeria de Paiva said:

One neat thing that I have not seen written (but I have not read all the stuff in Bruno's directory) is that the conditions of the Dialectica category
maps force the Law Lenses to be true. This is a small proposition that can be proved (if I remember correctly) relatively easy.

Uhm, I'm a bit puzzled by this. Lens laws are usually stated for monomorphic lenses, otherwise they do not make sense 'on the nose'. Can you clarify this point?

Valeria de Paiva (May 17 2022 at 12:59):

my bad, you're right. one needs to take the diagonal subcategory of Dial(Set) to do the calculations I mentioned.

Valeria de Paiva (May 17 2022 at 18:25):

And another "my bad" from today's MRC-meeting conversation:
I misremembered Sean's slides (https://topos.site/p-func-workshop/slides/Moss.pdf).
He says:

Cf. Lens ⊆ Poly and (in slide 12) Poly ≃ ΣΠ(1).

Moss is interested in the general properties of ΣΠ(C), which he calls the ‘polynomials in C’, is given by formally/freely adding sums
and products to the category C.

I'm interested in Dial ⊆ ΣΠ(2) as in his slide 26. He calls ΣΠ(2)= the dialectica polynomials, which seems a good name.