## Stream: PR reviews

### Topic: 2720 torsors

#### Yury G. Kudryashov (May 18 2020 at 14:54):

It seems that #2720 uses a non-standard naming convention for lemmas listing operations top-to-bottom of the syntax tree, not left-to-right. I was going to suggest renaming the lemmas but realized then with our current naming scheme the axioms

(vadd_vsub : ∀ (p1 p2 : P), p1 +ᵥ (p2 -ᵥ p1 : V) = p2)
(vsub_vadd : ∀ (p : P) (v : V), p +ᵥ v -ᵥ p = v)


should get the same name.

#### Kevin Buzzard (May 18 2020 at 14:55):

Maybe one just puts a ' on the one with the brackets?

#### Gabriel Ebner (May 18 2020 at 15:00):

Any naming strategy based on a tree traversal order will have ambiguities. You've listed one for in-order traversal, for pre-order consider (a - b) + c vs. a + (b - c) which would both get the name add_sub.

#### Kevin Buzzard (May 18 2020 at 15:04):

Maybe we should start using xml names

#### Scott Morrison (May 18 2020 at 15:08):

Maybe (just trying to provoke Patrick here :-) we should move beyond this primitive 1-categorical idea of linear names, and typeset higher-dimensional string diagrams showing the compositional structure of the name.

#### Scott Morrison (May 18 2020 at 15:08):

(Heptapod B?)

Last updated: May 06 2021 at 13:21 UTC