connectivity of the induced map between joins

[rwbarton]

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]

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.