diff --git a/formalizations/guarded-cubical/Semantics/Lift.agda b/formalizations/guarded-cubical/Semantics/Lift.agda
index 5dafca39cb1f3e7cf88db4fb3aacdd2cb33cebb1..7b5c5e09718745c2f6b01e8cd53510f1dd7b5d66 100644
--- a/formalizations/guarded-cubical/Semantics/Lift.agda
+++ b/formalizations/guarded-cubical/Semantics/Lift.agda
@@ -283,6 +283,9 @@ monad-unit-r = fix lem
                      ≡⟨ refl ⟩
                    θ x ∎
 
+monad-assoc : {A B C : Type} -> (f : A -> L℧ B) (g : B -> L℧ C) (la : L℧ A) -> ext g (ext f la) ≡ ext (λ x -> ext g (f x)) la
+monad-assoc = {!!}
+
 
 mapL : (A -> B) -> L℧ A -> L℧ B
 mapL f la = bind la (λ a -> ret (f a))