search

vikraman / 2DTypes

Collaborative work on reversible computing
17 stars 1 forks source link

Coxeter <-> MCoxeter #25

Closed inexxt closed 3 years ago

inexxt commented 3 years ago

Finished the proof of the equivalence in the title. Well, not really equivalence, but functions from and back - this is the relation we'll be truncating afterwards:

There are two functions in Coxeter.agda:

coxeter->mcoxeter : {m1 m2 : List} -> (m1 ~ m2) -> (m1 ≃ m2)
mcoxeter->coxeter : (m1 m2 : List) -> (m1 ≃ m2) -> (m1 ~ m2)

Coxeter is the true Coxeter relation, with cancel, swap and braid. MCoxeter is the my relation, with cancel, swap and long.

Fixes #15

vikraman commented 3 years ago

Functions back are forth are enough for equivalence since these will be props.