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 06 2022 at 18:57):Dear MRC-Dialectica participants, @Nelson Niu will talk this Tuesday at 8 am (Pacific time) about the connections between Dialectica constructions and Polynomials--or rather about the connections between Poly and Dialectica. You should've received a handout by email.
please let me and @Jérémie Koenig know if you cannot make it.
Once again, please have questions! And please let us know in which subgroup you are *tentatively associating yourself with.
Joseph Dorta (May 09 2022 at 20:58):@Valeria de Paiva @Jérémie Koenig @Nelson Niu
May I formally express interest in this topic, in particular questions 2.1.2, 2.1.8, and 2.1.13
Valeria de Paiva (May 09 2022 at 21:23):Hi, @Joseph Dorta you can certainly express interest in the topics, as you have, thank you for committing to a problem area! and more thanks to @Nelson Niu for presenting the problems in such a clear form. but how the work will (or not) progress is not guaranteed, right?
we will record the chat tomorrow and post it for the group, right @Jérémie Koenig ?
Eric Bond (May 10 2022 at 15:05):I was looking at your notes this morning Nelson. Playing around with the definitions of the objects in Agda.
record Poly : Set where
constructor _▹_
field
pos : Set
dir : pos -> Set
record DC : Set where
field
pos : Set
dir : pos -> Set
pred : ∀(i : pos)(a : dir i) → Two
record Dial (L : Set){{_ : Lineale L}} : Set where
field
pos : Set
dir : pos -> Set
pred : ∀(i : pos)(a : dir i) → L
This style of definition is the Container/Polynomial definition that is nice to work with in Agda (see here).
I had not thought about this type of encoding and I'd like to explore this more. Could have interesting applications.
I also started a "direct" encoding of Dialectica here
Valeria de Paiva (May 10 2022 at 18:56):Thanks @Nelson Niu for a great presentation!
Valeria de Paiva (May 10 2022 at 20:48):This is just to make sure that @Colin Bloomfield sees this stream! (myself I missed it again, had to go to recent topics to find it)
Valeria de Paiva (May 10 2022 at 20:51):Did anyone at the meeting today saved the chat? I wanted to do a summary, including the chat.
Jonathan Weinberger (May 10 2022 at 20:57):I did, up until the very end I think. Where should I put it @Valeria de Paiva ?
Jonathan Weinberger (May 10 2022 at 21:30):@Valeria de Paiva you've got :mail:
Valeria de Paiva (May 10 2022 at 22:27):@Eric Bond I don't think this Agda code is completely correct. but this is possibly an interesting "story"
the second block of code does not work for me.
record DC : Set where
field
pos : Set
dir : pos -> Set
pred : ∀(i : pos)(a : dir i) → Two
If one does a "dependent Dialectica" like the above, we have a problem.
Because this subcategory is not closed under morphisms! i.e it's not a subcategory.
The Dialectica category would have (using the notation above) objects
(pos, dir, pred) and (pos', dir', pred'), where dir=X^pos and X is a generic set and similarly
dir'= X'^pos'.
A dialectica morphism would map pos-> pos', but it would not know how to deal with the second coordinate, because
pos\times dir'=(X')^{pos'} == pos\times pos'\to dir' but then I cannot see a natural map into dir.
Don't know how clear this is, but the point is that Dial objects are not of the form (U, X^U, pred), they're generically (U,X, pred), any X, I cannot force the second coordinate to be of the form X^U. (or maybe I can, but I don't see this immediately. I can see a map using two evaluations plus projections, but don't see why it would satisfy the dialectica condition on the predicates.)
Valeria de Paiva (May 11 2022 at 02:03):Many thanks @Jonathan Weinberger !
Valeria de Paiva (May 11 2022 at 17:53):hi @Colin Bloomfield ! great to hear from you. Thanks!!
Valeria de Paiva (May 13 2022 at 17:03):Thanks for the code in the here link, @Eric Bond !
(I hadn't noticed it before!)
Carrying on comparing to Dialectica, you say in lines 57--61
--tensor \ox
-- Ayᴮ × Cyᴰ = ACyᴮᴰ
_⊗ₚ_ : Poly → Poly → Poly
p ⊗ₚ q = record { pos = pos p × pos q ; dir = λ {(i , j) → (dir p) i × (dir q) j} }
-- show these are all monoidal structures on poly
This tensor product structure is described for Dial_2(Set) in the thesis chapter 1.
Nelson Niu (May 18 2022 at 05:04):Hi everyone (but mostly the Poly group, for now @Joseph Dorta @Samantha Jarvis)!
Just wanted to share the most recent version of the Dialectica & Poly handout here. I added a little more to it today to round out the "Comparison" section, and I'll be filling in the rest over the next few days (while also continuing to fill in the Poly book...).
Speaking of the Poly book, you'd usually be able to find it at https://topos.site/poly-book.pdf, which is how I've linked it in the handout as well, but the online version seems to be down right now. I'm trying to get that fixed, but for now you can find the most recent version here (thanks @Abdullah Malik for uploading it the first time!).
EDIT: The book is back online! (many thanks to the inimitable Tim Hosgood)
Finally, for the two references Valeria asked for, I intended the handout to be the main thing you'd need to read, but I'd recommend David Spivak's Poly for dynamical systems primer and Sean Moss's hour-long talk (slides here) as well.
Thanks, and see you all soon!
Valeria de Paiva (May 18 2022 at 20:30):Awesome handout @Nelson Niu! and thanks for the two references, i.e for pointing out to David Spivak's Poly for dynamical systems primer as well as Sean Moss talk.
Eric Bond (May 27 2022 at 00:49):-- "non dependent Poly with a relation"?
record LDialSet {ℓ : Level}{ L : Set ℓ}{{ _ : Lineale L}} : Set (lsuc ℓ) where
constructor ⟨_,_,_⟩
field
pos : Set ℓ
dir : Set ℓ
α : pos → dir → L
-- Poly is "dependent Dialectica without a relation"?
record Poly {ℓ : Level} : Set (lsuc ℓ) where
field
pos : Set ℓ
dir : pos → Set ℓ
-- so what is ..? Dependent Dialectica with a relation?
record LDepDialSet {ℓ : Level}{ L : Set ℓ}{{ _ : Lineale L}} : Set (lsuc ℓ) where
field
pos : Set ℓ
dir : pos → Set ℓ
α : (p : pos) → dir p → L
Well, Eric I do not think this Dependent Dialectica with a relation works.
I don't know how the composition works to preserve the relation. but maybe I have not tried hard enough.
Nelson Niu (May 27 2022 at 16:08):It should work; this is just \sum\prod 2 (or L instead of 2) from Sean Moss’s talk
Nelson Niu (May 27 2022 at 16:09):I don’t think the dependence changes how the relation works too much, just the signatures of the backward functions slightly
Valeria de Paiva (May 27 2022 at 16:48):It should work; this is just \sum\prod 2 (or L instead of 2) from Sean Moss’s talk
well, if we want to call \sum\prod 2 Dialectica then maybe. but there is a difference between \sum\prod 2 and Dialectica, because there is no cartesian closed structure in Dialectica and no coproducts, only weak ones. so \sum\pro 2 is a generalization of dialectica, not Dialectica as originally considered.
Nelson Niu (May 27 2022 at 19:55):Yes, it’s different, which is why Sean Moss called it dependent dialectica instead of just dialectica I believe! And this is the same difference between Jules Hedges category of bimorphic lenses versus Poly, whose morphisms are “dependent” lenses
Valeria de Paiva (May 27 2022 at 21:42):And this is the same difference between Jules Hedges category of bimorphic lenses
well, I don't know much about Hedges category(I should), but I thought the adjective "dependent" had to do with one of the sets being an index set (so minimal structure) while the other set is like a space, plenty of structure. and in the case of Poly this space this full of structure set I thought was supposed to be or . but the issue with this class is that it's not closed under the monoidal structures we want to check in Dial or the internal-hom. so logically it seems a strange situation.
Now reversing tables @Nelson Niu , I have not seen in the Poly handout a discussion of the tensor product of GC, which I believe is also duoidal with .
this "cross-product" tensor takes and to
(pos A × pos B, (dir A)^{pos B} × (dir B)^{pos A}, evals)
Was that there?
Eric Bond (May 27 2022 at 22:06):EDIT:
moved the code snippet to here.
I did get composition to hold.
(Apologies for the sloppy code. it was jotted down quickly and ill clean it up)
https://gist.github.com/bond15/59582ea8a74e75a71764690d85137344
Valeria de Paiva (May 27 2022 at 22:23):cool. but
"non dependent Poly with a relation"
is exactly DialSet, right? why call it non-dependent Poly with a relation?
and
LDepDialSet
is exactly the subcategory of GSet with the second coordinate of the form pos A -> dir A
(*)
my issue above is that I don't think this subcategory is closed under the operations in GSet. I don't think I can restrict the operations I'm interested in
$$ \otimes, &, \oplus, [-,-] $$
to this subcategory. while Eric and Nelson think there's no problem. So I'll be happier if they're right, but cannot see it at the moment, bc the bifunctors exist in the large category, but they don't restrict to the small one. unless I am wrong about (*) or about the fact that the results of the bifunctors don't have the appropriate shape.
Eric Bond (May 28 2022 at 00:02):Still processing the posts above.
I'm a bit confused about.
LDepDialSet is exactly the subcategory of GSet with the second coordinate of the form posA→dirA , right? (*)
LDepDialSet objects would be of the form (pos A : Set , dir A : pos A -> Set, alpha)
so dir A is a pos A indexed family of sets.
Valeria de Paiva (May 28 2022 at 00:10):I see now, the question is whether your target is dir A : pos A -> Set or dir A: pos A-> dir A. I'm thinking too.
Eric Bond (May 28 2022 at 00:19):The composition holds using dirA : posA -> Set and its essentially the same as the composition in DSet2.
compare
https://github.com/vcvpaiva/Dialectica/blob/3634872482683a0be2c00337f29db623b656d49b/TwoDialSet.agda#L152
and
https://github.com/vcvpaiva/Dialectica/blob/3634872482683a0be2c00337f29db623b656d49b/LDDialSet.agda#L53
Eric Bond (May 28 2022 at 00:22):( I can switch to using Latex instead of Agda in these messages if that would be preferred and more broadly readable)
The trick is using f in the type level.
Eric Bond (May 28 2022 at 00:30):Don't have an answer about the desired structure (the tensor, internal hom,..)
Valeria de Paiva (May 28 2022 at 15:47):Don't have an answer about the desired structure (the tensor, internal hom,..)
well, we need to do the walking, before the running, right? we need to add the structure of DialSet to the agda file.
Valeria de Paiva (May 28 2022 at 18:02):Eric Bond said:
( I can switch to using Latex instead of Agda in these messages if that would be preferred and more broadly readable)
The trick is usingfin the type level.
Either latex or agda works, @Eric Bond . The issue here is the type of the objects, not how we write them. so
where is an object of DialSet (or GSet ) is one possible way to instantiate
(pos A : Set , dir A : pos A -> Set, alpha). But the latter is more generic.
So I 'd like to have the agda code for DialSet and LDialSet and their structures and theorems proved, before attacking the problem of the dependent version. As for that we have to read Tamara von Glehn and Sean Moss' theses, right?
Valeria de Paiva (May 28 2022 at 19:00):@Eric Bond in line 55 of https://github.com/vcvpaiva/Dialectica/blob/3634872482683a0be2c00337f29db623b656d49b/TwoDialSet.agda#L152 you have what I think is the correct notion of bifunctoriality of tensor in L. is this an agda proof or an agda definition?
also is (line 170)
record DialSet⊗ (A B : DialSet) : Set where
field
pos A⊗B : pos A × pos B
dir A⊗B : dir A × dir B
α : (pos A × pos B) → (dir A × dir B) → α(u,x) ⊗² β(v,y)
a sensible definition for the tensor in agda?
I also need to know how to define constants in agda, because I need four constants:
Valeria de Paiva (Jun 02 2022 at 01:37):@Nelson Niu nice to hear your group is working with factorizations! do you have a special motivation for that?
and can you tell me what do you think is special about
(Ahman-Uustalu, 2018). Comonoids in (Poly, y, ◁) are categories.
what did Danel and Tarmo wanted this theorem for?
Nelson Niu (Jun 02 2022 at 01:43):Factorization helps to isolate the properties of what’s happening on positions vs. what’s happening on directions. For example, we found yesterday that there is a canonical map from the cross product (where there is codependency in the directions, but not the positions) to the composition product (where there is dependency in the positions, but not the directions) that factors through the parallel product (where there is no dependency in either). So in some sense the parallel product can be defined in terms of these other products, and arises naturally from vertical/cartesian factorization
Nelson Niu (Jun 02 2022 at 01:50):I’m not sure what the theorem was initially intended for, but what I like about it is that it puts systems that can be expressed in Poly in a familiar context. Comonoids arise naturally when you want to talk about cycling through systems repeatedly—passing back and forth through a lens more than just one round trip. They give you a way to think of directions as actually pointing to the next position, and a way to run through several directions coherently. The coherence conditions seem foreign until you realize they really act just like categories: directions lead from one position to another and compose unitally and associatively. Coming up with examples of a comonoid, or checking whether something is a comonoid, then becomes really easy—you know how to do it already if you know how to check if something is a category.
Valeria de Paiva (Jun 02 2022 at 01:50):Yes, there's also a natural map from the cross product to the cartesian product, which factors the parallel product. this should be the other duoidal structure I mentioned to you.
EDIT: the duoidal structure I'm mentioning here should be between the cross product and the parallel tensor, I wrote about that in 1996 in the paper https://www.academia.edu/674289/A_dialectica_model_of_state and at that state discussed the interchange law, before the duoidal stuff was so christened.
Nelson Niu (Jun 02 2022 at 01:50):(Also, there’s a nice double category that puts categories, functors, and cofunctor on the same footing, but I haven’t really investigated that thoroughly yet)
Nelson Niu (Jun 02 2022 at 01:51):Oh yes, every monoidal structure is duoidal with the cartesian product just because of its universal property
Nelson Niu (Jun 02 2022 at 01:54):We worked out today that tri-comonoids in SigmaPi(C^op) for general monoidal categories C correspond to SigmaC-enriched categories
Valeria de Paiva (Jun 02 2022 at 02:01):Thanks also for the motivation for the Ahman-Uustalu result!
Valeria de Paiva (Jun 02 2022 at 02:04):I had also started an overleaf on the double category, but I was doing it for Dial, only, and I didn't know whether the squares were there or not.
Nelson Niu (Jun 02 2022 at 02:05):Yeah, I’m not sure either
Valeria de Paiva (Jun 02 2022 at 13:42):Comonoids arise naturally when you want to talk about cycling through systems repeatedly—passing back and forth through a lens more than just one round trip.
Comonoids are even more natural in the setting of Linear Logic where they're exactly what you're trying to get, your goal, so that you have linear and non-linear types interacting. But thinking of them as categories doesn't seem obvious to me.
Nelson Niu (Jun 02 2022 at 14:25):@Valeria de Paiva You know how otimes-comonoids, the one in Ch. 2 of your thesis, are monoids in Set indexed over some other set, along with some assignment of True/False for each monoid element that respects the monoid structure?
Well, you can think of an indexed set of monoids as a slightly boring category, where every object “keeps to itself”—the only morphisms start and end at the same object (and the True/False part picks a wide subcategory, a submonoid of each monoid). So the data of the category can be captured just by a bunch of monoids: one for each object, the endomorphims on that object. Then tri-comonoids generalize this by allowing morphisms between different objects, which becomes a category
Valeria de Paiva (Jun 02 2022 at 14:30):well, in my thesis they're monoids in a mythical category C with finite limits, not exactly Set. where do the 'tri ' in tricomonoids comes from?
Nelson Niu (Jun 02 2022 at 14:30):Oh yes, I’m taking C = Set
Nelson Niu (Jun 02 2022 at 14:30):tri is the triangle, the composition product
Nelson Niu (Jun 02 2022 at 14:31):Sorry I realize that’s misleading, there’s not much to do with 3
Valeria de Paiva (Jun 02 2022 at 14:44):great, thanks @Nelson Niu !
I also have a small problem with the notions of mono and epi. You've hinted at it already: In the subcategory GSet =LDial we can say that (f,F) or $$(\phi, \phi^#)$$ is mono iff f is mono and F is epi. Also, (f,F) is epi if f is epi and F is mono, bc the category is symmetric. But in Dial this is blurred, bc of the dependence of F in A. how are you dealing with this?
Nelson Niu (Jun 02 2022 at 15:19):Yeah, it’s a little tricky: in Poly, a mono has to be a mono on positions, and an epi has to be an epi on positions. The dependence backward on directions is where things get a little hairy, but it’s still manageable:
Nelson Niu (Jun 02 2022 at 15:38):You can think of the backward part of (I, A) -> (J, B), in two ways: either as a function B -> A for every element of I, or (a little less intuitively) as a function B -> A^{f^-1 j} for every element j of J.
Nelson Niu (Jun 02 2022 at 15:39):Then a mono in Poly is a mono on positions and every B -> A is an epi on directions; and an epi in Poly is an epi on positions and every B -> A^{f^-1 j} is a mono on directions.
Nelson Niu (Jun 02 2022 at 15:39):(Limits and colimits can be interpreted analogously)
Valeria de Paiva (Jun 02 2022 at 15:50):but then
Then a mono in Poly is a mono on positions and every B -> A is an epi on directions; and an epi in Poly is an epi on positions and every B -> A^{f^-1 j} is a mono on directions.
this is exactly what I wrote for LDial:
(f,F) is mono iff f is mono and F is epi. Also, (f,F) is epi iff f is epi and F is mono
Valeria de Paiva (Jun 02 2022 at 17:13):@Nelson Niu I asked Danel Ahman and Tarmo my question.
I’m not sure what the theorem was initially intended for, but what I like about it is that it puts systems that can be expressed in Poly in a familiar context.
Danel says:
We observed it in the MFPS 2016 paper
"Directed Containers as Categories" (https://danel.ahman.ee/papers/msfp16.pdf).
From what I remember, the motivations were:
I had been talking about directed containers feeling like some form of state machines,
and the correspondence with categories made that feeling evident.
In the above paper the correspondence allows us to view constructions on containers
from the viewpoint of categories, showing that there is something canonical and natural
about them (e.g., that the bidirected containers correspond to groupoids).
It turns out that there is a general decomposition operation [1] on directed
container (and corresponding comonad) morphisms that is analogous to
the full image factorisation [2] of functors between categories (in the case
of directed containers, we have a factorisation of cofunctors). Under some
mild assumptions one can then also perform this kind of decomposition for
general comonad morphisms (also in [1]).
[1] Ahman, Uustalu: Decomposing Comonad Morphisms (https://drops.dagstuhl.de/opus/volltexte/2019/11442/pdf/LIPIcs-CALCO-2019-14.pdf)
[2] https://ncatlab.org/nlab/show/full+image
=====
So similar intuitions as yours @Nelson Niu .
Nelson Niu (Jun 02 2022 at 17:40):@Valeria de Paiva Yeah, the epi mono characterization is similar, but not exactly the same—which is not surprising, because there is an adjunction between GSet and SigmaPi2 (or just DialSet)
Valeria de Paiva (Jun 02 2022 at 17:57):cool, I hope you're writing it down too. as I don't know this one.
I know that GSet=LDial is included in DIal (which is Dial_2Set). Now SigmaPi2 is defined via the completions right? then I don't know that SigmaPi2 is the same as DialSet. a proof would be very welcome