search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
454 stars 139 forks source link

Graded commutativity of cup product #938

Closed aljungstrom closed 2 years ago

aljungstrom commented 2 years ago

This PR contains graded commutativity for the various versions of the cup product in the library. The main result (or, at least, the most general one) is the final theorem in Homotopy.EilenbergMacLane.GradedCommTensor. The proof itself is (beautiful in theory but in practice) a massive mess of transports and congs. It should be read by no one.

This means some ad hoc solutions in Cohomology/Rings can be removed, but I'll leave this for a future PR.

aljungstrom commented 2 years ago

@mortberg should be done now