NOTE: Work is primarily done on this fork https://github.com/vcvpaiva/Dialectica
2022 AMS MRC on Applied Category Theory
-
basic categories
-
DialSet.agda = chapters 1 and 2 of https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-213.pdf over Set. This exists in two different styles:
A. objects as subsets of U \times X (we want to have the code, but will not do much with it to begin with) OR
B. objects as maps into Two, U\times X--> Two, which we will work on to begin with (thinking of L, but workign with Two) These two kinds are equivalent in the category Set. (later DialC, C any finite limit, CCC cat)
-
LDialSet.agda = chapters 3 and 4 of https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-213.pdf, over Set. Note the simplified morphisms, but much more complicated tensor products. (later LDialC, C any finite limit, CCC cat)
-
Lineales = poset reflection of an smcc (symmetric monoidal closed category) (to begin with Two, later Three, Four, Q, Z, R, [0,1])
-
*-autonomous posets = Girard algebras (possibly)= poset reflection of *-autonomous categories, full duality
-
Petri nets: Using two copies of DialSet and two relations pre, post: U\times X --> L or in the new notation pre, post: pos A\times dir A --> Two
-
Event structures (possibly, to make connection to Dialectica games, Winskel)
-
Poly = chapters 1,2, ... Not all, but following Nelson's suggestion we should do Dynamical Systems.
Dialectica Petri Nets https://arxiv.org/abs/2105.12801
Lineales https://drive.google.com/file/d/1Xk-2LKABGNfnYTf9CGV6lkhWBUHpGT9m/view?usp=sharing
Winskel's Dialectica games in "Making Concurrency Functional", https://arxiv.org/abs/2202.13910
https://github.com/heades/cut-fill-agda reimplementing in Cubical Agda