changeset 1123:b6ab443f7a43

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jul 2024 17:05:16 +0900
parents 47694f2bcd7f
children f683d96fbc93
files src/monad→monoidal.agda
diffstat 1 files changed, 25 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/monad→monoidal.agda	Sun Jul 07 13:54:12 2024 +0900
+++ b/src/monad→monoidal.agda	Sun Jul 07 17:05:16 2024 +0900
@@ -116,10 +116,33 @@
           proj1 =  proj₁
           proj2 :  {a : Obj Sets} → _*_ {l} {l} One a → a
           proj2 =  proj₂
+          import HomReasoning
+          -- open ≈-Reasoning  (Sets {l}) as HR
           idrφ : {a : Obj Sets } { x : FObj T a } → FMap T (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ≡ x
-          idrφ {a} {x} =  ?
+          idrφ {a} {x} =  begin
+             FMap T (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ≡⟨ cong (λ f → FMap T (Iso.≅→ (mρ-iso isM)) (TMap μ _ f)) ( begin
+               FMap T (λ f → FMap T (λ g → f , g) unit) x ≡⟨ fcong x (λ g → nat η _ )  ⟩
+               FMap T (λ z → TMap η (Σ a (λ v → One)) (z  , OneObj)) x ≡⟨ fdistr x  ⟩
+               FMap T ( TMap η(a * One  )) (FMap T ( λ f → ( f , OneObj  )) x ) ∎ ) ⟩
+             FMap T proj1 (  TMap μ (a * One ) (FMap T ( TMap η(a * One  )) (FMap T ( λ f → ( f , OneObj  )) x )))  
+                 ≡⟨ cong (λ f →  FMap T proj₁ f) (IsMonad.unity2 isMonad _ ) ⟩
+             FMap T proj₁ (id1 Sets (FObj T (a * One)) (FMap T (λ f → f , OneObj) x)) ≡⟨ fcong _ (λ f →  ≈-Reasoning.idL Sets x ) ⟩
+             FMap T proj₁ (FMap T (λ f → f , OneObj) x) ≡⟨ sym (fdistr x) ⟩
+             FMap T ( id1 Sets a) x ≡⟨ IsFunctor.identity (isFunctor T) x ⟩
+             id1 Sets (FObj T a) x ≡⟨ refl ⟩
+             x ∎
           idlφ : {a : Obj Sets } { x : FObj T a } → FMap T (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x
-          idlφ {a} {x} =  ?
+          idlφ {a} {x} = begin
+             FMap T (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡⟨ cong (λ f → FMap T (Iso.≅→ (mλ-iso isM)) (TMap μ _ f)) ( begin
+               FMap T (λ f → FMap T (λ g → f , g) x) unit ≡⟨ nat η _  ⟩
+               TMap η (FObj T (Σ One (λ _ → a))) (FMap T (λ f → OneObj , f) x)  ∎ ) ⟩
+             FMap T proj₂ (TMap μ (One * a) (TMap η (FObj T (Σ One (λ _ → a))) (FMap T (λ f → OneObj , f) x))) 
+                 ≡⟨ cong (λ f →  FMap T proj₂ f) (IsMonad.unity1 isMonad _ )  ⟩
+             FMap T proj₂ (id1 Sets (FObj T (One * a)) (FMap T (λ f → OneObj , f) x)) ≡⟨ fcong _ (λ f →  ≈-Reasoning.idR Sets x ) ⟩
+             FMap T proj₂ (FMap T (λ f → OneObj , f) x) ≡⟨ sym (fdistr x) ⟩
+             FMap T ( id1 Sets a) x ≡⟨ IsFunctor.identity (isFunctor T) x ⟩
+             id1 Sets (FObj T a) x ≡⟨ refl ⟩
+             x ∎
 
 Monad→Applicative : {l : Level } (m : Monad (Sets {l} ) ) → Applicative ( Monad.T m )
 Monad→Applicative {l} monad = record {