Remove commutativity assumption to bigOpSplit++

agda / cubical

An experimental library for Cubical Agda

https://agda.github.io/cubical/Cubical.README.html

Other

446 stars 136 forks source link

Remove commutativity assumption to bigOpSplit++ #1045

Closed jpoiret closed 11 months ago

jpoiret commented 11 months ago

This is only needed for bigOpSplit.

felixwellen commented 11 months ago

Sorry - I just produces a conflict, since I moved those bigops from Rings to Semiring. I guess it would make sense to just move products in the same way.

jpoiret commented 11 months ago

That should solve the conflict, let's wait for CI