# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1511404812 -32400
# Node ID 359f34ed60ff1a36a4fb601467e6ec422330e6f8
# Parent  2807335e3fa01c81dddf7f92c4de713a9286b15f
fix

diff -r 2807335e3fa0 -r 359f34ed60ff monoidal.agda
--- a/monoidal.agda	Thu Nov 23 10:47:46 2017 +0900
+++ b/monoidal.agda	Thu Nov 23 11:40:12 2017 +0900
@@ -352,7 +352,7 @@
        mρiso : {a : Obj Sets} (x : a ⊗ One ) →  (Sets [ mρ← o mρ→ ]) x ≡ id1 Sets (a ⊗ One) x
        mρiso (_ , OneObj ) = refl
 
-
+≡-cong = Relation.Binary.PropositionalEquality.cong 
 
 record HaskellMonoidalFunctor {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
         : Set (suc (suc c₁)) where
@@ -369,8 +369,8 @@
     ; isMonodailFunctor = record {
              φab  = record { TMap = λ x →  φ x ; isNTrans = record { commute = comm0 } }
          ;   associativity  = comm1
-         ;   unitarity-idr = comm2
-         ;   unitarity-idl = comm3
+         ;   unitarity-idr = λ {a b} → comm2 {a} {b}
+         ;   unitarity-idl = λ {a b} → comm3 {a} {b}
       }
   } where
       open Monoidal 
@@ -384,13 +384,45 @@
       _□_ f g = FMap (m-bi M) ( f , g )
       φ : (x : Obj (Sets × Sets) ) → Hom Sets (FObj (Functor● Sets Sets MonoidalSets F) x) (FObj (Functor⊗ Sets Sets MonoidalSets F) x)
       φ _ z = HaskellMonoidalFunctor.φ mf z
+      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 φ a ]) x ≡ (Sets [ φ b o FMap (Functor● Sets Sets MonoidalSets F) f ]) x
+      comm00 {a} {b} {(f , g)} (x , y) = begin
+                 (FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) ((φ a)  (x , y))
+             ≡⟨⟩
+                 (FMap F ( f □ g ) ) ((φ a)  (x , y))
+             ≡⟨⟩
+                 FMap F ( map f g ) ((φ a)  (x , y))
+             ≡⟨ {!!} ⟩
+                 (φ b ) (  FMap F  f x , FMap F g  y )
+             ≡⟨⟩
+                 (φ b ) ( (  FMap F  f □ FMap F g ) (x , y) )
+             ≡⟨⟩
+                 (φ b ) ((FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) (x , y) )
+             ∎ 
+           where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
       comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ a ]
         ≈ Sets [ φ b o FMap (Functor● Sets Sets MonoidalSets F) f ] ]
-      comm0 {a} {b} {f} =  extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → {!!} )
+      comm0 {a} {b} {f} =  extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → comm00 x )
+      comm10 :  {a b c : Obj Sets} → (x : ((FObj F a ⊗ FObj F b) ⊗ FObj F c) ) → (Sets [ φ (a , (b ⊗ c)) o Sets [ id1 Sets (FObj F a) □ φ (b , c) o Iso.≅→ (mα-iso isM) ] ]) x ≡
+                (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ ((a ⊗ b) , c) o φ (a , b) □ id1 Sets (FObj F c) ] ]) x
+      comm10 {x} {y} {f} ((a , b) , c ) = begin
+                  ( φ (x , (y ⊗ f)))  (( id1 Sets (FObj F x) □ φ (y , f) ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c)))
+               ≡⟨⟩
+                  ( φ (x , (y ⊗ f)))  ( a , φ (y , f) (b , c)) 
+               ≡⟨ {!!} ⟩
+                 ( FMap F (Iso.≅→ (mα-iso isM))) (( φ ((x ⊗ y) , f) ) (( φ (x , y) (a , b)) , c ))
+               ≡⟨⟩
+                 ( FMap F (Iso.≅→ (mα-iso isM))) (( φ ((x ⊗ y) , f) ) (( φ (x , y) □  id1 Sets (FObj F f) ) ((a , b) , c)))
+             ∎
+           where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
       comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ (a , (b ⊗  c))
            o Sets [  (id1 Sets (FObj F a) □ φ (b , c)) o Iso.≅→ (mα-iso isM) ] ]
         ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ (a ⊗ b , c) o  (φ (a , b) □ id1 Sets (FObj F c)) ] ] ]
-      comm1 {a} {b} {c} =  extensionality Sets ( λ x  → {!!} )
+      comm1 {a} {b} {c} =  extensionality Sets ( λ x  → comm10 x )
       comm2 : {a b : Obj Sets} → Sets [ Sets [
          FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ (a , m-i MonoidalSets) o
              FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ]