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?

[anshwad10]

Ah, I think I see the problem. All the lemmas you're using are fully polymorphic, but I think the only problem is that it uses paths instead of equivalences. So you could make another lemma called join-assoc-≃ and use the equivalence version of all the lemmas (use isoToEquiv 3x3-Iso instead of 3x3-lemma, and apply pathToEquiv to spanEquivToPushoutPath). Afterwards you could then turn it into join-assoc using univalence. This would definitely be better than messing with Lifts, and it would be more useful to have an equivalence version as well<\del>

[anshwad10]

Oh wait, joinAssocDirect already exists