[x] Change syntax for 𝓐𝓹 (@DreamLinuxer doesn't want it)
[x] in 2D/Frac.agda, I currently defined "left groupoid" and "right groupoid", corresponding to // and \ more closely. The symmetric definition worked, but was really not justified. I think these are easier to explain. If you agree, I can tweak section 3.5 accordingly. But that does give us left and right division groupoids, which will mean that Pi will need adapted. I don't think that will take too long.
[x] Proof sketch of lemma 7
[ ] In 4.1, remove all mention of information
[ ] In 4.1, // and \\ and # are not 'convenience'!
[ ] In 4.1, explain more deeply why we're influenced by compact closed categories (ccc from here on).
[ ] In 4.1, explain that we need to introduce fractions, so from ccc we go with generalizations of 1 = a/a, which then show up in 2 pairs.
[ ] in 4.1, explain that the ccc associativity A x (A x A) ~ (A x A) x A is not fine enough. In our situation, this shows up as #p x (q \ p) ~ (p // q) x #p. We call them 'synchr' from the effect they have in the operational semantics, even though these are induced by an associativity axiom. And not a commutativity axiom, even though that's what the syntax makes it look like!
[ ] In 4.1, try to hide all the parts of the definitions which have already been seen, to focus on just the new ones. And explain a lot.
[ ] in 4.2, introduce left and right-handed versions of 'division'. Use as appropriate in tangle.
[ ] in 4.2, explain that 'tangle' as a name is chosen because of the op.sem.
[ ] in 4.2, should prove a handed-version of lemmas at the end. And find a cleaner way to state them - the current way is quite ugly.
[ ] 5 should be split into sections (op.sem., properties, examples)
[ ] in 5.1, the definition of the action of synchr seems naive, but in the code I (JC) proved some structure lemma that says that this is the only choice. Comment.
[ ] in 5.1, there should be a lot more explanations throughout.
Change syntax for 𝓐𝓹 (@DreamLinuxer doesn't want it)