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 for Friends video

Valeria de Paiva (Apr 29 2022 at 19:01):

I thought it might be easier if people could write down questions they had about the video that I've posted in the MRC wiki here.

I still have several questions myself, but I thought it would be nice to see the things that were not clear to you!
So to get the ball rolling let me ask two questions:

1. Can we do Dial (Cat) instead of Dial (Set) ?
2. If we do Dial (Set) but have objects (U,X, alpha) mapping to 1, instead of 2, what happens to the structure I described in chapter 1 of https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-213.pdf?

Valeria de Paiva (May 01 2022 at 04:35):

More questions:

3. Tim Hosgood wanted to know if people had worked out other dialectica categories that were not over Sets. In particular he wanted to know about categories of spaces—but see https://ncatlab.org/nlab/show/nice+category+of+spaces. Nice categories of spaces are rare. if one likes topology one might want to do the Dialectica construction over "sequential topological spaces" (https://ncatlab.org/nlab/show/sequential+topological+space)--a "nice" category of spaces described by Escardo in the Topos Colloquium this week.
4. Dialectica objects have a mapping from a double object into a simplified category, a lineale, L. So we can write it as Dial_L(C) and we can vary both C and L and how they interact. The (minor) generalization I've done is described in the preprint Categorical Multirelations, Linear Logic and Petri Nets, which was not published, but it was explored a little in the paper with Elena di Lavore and Wilmer Leal on Dialectica Petri Nets. Relationships to "dynamical systems" have not been studied: is there anything interesting to say here?

Valeria de Paiva (May 03 2022 at 18:34):

hi all,

we had our first contents meeting of the MRC-Dialectica group today.

It started well, with Charlotte asking "what are the motivations for the dialectica construction?"
Motivations are always hard to share, but we had a beginning of a conversation about left-handed-side of an object proves things, right-handed-side provides counter-examples: this is where the bidirectionality of the Dialectica construction comes from.

We have a schedule for subgroups in the 4 weeks, along the lines of:

1. Dialectica and Games -- Jeremie Koenig leading (was today at 8 am Pacific time)
   Valeria recommends Jeremie's talk at the ACT2021 and Glynn Winskel talk at Topos Colloquium

   
   

2. Dialectica and Poly -- Nelson Niu leading (next week)

3. Dialectica and Lenses -- Bruno Gravanovic+Matteo Capucci leading (see some above)

4. Dialectica implementations -- Eric Bond leading

but this is all subject to confirmation on email, shortly, we hope.

NOTE: Everyone in the group is supposed to try to sort themselves into one of the subgroups, tentatively.
Or to propose another subgroup, if they feel this is most appropriate.

Questions here or by email to the whole group are highly appreciated: this is how we make progress.

Valeria de Paiva (May 03 2022 at 20:09):

Complementing my message above:

1. we also discussed the difference between tensor products and cartesian products in the original Dialectica categories.

Tensor product of A=(U, X, alpha) and B= (V, Y, beta) is A\otimesB= (U\times V, X\times Y, alpha\times\beta), while the cartesian product
is A&B=(U\times V, X+ Y, choose(alpha,\beta)).
the tensor product is the multiplicative conjunction, while the cartesian product is the additive conjunction. Hence A&B has projections and diagonals, while A\otimes B has neither.

2. I thought it would be very helpful if people tried to prove the theorem in slide 5 of this, as they would appreciate better CT's ability to hide many calculations behind sleek diagrams.

3. Please ask questions if the proof of Theorem 1 does not make sense to you, we want to generalize it. a lot.

Colin Bloomfield (May 13 2022 at 16:57):

Now that I have a little more time, I wanted to start getting my hands dirty with Dialectica Categories and work through your suggested homework. Not counting the intro slide, I am still on slide 4, proving DC is a category with extra structure. I proved DC is a category, but I suspect I am sweating more than I should. For example, to show the composition of two morphisms in DC is well defined, I couldn't figure it out visually. Essentially, I proved it pointwise for D(Set) then rewrote the argument via pullbacks of subsets and then realized that products and pullbacks allow this argument to go through more generally on subobjects. I am curious if there is a more visual approach as you mention "pullback patching," in your thesis? Now I am on proving that DC has tensor products and my head is really hurting! :joy: I suspect I can am not approaching these arguments at the right level of abstraction as I grind through equationally and use particular representations of products.

Lastly, I was wondering if you think it would be a good idea to have a section Dialectica Basics, or something where non-research work on the fundamentals could be shared and discussed? I think I would benefit from peaking at other participants solutions to your homework! :)

Valeria de Paiva (May 13 2022 at 17:35):

well @Colin Bloomfield

to show the composition of two morphisms in DC is well defined, I couldn't figure it out visually

I cannot figure these things visually either.

I am curious if there is a more visual approach as you mention "pullback patching," in your thesis?

I just meant that you can go gluing pullback squares, nothing more fancy. (but I have Australian friends who can do much fancier gluing of squares!)

Personally, I also use particular representations of products, and it's a pain, I agree. But I'm very glad you're really trying to do the calculations, as they may look easy when presented in a slide, but getting there is not that easy.

This is why I changed my calculations in chapter 3 and 4 to be about maps into 2 (or the lineale $L$ later on).

However, you can also use the internal language:
So $(f,F):A\to B$ iff for all $u\in U,y\in Y$, $u\alpha F(u,y) \rightarrow f(u) \beta y$ and
$(g,G):B\to C$ iff for all $v\in V,z\in Z$, $(v\beta G(v,z)) \rightarrow (g(v) \gamma z)$, implies that
$(f,F);(g,G)= (f;g, comp:U\times Z\to X)$ iff for all $u\in U,z\in Z$, we have that
$(u\alpha(comp(u,z)) \rightarrow ((f;g)u) \gamma z$.
and showing this is much easier for a logician, right?

of course you have to rewrite the long composition and substitute it in $comp:U\times Z\to X$.

Valeria de Paiva (May 19 2022 at 00:11):

@Colin Bloomfield I was thinking about your point:

Lastly, I was wondering if you think it would be a good idea to have a section Dialectica Basics, or something where non-research work on the fundamentals could be shared and discussed?

I think this is a good idea. I especially think that you may enjoy helping to write down the file lineale.agda, as it's purely algebraic logic, so your style. so I'm suggesting that we write together the mathematics and you and @Eric make sure that the thing runs in agda.
and then maybe we can think about how algebraic logic of this substructural-style fits in your conception of algebraic logics.

The thing would be to have a look at:

Lineales: algebras and categories in the semantics of Linear Logic. Presented at LLC8, Stanford, May 1999. Revised version appears in CSLI book "Words, Proofs, and Diagrams" (eds. D. Barker-Plummer, D. Beaver, Johan van Benthem and P. Scotto di Luzio), 2002 Official version: (https://drive.google.com/file/d/1Xk-2LKABGNfnYTf9CGV6lkhWBUHpGT9m/view?usp=sharing). Original version Lineales: Algebraic Models of Linear Logic from a Categorical Perspective, https://drive.google.com/file/d/11BMFAOhACYHa7asGf5i2DuRywWQjSmp1/view?usp=sharing.

You could have a look and then let me know if this helps or not.