From 206bb935c621ec907b254a6f3aa46f4e12cf6de2 Mon Sep 17 00:00:00 2001
From: akai <1543960716@qq.com>
Date: Fri, 4 Aug 2023 17:20:11 -0400
Subject: [PATCH] add monad-assoc to Lift
---
formalizations/guarded-cubical/Semantics/Lift.agda | 3 +++
1 file changed, 3 insertions(+)
diff --git a/formalizations/guarded-cubical/Semantics/Lift.agda b/formalizations/guarded-cubical/Semantics/Lift.agda
index 5dafca3..7b5c5e0 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))
--
GitLab