Lifting relation on Fin to Fin + Fin

[inexxt]

We write that

The general observation is: If we have a group structure on (List(A), <~*~>) (with multiplication given by ++, inverse given by reverse), then we can lift it uniquely to a group structure on (List(A + A), <<~*~>>), in the following way:

codiag : A + A → A
map codiag : List(A + A) → List(A)
w1 <<~*~>> w2 := map codiag w1 <~*~> map codiag w2
This is in the formalisation (see Coxeter/GeneratedGroupGeneralised.agda), and we will highlight this result.