With the notation conventions from em-convex, there are 3 pairs of torsor rewrites. A torsor, figured by a fat circle here, is a term of type
with the rewrites:
Finally, there is a third pair of rewrites which involve terms of the form for
The rewrite T3-1 tells that the torsor is a propagator for , the rewrite T3-2 is an apparently weird form of a DIST rewrite.
Now, the following happen:
- if you add the torsor rewrites to em-convex then you get a theory of topological groups which have a usual, commutative smooth structure, such that the numbers from em-convex give the structure of 1-parameter groups
- if you add the torsor rewrites to em, but without the convex rewrite then you get a more general theory, which is not based on 1-parameter groups, because the numbers from em-convex give a structure more general
- if you look at the emergent structure from em without convex, then you can define torsor terms whch satisfy the axioms, but of course there is no em-convex axiom.
Lots of fun, this will be explained in em-torsor soon.