Zulip Chat Archive

Stream: PR reviews

Topic: 2720 torsors


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 18 2020 at 14:55):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 18 2020 at 15:04):

Maybe we should start using xml names

view this post on Zulip 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.

view this post on Zulip Scott Morrison (May 18 2020 at 15:08):

(Heptapod B?)


Last updated: May 06 2021 at 13:21 UTC