op and equations

Stream: Equational

[Kevin Buzzard]

The involution sending a magma to its opposite magma maps some equations to others (for example it fixes equations 1 to 3, and interchanges Equation4 and Equation5). Equation 8 is the first to not have a twin, which would be x = (x ∘ x) ∘ x. Similarly Equation42 seems to have no twin. This means that a symmetry in the picture is obscured (you can recover it by throwing away nodes whose dual is not a node). Adding dual equations means more work, but many proofs can be duplicated (because they are just an op of an existing proof). Note that Equation168 is self-dual. I guess for the associativity choices at the end you could weaken the variables in any order giving four more equations. Weakening y first (x ∘ (a ∘ z) = (x ∘ b) ∘ z) is self-dual and what might be a genuinely new thing. Weakening z is the dual of weakening x.