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.
Valeria de Paiva (May 30 2022 at 12:44):Proposition1.20. Poly has all products and coproducts and is completely distributive. Poly also has exponential objects, making it a bicartesian closed category. It therefore supports the simply typed lambda calculus.
Can you state a corresponding proposition for the dialectica categories and prove it with the material already at your disposal?
Valeria de Paiva (May 31 2022 at 21:32):my answer would be
Proposition1: LDial has all products and coproducts and is completely distributive. LDial also has exponential objects, making it a symmetric monoidal closed category. It therefore supports the simply typed linear lambda calculus.
Proposition2: Dial has all products and weak coproducts and is completely distributive. Dial also has exponential objects, making it a symmetric monoidal closed category. It therefore supports the simply typed linear lambda calculus.
Valeria de Paiva (May 31 2022 at 23:44):What is the dialectica corresponding proposition?
Valeria de Paiva (Jun 02 2022 at 17:26):Answering puzzle 2:
Proposition3. Beyond the cocartesian and cartesian monoidal structures (0,+) and (1, ×), the category LDial has two additional monoidal structures, denoted (I, ⊗) and (I, cross-product), which are together duoidal. Moreover ⊗ is a closed monoidal structure that distributes over coproducts.
(I don't know about connected limits)
Valeria de Paiva (Jun 02 2022 at 17:59):puzzle 4. the proposition corresponding to
Proposition 1.25. The category Comon(Poly) has finite coproducts and products, and
coproducts in Comon(Poly) agree with those in Cat.
Valeria de Paiva (Jun 03 2022 at 01:32):answering puzzle 3:
Proposition 4. The forgetful functor 𝑈 : Comon_\otimes(Dial) → Dial has a right adjoint
called the cofree comonoid construction. It is monoidal with respect to ⊗.
(this is the main theorem of chapter 2 of the thesis)
Valeria de Paiva (Jun 03 2022 at 03:02):extra puzzle: the Dialectica construction has a logical interpretation in terms of Godel's Dialectica interpretation, which provides a proof of consistency of arithmetic, a modified form of Hilbert's program. Can we find a logical interpretation of the polynomial construction?
Valeria de Paiva (Jun 03 2022 at 14:56):puzzle 5: What's the corresponding Dialectica proposition to
Proposition 1.28. For any polynomial 𝑝, the category Sys(𝑝) \cong [T𝑝 , Set]
of dynamical systems on 𝑝 forms a topos
Valeria de Paiva (Jun 03 2022 at 15:00):Answering puzzle 4:
Proposition 5. The category Comon(LDial) has finite coproducts and products.
Valeria de Paiva (Jun 03 2022 at 15:07):Writing the answers to the puzzles with the corresponding details would be a nice paper, as the area is very scattered and with very different notations. this could be one output of the whole Dialectica Team, what do you think?
it's not extremely exciting, as it is systematization of what's known--so a bit like covering one of the edges of Bruno's proposed cube.
but it will be useful for people writing their own subgroups papers and it will make easier the lives of people trying to get into the area
Valeria de Paiva (Jun 08 2022 at 19:51):Puzzle 5 is a little hard to answer, as in page 285 of the Poly book, theorem 7.53 we're told that the proof is based in "Beck’s monadicity theorem via a straightforward generalization of an argument given by Paré in [Par69, pp. 138-9], as pointed out by Porst in [Por19, Fact 3.1]." This seems on the face of it very generic and maybe we can have
Proposition 6. For any A in Dial, the category Sys(A) \cong [T_A , Set]
but I am not sure.