# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1511577262 -32400
# Node ID 13cef2bfa5c87cea6660a01f67b960cd9c6ac139
# Parent  a017ed40dd77901038fbecc1563d7bc0fe29d914
...

diff -r a017ed40dd77 -r 13cef2bfa5c8 monoidal.agda
--- a/monoidal.agda	Fri Nov 24 16:38:34 2017 +0900
+++ b/monoidal.agda	Sat Nov 25 11:34:22 2017 +0900
@@ -479,13 +479,13 @@
       comm3 {a} {b} =  extensionality Sets ( λ x  → comm30 {a} {b} x )
 
 
+_・_ : {c₁ : Level} { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c
+_・_ f g = λ x → f ( g x ) 
 
 record IsApplicative {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
     ( pure  : {a : Obj Sets} → Hom Sets a ( FObj f a ) )
     ( _<*>_ : {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b )
         : Set (suc (suc c₁)) where
-  _・_ : { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c
-  _・_ f g = λ x → f ( g x ) 
   field
           --   http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf
           identity : { a : Obj Sets } { u : FObj f a } → pure ( id1 Sets a )  <*> u ≡ u
@@ -541,10 +541,14 @@
       _⊗_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
       _□_ : {a b c d : Obj Sets } ( f : Hom Sets a c ) ( g : Hom Sets b d ) → Hom Sets ( a ⊗ b ) ( c ⊗ d )
       _□_ f g = FMap (m-bi M) ( f , g )
+      right : {n : Level} { a b : Set n} → { x y : a → b } { h : a }  → ( x ≡ y ) → x h ≡ y h
+      right {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k h ) eq 
       φ : {x : Obj (Sets × Sets) } → Hom Sets (FObj (Functor● Sets Sets MonoidalSets F) x) (FObj (Functor⊗ Sets Sets MonoidalSets F) x)
       φ x = Applicative.<*> mf  (FMap F (λ j k → (j , k))  (proj₁ x )) (proj₂ x)
       _<*>_ :   {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b  
       _<*>_  = Applicative.<*> mf  
+      pure : {a : Obj Sets } → Hom Sets a ( FObj F a )
+      pure a = Applicative.pure mf a
       comm00 : {a b :  Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b}  (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) →
          (Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]) x ≡ (Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ]) x
       comm00 {a} {b} {(f , g)} (x , y) = begin
@@ -553,7 +557,7 @@
                  FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) ((FMap F (λ j k → j , k) x) <*> y)
              ≡⟨ {!!} ⟩
                  (FMap F (λ j k → f j , k)  x) <*> (FMap F g y)
-             ≡⟨ {!!} ⟩
+             ≡⟨  ≡-cong ( λ k → k  x <*> (FMap F g y)) ( IsFunctor.distr (isFunctor F ))  ⟩
                  (FMap F (λ j k → j , k) (FMap F f x)) <*> (FMap F g y)
              ≡⟨⟩
                  φ ( ( FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) ( x , y ) )
@@ -566,11 +570,18 @@
       comm10 :  {a b c : Obj Sets} → (x : ((FObj F a ⊗ FObj F b) ⊗ FObj F c) ) → (Sets [ φ  o Sets [ id1 Sets (FObj F a) □ φ  o Iso.≅→ (mα-iso isM) ] ]) x ≡
                 (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ  o φ  □ id1 Sets (FObj F c) ] ]) x
       comm10 {x} {y} {f} ((a , b) , c ) = begin
-                  {!!}
+                  φ  (( id1 Sets (FObj F x) □ φ  ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c)))
+               ≡⟨⟩
+                 (FMap F (λ j k → j , k) a) <*> ( (FMap F (λ j k → j , k) b) <*> c)
+               ≡⟨  sym (IsApplicative.composition  ismf) ⟩
+                 ((pure _・_ <*> (FMap F (λ j k → j , k) a)) <*>  (FMap F (λ j k → j , k) b))  <*> c
                ≡⟨ {!!} ⟩
-                 {!!}
+                  FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) ( (FMap F (λ j k → j , k) ( (FMap F (λ j k → j , k) a) <*> b)) <*> c)
+               ≡⟨⟩
+                 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ  □  id1 Sets (FObj F f) ) ((a , b) , c)))
              ∎
            where
+                  open Relation.Binary.PropositionalEquality
                   open Relation.Binary.PropositionalEquality.≡-Reasoning
       comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ 
            o Sets [  (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ]
@@ -582,9 +593,9 @@
       comm20 {a} {b} (x , OneObj ) =  begin 
                  (FMap F (Iso.≅→ (mρ-iso isM))) ( φ ((  FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit))) (x , OneObj) ))
                ≡⟨⟩
-                 FMap F proj₁ ((FMap F (λ j k → j , k) x) <*> (Applicative.pure mf OneObj))
+                 FMap F proj₁ ((FMap F (λ j k → j , k) x) <*> (pure OneObj))
                ≡⟨ ≡-cong ( λ k → FMap F  proj₁ k) ( IsApplicative.interchange   ismf )  ⟩
-                 FMap F proj₁ ((Applicative.pure mf (λ f → f OneObj)) <*> (FMap F (λ j k → j , k) x))
+                 FMap F proj₁ ((pure (λ f → f OneObj)) <*> (FMap F (λ j k → j , k) x))
                ≡⟨ {!!} ⟩
                  x
                ≡⟨⟩
@@ -600,9 +611,13 @@
          FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ  o
              FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x  ≡ Iso.≅→ (mλ-iso isM) x
       comm30 {a} {b} ( OneObj , x) =  begin 
-                 {!!}
+                 (FMap F (Iso.≅→ (mλ-iso isM))) ( φ  ( unit , x ) )
+               ≡⟨⟩
+                  FMap F proj₂ ((FMap F (λ j k → j , k) (pure OneObj)) <*> x)
                ≡⟨ {!!} ⟩
-                 {!!}
+                 x
+               ≡⟨⟩
+                 Iso.≅→ (mλ-iso isM) (  OneObj , x )
              ∎ 
            where
                   open Relation.Binary.PropositionalEquality.≡-Reasoning
@@ -632,8 +647,6 @@
           pure {a} x = FMap F ( λ y → x ) (unit )
           _<*>_ :   {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b        
           _<*>_ {a} {b} x y = FMap F ( λ r →  ( proj₁ r )  ( proj₂  r ) )  (φ ( x , y ))
-          _・_ : { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c
-          _・_ f g = λ x → f ( g x ) 
           -- left does not work right it makes yellows. why?
           -- left : {n : Level} { a b : Set n} → { x y : a } { h : a → b }  → ( x ≡ y ) → h x ≡ h y
           -- left {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → h k ) eq