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

diff -r bb5b028489dc -r 9092874a0633 monoidal.agda
--- a/monoidal.agda	Thu Nov 23 12:08:42 2017 +0900
+++ b/monoidal.agda	Thu Nov 23 12:37:22 2017 +0900
@@ -411,7 +411,7 @@
                   φ  (( id1 Sets (FObj F x) □ φ  ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c)))
                ≡⟨⟩
                   φ  ( a , φ  (b , c)) 
-               ≡⟨ {!!} ⟩
+               ≡⟨ {!!}  ⟩
                  ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ  (a , b)) , c ))
                ≡⟨⟩
                  ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ  □  id1 Sets (FObj F f) ) ((a , b) , c)))
@@ -423,28 +423,39 @@
            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 )
+      comm20 : {a b : Obj Sets} ( x : FObj F a * One )  → (  Sets [
+         FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ  o
+             FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x  ≡ Iso.≅→ (mρ-iso isM) x
+      comm20 {a} {b} (x , OneObj ) =  begin 
+                 (FMap F (Iso.≅→ (mρ-iso isM))) ( φ  ( x , unit ) )
+               ≡⟨ {!!} ⟩
+                 x
+               ≡⟨⟩
+                 Iso.≅→ (mρ-iso isM) ( x , OneObj )
+             ∎ 
+           where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
       comm2 : {a b : Obj Sets} → Sets [ Sets [
          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  → begin 
-                 (FMap F (Iso.≅→ (mρ-iso isM))) ( φ  ( proj₁ x , unit ) )
+      comm2 {a} {b} =  extensionality Sets ( λ x  → comm20 {a} {b} x )
+      comm30 : {a b : Obj Sets} ( x : One * FObj F b )  → (  Sets [
+         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 ) )
                ≡⟨ {!!} ⟩
-                 Iso.≅→ (mρ-iso isM) x
-             ∎ )
+                 x
+               ≡⟨⟩
+                 Iso.≅→ (mλ-iso isM) (  OneObj , x )
+             ∎ 
            where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
       comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o
         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
-
+      comm3 {a} {b} =  extensionality Sets ( λ x  → comm30 {a} {b} x )
 
 
 record Applicative {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )