Construct the quotient of List (Fin n) by the Coxeter relation - Githubissues

vikraman / 2DTypes

Collaborative work on reversible computing

17 stars 1 forks source link

Construct the quotient of List (Fin n) by the Coxeter relation #11

Closed vikraman closed 3 years ago

vikraman commented 3 years ago

This requires that the Coxeter relation:

[ ] is an equivalence
[ ] is prop valued (diamond lemma)

vikraman commented 3 years ago

This is in PiFin+/Coxeter/Equiv.agda but some things are marked as TODO.