search

agda / cubical

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

connectivity of the induced map between joins #963

Closed rwbarton closed 1 year ago

rwbarton commented 1 year ago

When B = Unit, this specializes (up to equivalences) to isConnectedSuspFun earlier in the same file. When A' = Unit, this is (again up to equivalences) the connectivity of the join of spaces. It is then (up to more equivalences) a special case of isConnected×̂, the connectivity of the pushout product. It might be desirable to unify these proofs, but I haven't tried to come up with a statement that would include all of them.

felixwellen commented 1 year ago

Thanks for the contribution and sorry for the long reaction time.

I usually don't look at homotopy theoretic things, but it should be in the right place and it still checks on latest master. Code also looks good to me, so I'll just merge it.