search

vikraman / 2DTypes

Collaborative work on reversible computing
17 stars 1 forks source link

Lifting relation on Fin to Fin + Fin #142

Closed inexxt closed 2 years ago

inexxt commented 3 years ago

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.