Mercurial > hg > Members > kono > Proof > category
changeset 755:a1c3d82be8c8
monad to haskell monoidal done.
applicative remains
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 11 Dec 2017 11:01:23 +0900 |
| parents | f01e8d16a85d |
| children | 03f09d7dfffd |
| files | monad→monoidal.agda |
| diffstat | 1 files changed, 17 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/monad→monoidal.agda Mon Dec 11 01:45:18 2017 +0900 +++ b/monad→monoidal.agda Mon Dec 11 11:01:23 2017 +0900 @@ -89,9 +89,9 @@ open Relation.Binary.PropositionalEquality.≡-Reasoning ≡←≈ : {a b : Obj (Sets {l}) } { x y : Hom (Sets {l}) a b } → (x≈y : Sets [ x ≈ y ]) → x ≡ y ≡←≈ refl = refl - fcongλ : { a b c : Obj (Sets {l} ) } { x y : a → Hom (Sets {l}) a b } → Sets [ x ≈ y ] - → Sets [ FMap F ( λ (f : a) → ( x f )) ≈ FMap F ( λ (f : a ) → ( y f )) ] - fcongλ {a} {b} {c} {x} {y} eq = let open ≈-Reasoning (Sets {l}) hiding ( _o_ ) in fcong F eq + -- fcongλ : { a b c : Obj (Sets {l} ) } { x y : a → Hom (Sets {l}) a b } → Sets [ x ≈ y ] → ( g : ? ) + -- → Sets [ FMap F ( λ (f : a) → ( x f )) ≈ FMap F ( λ (f : a ) → ( y f )) ] + -- fcongλ {a} {b} {c} {x} {y} g eq = let open ≈-Reasoning (Sets {l}) hiding ( _o_ ) in fcong F ( extensionality Sets (λ f → monoidal.≡-cong ( λ h → g h f ) eq assocφ : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z } → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (a , b) , c)) assocφ {x} {y} {z} {a} {b} {c} = monoidal.≡-cong ( λ h → h a ) ( begin @@ -111,7 +111,12 @@ μ ( x * ( y * z ) ) o (FMap F (λ f → ( μ ( x * ( y * z ) ) o ( FMap F (FMap F (λ g → f , g) o (λ f₁ → FMap F (λ g → f₁ , g) c)))) b )) ≈⟨⟩ μ ( x * ( y * z ) ) o (FMap F (λ f → ( μ ( x * ( y * z ) ) o ( FMap F ((λ f₁ → (FMap F (λ g → f , g) o FMap F (λ g → f₁ , g)) c)))) b )) - ≈⟨ cdr {_} {_} {_} {_} {_} { μ ( x * ( y * z ) ) } (fcong F (extensionality Sets (λ f → {!!} ) )) ⟩ + ≈⟨ cdr {_} {_} {_} {_} {_} { μ ( x * ( y * z ) ) } (fcong F (extensionality Sets (λ f → monoidal.≡-cong ( λ h → h b ) ( begin + μ (x * y * z) o FMap F (λ f₁ → (FMap F (λ g → f , g) o FMap F (λ g → f₁ , g)) c) + ≈↑⟨ cdr {_} {_} {_} {_} {_} {μ (x * y * z)} ( fcong F ( extensionality Sets (λ f → monoidal.≡-cong ( λ h → h c ) ( distr F) ))) ⟩ + μ (x * y * z) o FMap F (λ f₁ → FMap F ((λ g → f , g) o (λ g → f₁ , g)) c) + ∎ + ) ))) ⟩ μ ( x * ( y * z ) ) o (FMap F (λ f → ( μ ( x * ( y * z ) ) o ( FMap F (λ f₁ → (FMap F ((λ g → f , g) o (λ g → f₁ , g))) c))) b )) ≈⟨⟩ μ ( x * ( y * z ) ) o (FMap F (λ f → ( μ ( x * ( y * z ) ) o ( FMap F (λ g → (FMap F (λ h → f , (g , h))) c))) b )) @@ -127,13 +132,13 @@ FMap F (λ f → ( FMap F (λ g → (FMap F (λ h → f , (g , h))) c)) b ) ≈⟨⟩ FMap F ( λ h → ( FMap F (( λ f → ( FMap F (λ x₂ → proj₁ f , proj₂ f , x₂)) c) o (λ g → h , g))) b ) - ≈⟨ {!!} ⟩ + ≈⟨ fcong F ( extensionality Sets (λ f → monoidal.≡-cong ( λ h → h b ) (distr F) )) ⟩ FMap F ( λ h → ( FMap F ( λ f → ( FMap F (λ x₂ → proj₁ f , proj₂ f , x₂)) c) o (FMap F (λ g → h , g))) b ) ≈⟨⟩ FMap F ( FMap F ( λ f → ( FMap F (λ x₂ → proj₁ f , proj₂ f , x₂)) c) o (λ h → FMap F (λ g → h , g) b) ) ≈⟨⟩ FMap F ( FMap F ( λ f → ( FMap F ((λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) o (λ g → f , g))) c) o (λ f → FMap F (λ g → f , g) b)) - ≈⟨ {!!} ⟩ + ≈⟨ fcong F ( car ( fcong F ( extensionality Sets (λ f → monoidal.≡-cong ( λ h → h c ) ( distr F ) )))) ⟩ FMap F ( FMap F ( λ f → ( FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) o FMap F (λ g → f , g)) c) o (λ f → FMap F (λ g → f , g) b) ) ≈⟨⟩ FMap F ( FMap F (FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) o (λ f → FMap F (λ g → f , g) c)) o (λ f → FMap F (λ g → f , g) b) ) @@ -310,7 +315,13 @@ ≈⟨⟩ ( λ w → μ c (FMap F (λ k → FMap F k w) (μ (a → c) (FMap F (λ k → FMap F k v) (μ ((a → b) → a → c) (FMap F (λ k → FMap F k u) (η ((b → c) → (a → b) → a → c) (λ f g x → f (g x))))))))) + ≈⟨⟩ + ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F (λ k → FMap F k v) o ( + μ ((a → b) → a → c) o (FMap F (λ k → FMap F k u) o η ((b → c) → (a → b) → a → c)) + ) ) ) ) ) (λ f g x → f (g x)) ) ≈⟨ {!!} ⟩ + ( λ w → (μ c o (FMap F ( λ k → ( FMap F k o ( μ b o FMap F (λ h → FMap F h w))) v )) ) u ) + ≈⟨⟩ ( λ w → μ c (FMap F (λ k → FMap F k (μ b (FMap F (λ h → FMap F h w) v))) u) ) ≈⟨⟩ ( λ w → u <*> (v <*> w) )