Mercurial > hg > Members > kono > Proof > category

changeset 1120:121e28cccdf6

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 Sun, 07 Jul 2024 10:18:45 +0900
parents 4e7513a4229a
children 7df508f857cc
files src/monad→monoidal.agda
diffstat 1 files changed, 13 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/src/monad→monoidal.agda	Sat Jul 06 17:33:36 2024 +0900
+++ b/src/monad→monoidal.agda	Sun Jul 07 10:18:45 2024 +0900
@@ -64,6 +64,9 @@
           fcong : {b c : Obj (Sets {l})} → {f g : Hom (Sets {l}) b c }  → (x : FObj T b) 
              →  ((x : b) → f x ≡ g x) →  FMap T f x ≡ FMap T g x
           fcong x eq = IsFunctor.≈-cong (isFunctor T) eq x
+          fcong₂ : {b c : Obj (Sets {l})} → {f g : Hom (Sets {l}) b c }  → (x y : FObj T b) 
+             →  ((x : b) → f x ≡ g x) → x ≡ y →  FMap T f x ≡ FMap T g y
+          fcong₂ x x eq refl = IsFunctor.≈-cong (isFunctor T) eq x
           natφ : { a b c d : Obj Sets } { x : FObj T a} { y : FObj T b} { f : a → c } { g : b → d  }
              → FMap T (map f g) (φ (x , y)) ≡ φ (FMap T f x , FMap T g y)
           natφ {a} {b} {c} {d} {x} {y} {f} {g} = begin 
@@ -90,17 +93,22 @@
                   TMap μ (x * y * z) (FMap T ((λ f₁ → (FMap T (λ g → f , g)  (FMap T (λ g → f₁ , g) c )))) b)  
                      ≡⟨ sym (cong (λ k → TMap μ (x * y * z) k ) (fcong b (λ x → fdistr c )  ))  ⟩
                   TMap μ (x * y * z) (( FMap T (λ g → (FMap T (λ h → f , (g , h))) c)) b )  ∎ )  ) ⟩
-               ? ≡⟨ ? ⟩
-               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 (λ z₁ → TMap μ (x * y * z) (FMap T (λ g → FMap T (λ h → z₁ , g , h) c) b)) a) 
+                   ≡⟨ cong (λ k → TMap μ (x * y * z) k ) (fdistr a ) ⟩
                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 (λ f → FMap T (λ g → FMap T (λ h → f , g , h) c) b) a))  
+                   ≡⟨ cong ( λ k → TMap μ (x * (y * z)) (TMap μ _ k) ) (fcong a (λ w → begin
+                      FMap T (λ g  → FMap T (λ h → w , g , h) c) b  ≡⟨ fcong b (λ w → fdistr c) ⟩
+                      FMap T (λ g → FMap T (Iso.≅→ (mα-iso isM)) (FMap T (λ h → (w , g) , h) c)) b  ≡⟨ ?  ⟩
+                      FMap T (λ x₁ → FMap T (Iso.≅→ (mα-iso isM)) (FMap T (λ g → x₁ , g) c)) (FMap T (λ g → w , g) b)  ∎ ) ) ⟩
+               TMap μ (x * y * z) (TMap μ (FObj T (x * y * z)) (FMap T (λ z₁ → FMap T (λ x₁ → FMap T (Iso.≅→ (mα-iso isM)) (FMap T (λ g → x₁ , g) c)) (FMap T (λ g → z₁ , g) b)) a))
+                   ≡⟨ cong ( λ k → TMap μ (x * (y * z)) (TMap μ _ k) ) (fdistr a) ⟩
                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) _)  ⟩
+                   ≡⟨ cong (λ k → TMap μ (x * (y * z)) k ) (fdistr _)  ⟩
                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