agda / cubical

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

Minor fix: improved definition of whitehead products #1155

Closed aljungstrom closed 2 months ago

aljungstrom commented 2 months ago

This PR i just a bit of refactoring. It removes and old (bad) version of the equivalence between joins of spheres Sⁿ * Sᵐ = Sⁿ⁺ᵐ⁺¹ and replaces every occurrence of it with a better one. This makes Whitehead products a bit more manageable. I've also made the simplified definition of Whitehead products the primary one.

Should be ready for merge directly.