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

diff -r 359f34ed60ff -r bb5b028489dc monoidal.agda
--- a/monoidal.agda	Thu Nov 23 11:40:12 2017 +0900
+++ b/monoidal.agda	Thu Nov 23 12:08:42 2017 +0900
@@ -367,8 +367,8 @@
       MF = F
     ; ψ  = λ _ → HaskellMonoidalFunctor.unit mf
     ; isMonodailFunctor = record {
-             φab  = record { TMap = λ x →  φ x ; isNTrans = record { commute = comm0 } }
-         ;   associativity  = comm1
+             φab  = record { TMap = λ x →  φ ; isNTrans = record { commute = comm0 } }
+         ;   associativity  = λ {a b c} → comm1 {a} {b} {c}
          ;   unitarity-idr = λ {a b} → comm2 {a} {b}
          ;   unitarity-idl = λ {a b} → comm3 {a} {b}
       }
@@ -382,55 +382,68 @@
       _⊗_ 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 )
-      φ : (x : Obj (Sets × Sets) ) → Hom Sets (FObj (Functor● Sets Sets MonoidalSets F) x) (FObj (Functor⊗ Sets Sets MonoidalSets F) x)
-      φ _ z = HaskellMonoidalFunctor.φ mf z
+      φ : {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
+         (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
-                 (FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) ((φ a)  (x , y))
+                 (FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) (φ  (x , y))
              ≡⟨⟩
-                 (FMap F ( f □ g ) ) ((φ a)  (x , y))
+                 (FMap F ( f □ g ) ) (φ  (x , y))
              ≡⟨⟩
-                 FMap F ( map f g ) ((φ a)  (x , y))
+                 FMap F ( map f g ) (φ  (x , y))
              ≡⟨ {!!} ⟩
-                 (φ b ) (  FMap F  f x , FMap F g  y )
+                 φ (  FMap F  f x , FMap F g  y )
              ≡⟨⟩
-                 (φ b ) ( (  FMap F  f □ FMap F g ) (x , y) )
+                 φ ( (  FMap F  f □ FMap F g ) (x , y) )
              ≡⟨⟩
-                 (φ b ) ((FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) (x , y) )
+                 φ ((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 : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ  ]
+        ≈ Sets [ φ  o FMap (Functor● Sets Sets MonoidalSets F) f ] ]
       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 :  {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
-                  ( φ (x , (y ⊗ f)))  (( id1 Sets (FObj F x) □ φ (y , f) ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c)))
+                  φ  (( id1 Sets (FObj F x) □ φ  ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c)))
                ≡⟨⟩
-                  ( φ (x , (y ⊗ f)))  ( a , φ (y , f) (b , c)) 
+                  φ  ( a , φ  (b , c)) 
                ≡⟨ {!!} ⟩
-                 ( FMap F (Iso.≅→ (mα-iso isM))) (( φ ((x ⊗ y) , f) ) (( φ (x , y) (a , b)) , c ))
+                 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ  (a , b)) , c ))
                ≡⟨⟩
-                 ( FMap F (Iso.≅→ (mα-iso isM))) (( φ ((x ⊗ y) , f) ) (( φ (x , y) □  id1 Sets (FObj F f) ) ((a , b) , c)))
+                 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ  □  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 : Obj Sets} → Sets [ Sets [ φ 
+           o Sets [  (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ]
+        ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ  o  (φ  □ id1 Sets (FObj F c)) ] ] ]
       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 F (Iso.≅→ (mρ-iso isM)) o Sets [ φ  o
              FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ]
-      comm2 {a} {b} =  extensionality Sets ( λ x  → {!!} )
+      comm2 {a} {b} =  extensionality Sets ( λ x  → begin 
+                 (FMap F (Iso.≅→ (mρ-iso isM))) ( φ  ( proj₁ x , unit ) )
+               ≡⟨ {!!} ⟩
+                 Iso.≅→ (mρ-iso isM) x
+             ∎ )
+           where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
       comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o
-        Sets [ φ (m-i MonoidalSets , b) o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ]
-        ≈ Iso.≅→ (mλ-iso isM) ]
-      comm3 {a} {b} =  extensionality Sets ( λ x  → {!!} )
+        Sets [ φ  o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ]
+      comm3 {a} {b} =  extensionality Sets ( λ x  → begin 
+                 (FMap F (Iso.≅→ (mλ-iso isM))) ( φ  ( unit , proj₂ x) )
+               ≡⟨ {!!} ⟩
+                 Iso.≅→ (mλ-iso isM) x
+             ∎ )
+           where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning