search

agda / cubical

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

Ganea's theorem #1055

Closed aljungstrom closed 11 months ago

aljungstrom commented 11 months ago

Pretty self-explanatory:-) The proof is rather explicit to make sure that things compute decently.

rwbarton commented 11 months ago

I didn't look at the details of the construction but the final statement looks perfectly suitable for our application. Thanks!

mortberg commented 11 months ago

I didn't look at the details of the construction but the final statement looks perfectly suitable for our application. Thanks!

Great, then I'll merge now!