Mercurial > hg > Members > kono > Proof > category

changeset 1117:e0ddd6d9ac80

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 05 Jul 2024 08:50:04 +0900
parents 5b80413de9b1
children 939dd4cdfea4
files src/monad→monoidal.agda
diffstat 1 files changed, 20 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/monad→monoidal.agda	Thu Jul 04 11:04:09 2024 +0900
+++ b/src/monad→monoidal.agda	Fri Jul 05 08:50:04 2024 +0900
@@ -75,12 +75,28 @@
           assocφ : { x y z : Obj Sets } { a : FObj T x } { b : FObj T y }{ c : FObj T z }
              → φ (a , φ (b , c)) ≡ FMap T (Iso.≅→ (mα-iso isM)) (φ (φ (a , b) , c))
           assocφ {x} {y} {z} {a} {b} {c} =  begin
-               φ (a , φ (b , c)) ≡⟨ cong ( TMap μ (x * (y * z)) ) (IsFunctor.≈-cong (isFunctor T) (λ x → begin
-                  FMap T (λ g → x , g) (φ (b , c)) ≡⟨ nat μ (FMap T (λ f → FMap T (λ g → (f , g)) c) b) ⟩
-                  TMap μ (Σ ? (λ v → Σ y (λ x₂ → z))) (FMap T (FMap T (λ g → x , g)) (FMap T (λ f → FMap T (λ g → f , g) c) b)) ≡⟨ ? ⟩
+               φ (a , φ (b , c)) ≡⟨ cong ( TMap μ (x * (y * z)) ) (IsFunctor.≈-cong (isFunctor T) (λ f → begin
+                  FMap T (λ g → f , g) (φ (b , c)) ≡⟨ refl ⟩
+                  FMap T (λ g → f , g)  (TMap μ (Σ y (λ v → z)) (FMap T (λ f → FMap T (λ g → f , g) c) b)) 
+                       ≡⟨ nat μ (FMap T (λ f → FMap T (λ g → (f , g)) c) b) ⟩
+                   TMap μ (x * y * z) (FMap T (FMap T (λ g → f , g)) (FMap T (λ f → FMap T (λ g → f , g) c) b))
+                       ≡⟨ ? ⟩
+                   TMap μ ( x * ( y * z ) ) ( ( FMap T (λ g → (FMap T (λ h → f , (g , h))) c)) b)   
+                        ≡⟨ sym ( cong (λ k → TMap μ (x * y * z) k ) (IsFunctor.≈-cong (isFunctor T) (λ w → sym (IsFunctor.distr (isFunctor T) c) ) b  )  )  ⟩
+                    ?   ≡⟨ cong (λ k → TMap μ (Σ ? (λ v → Σ y (λ x₂ → z)) ) k ) (IsFunctor.≈-cong (isFunctor T) (λ x → IsFunctor.distr (isFunctor T) ? ) ? )  ⟩
                   ? ∎ ) a ) ⟩
                ? ≡⟨ ? ⟩
-               TMap μ (x * y * z) (FMap T (FMap T (Iso.≅→ (mα-iso isM))) (FMap T (λ f → FMap T (λ g → f , g) c) (φ (a , b)))) ≡⟨ sym ( nat μ ? ) ⟩
+               TMap μ (x * y * z) (FMap T (TMap μ (x * y * z)) (FMap T (λ h → ? h) b))  
+                          ≡⟨ cong (λ k → TMap μ (x * y * z) (FMap T (TMap μ (x * y * z)) k ))  ? ⟩
+               TMap μ (x * y * z) (FMap T (TMap μ (x * y * z)) (FMap T (λ f → ( FMap T (λ g → (FMap T (λ h → f , (g , h))) c)) b ) a ))   
+                   ≡⟨ sym (IsMonad.assoc isMonad _ ) ⟩
+               ? ≡⟨ cong ( λ k → TMap μ (x * (y * z)) (TMap μ ? k) ) ? ⟩
+               TMap μ (x * y * z) (TMap μ (FObj T (x * y * z)) 
+                  (FMap T (FMap T (λ x₁ → FMap T (Iso.≅→ (mα-iso isM)) (FMap T (λ g → x₁ , g) c))) (FMap T (λ f → FMap T (λ g → f , g) b) a))) 
+                      ≡⟨ cong (λ k → TMap μ (x * (y * z)) k ) (sym ( nat μ _ )) ⟩
+               TMap μ (x * y * z) (FMap T (λ x₁ → FMap T (Iso.≅→ (mα-iso isM)) (FMap T (λ g → x₁ , g) c)) (φ (a , b))) 
+                   ≡⟨ cong (λ k → TMap μ (x * (y * z)) k ) (IsFunctor.distr (isFunctor T) _)  ⟩
+               TMap μ (x * y * z) (FMap T (FMap T (Iso.≅→ (mα-iso isM))) (FMap T (λ f → FMap T (λ g → f , g) c) (φ (a , b)))) ≡⟨ sym ( nat μ _ ) ⟩
                FMap T (Iso.≅→ (mα-iso isM)) (φ (φ (a , b) , c)) ∎
           proj1 :  {a : Obj Sets} → _*_ {l} {l} a One → a
           proj1 =  proj₁