Make join-assoc level-polymorphic

[ricky136973]

The original join-assoc in Cubical.HITs.Join assumes all types involved are of level 0. This restriction can be relaxed to only require the types being of the same level, not necessarily 0.

[anshwad10]

Why do they have to be the same level? why not generalize it more so that they can all be different levels

[ricky136973]

The original proof does not type check if I just simply assigning the types with different levels. I renamed it into join-assoc-samelevel and wrote a new join-assoc using the old one that supports different levels.

[anshwad10]

The original proof does not type check if I just simply assigning the types with different levels.

Why would that be? only reason I can think of is that the lemmas it was using (spanEquivToPushoutPath and 3x3-span.3x3-lemma) weren't level-polymorphic enough, but if thats the case why not generalize them too?