2720 torsors

Stream: PR reviews

[Yury G. Kudryashov]

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]

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

[Gabriel Ebner]

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]

Maybe we should start using xml names

[Scott Morrison]

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]

(Heptapod B?)