Mercurial > hg > Members > kono > Proof > category
changeset 1118:939dd4cdfea4
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 06 Jul 2024 09:41:27 +0900 |
| parents | e0ddd6d9ac80 |
| children | 4e7513a4229a |
| files | src/monad→monoidal.agda |
| diffstat | 1 files changed, 18 insertions(+), 11 deletions(-) [+] |
line wrap: on
line diff
--- a/src/monad→monoidal.agda Fri Jul 05 08:50:04 2024 +0900 +++ b/src/monad→monoidal.agda Sat Jul 06 09:41:27 2024 +0900 @@ -58,33 +58,40 @@ open IsMonoidal id : { a : Obj (Sets {l}) } → a → a id x = x + fdistr : {a b c : Obj (Sets {l})} → {f : Hom (Sets {l}) b c } {g : Hom (Sets {l} ) a b } → (x : FObj T a) + → FMap T (λ z → f (g z)) x ≡ FMap T f ( FMap T g x ) + fdistr x = IsFunctor.distr (isFunctor T) x + 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 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 FMap T (map f g) (φ (x , y)) ≡⟨ nat μ (FMap T (λ a → FMap T (λ b → (a , b)) y ) x) ⟩ TMap μ (c * d) (FMap T (FMap T (map f g)) (FMap T (λ f₁ → FMap T (λ g₁ → f₁ , g₁) y) x)) ≡⟨ cong (λ k → TMap μ (c * d) k) ( begin - FMap T (FMap T (map f g)) (FMap T (λ f₁ → FMap T (λ g₁ → f₁ , g₁) y) x) ≡⟨ sym (IsFunctor.distr ( isFunctor T ) x) ⟩ - FMap T (λ f₁ → FMap T (map f g) (FMap T (λ g₁ → f₁ , g₁) y)) x ≡⟨ IsFunctor.≈-cong (isFunctor T) ( λ x → begin + FMap T (FMap T (map f g)) (FMap T (λ f₁ → FMap T (λ g₁ → f₁ , g₁) y) x) ≡⟨ sym (fdistr x) ⟩ + FMap T (λ f₁ → FMap T (map f g) (FMap T (λ g₁ → f₁ , g₁) y)) x ≡⟨ fcong x ( λ x → begin FMap T (map f g) (FMap T (λ g₁ → x , g₁) y) ≡⟨ sym (IsFunctor.distr (isFunctor T) y) ⟩ - FMap T (λ x₂ → map f g (x , x₂)) y ≡⟨ (IsFunctor.distr (isFunctor T) y) ⟩ -- to use Sets assoc in F - FMap T (λ g₁ → f x , g₁) (FMap T g y) ∎ ) x ⟩ - FMap T (λ x₁ → FMap T (λ g₁ → f x₁ , g₁) (FMap T g y)) x ≡⟨ IsFunctor.distr ( isFunctor T ) x ⟩ + FMap T (λ x₂ → map f g (x , x₂)) y ≡⟨ fdistr y ⟩ -- to use Sets assoc in F + FMap T (λ g₁ → f x , g₁) (FMap T g y) ∎ ) ⟩ + FMap T (λ x₁ → FMap T (λ g₁ → f x₁ , g₁) (FMap T g y)) x ≡⟨ fdistr x ⟩ FMap T (λ f → FMap T (λ g → f , g) (FMap T g y)) (FMap T f x) ∎ ) ⟩ φ (FMap T f x , FMap T g y) ∎ 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) (λ f → begin + φ (a , φ (b , c)) ≡⟨ cong ( TMap μ (x * (y * z)) ) (fcong a (λ 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 (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 (λ g → (FMap T (λ h → f , (g , h))) c)) b) + ≡⟨ sym ( cong (λ k → TMap μ (x * y * z) k ) (fcong b (λ w → sym (fdistr c) ) ) ) ⟩ + TMap μ (x * y * z) (FMap T (λ z₁ → FMap T ? (FMap T ? c)) b) ≡⟨ ? ⟩ + TMap μ (x * y * z) (FMap T (λ z₁ → FMap T (λ z₂ → ?) ? ) a ) ≡⟨ cong (λ k → TMap μ (x * y * z) k ) (fcong ? (λ x → fdistr ? ) ) ⟩ + TMap μ (x * y * z) ? ∎ ) ) ⟩ ? ≡⟨ ? ⟩ 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 )) ? ⟩