diff --git a/Cubical/HITs/Join/Properties.agda b/Cubical/HITs/Join/Properties.agda
index c2a9c1bcb..9d0f437be 100644
--- a/Cubical/HITs/Join/Properties.agda
+++ b/Cubical/HITs/Join/Properties.agda
@@ -19,6 +19,7 @@ module Cubical.HITs.Join.Properties where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
 open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Path
@@ -99,8 +100,8 @@ joinPushout≡join A B = isoToPath (joinPushout-iso-join A B)
 {-
   Proof of associativity of the join
 -}
-join-assoc : (A B C : Type₀) → join (join A B) C ≡ join A (join B C)
-join-assoc A B C = (joinPushout≡join (join A B) C) ⁻¹
+join-assoc-samelevel : (A B C : Type ℓ) → join (join A B) C ≡ join A (join B C)
+join-assoc-samelevel {ℓ} A B C = (joinPushout≡join (join A B) C) ⁻¹
                    ∙ (spanEquivToPushoutPath sp3≃sp4) ⁻¹
                    ∙ (3x3-span.3x3-lemma span) ⁻¹
                    ∙ (spanEquivToPushoutPath sp1≃sp2)
@@ -163,7 +164,7 @@ join-assoc A B C = (joinPushout≡join (join A B) C) ⁻¹
       H1 = H1;
       H3 = H2 }
       where
-        A×join : Type₀
+        A×join : Type ℓ
         A×join = A × (join B C)
 
         A□2→A×join : 3x3-span.A□2 span → A×join
@@ -245,7 +246,7 @@ join-assoc A B C = (joinPushout≡join (join A B) C) ⁻¹
       H1 = H4;
       H3 = H3 }
       where
-        join×C : Type₀
+        join×C : Type ℓ
         join×C = (join A B) × C
 
         A2□→join×C : 3x3-span.A2□ span → join×C
@@ -300,6 +301,41 @@ join-assoc A B C = (joinPushout≡join (join A B) C) ⁻¹
         H4 (inr (b , c)) = refl
         H4 (push (a , (b , c)) i) j = fst (joinPushout≃join _ _) (doubleCompPath-filler refl (λ i → push (a , b) i) refl j i)
 
+join-assoc : ∀ {ℓ''} (A : Type ℓ) (B : Type ℓ') (C : Type ℓ'') → join (join A B) C ≡ join A (join B C)
+join-assoc {ℓ} {ℓ'} {ℓ''} A B C =
+  LiftExt {ℓ' = ℓ-max (ℓ-max ℓ ℓ') ℓ''} (join-lift ⁻¹
+                                        ∙ cong₂ join join-lift refl ⁻¹
+                                        ∙ join-assoc-samelevel (Lift A) (Lift B) (Lift C)
+                                        ∙ cong₂ join refl join-lift
+                                        ∙ join-lift)
+  where
+    join-lift : ∀ {ℓ ℓ' ℓ-out} {A : Type ℓ} {B : Type ℓ'} →
+      join (Lift {j = ℓ-out} A) (Lift {j = ℓ-out} B) ≡ Lift {j = ℓ-out} (join A B)
+    join-lift {ℓ-out = ℓ-out} {A = A} {B = B} = isoToPath (iso f g fg gf)
+      where
+        f : join (Lift {j = ℓ-out} A) (Lift {j = ℓ-out} B) → Lift {j = ℓ-out} (join A B)
+        f (inl (lift x)) = lift (inl x)
+        f (inr (lift x)) = lift (inr x)
+        f (push (lift a) (lift b) i) = lift (push a b i)
+
+        g : Lift {j = ℓ-out} (join A B) → join (Lift {j = ℓ-out} A) (Lift {j = ℓ-out} B)
+        g (lift (inl x)) = inl (lift x)
+        g (lift (inr x)) = inr (lift x)
+        g (lift (push a b i)) = push (lift a) (lift b) i
+
+        fg : ∀ x → f (g x) ≡ x
+        fg (lift (inl x)) = refl
+        fg (lift (inr x)) = refl
+        fg (lift (push a b i)) = refl
+
+        gf : ∀ x → g (f x) ≡ x
+        gf (inl (lift x)) = refl
+        gf (inr (lift x)) = refl
+        gf (push (lift a) (lift b) i) = refl
+
+    LiftExt : ∀ {ℓ ℓ'} {A B : Type ℓ} → Lift {j = ℓ'} A ≡ Lift {j = ℓ'} B → A ≡ B
+    LiftExt p = ua (LiftEquiv ∙ₑ pathToEquiv p ∙ₑ invEquiv LiftEquiv)
+
 {-
   Direct proof of an associativity-related property. Combined with
   commutativity, this implies that the join is associative.