# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1511429084 -32400
# Node ID 5e101ee6dab95724fd973f3e26068ffdec32d391
# Parent  9092874a0633aa3d135395629564de99da8c5847
identity done

diff -r 9092874a0633 -r 5e101ee6dab9 monoidal.agda
--- a/monoidal.agda	Thu Nov 23 12:37:22 2017 +0900
+++ b/monoidal.agda	Thu Nov 23 18:24:44 2017 +0900
@@ -354,6 +354,22 @@
 
 ≡-cong = Relation.Binary.PropositionalEquality.cong 
 
+
+record IsHaskellMonoidalFunctor {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
+      ( unit  : FObj F One )
+      ( φ    : {a b : Obj Sets} → Hom Sets ((FObj F a) *  (FObj F b )) ( FObj F ( a * b ) ) )
+        : Set (suc (suc c₁)) where
+  isM  : IsMonoidal (Sets {c₁}) One SetsTensorProduct  
+  isM = Monoidal.isMonoidal MonoidalSets 
+  open IsMonoidal
+  field
+          law1 : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d  }
+             → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y)
+          law2 : { 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))
+          law3 : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ≡ x
+          law4 : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x
+
 record HaskellMonoidalFunctor {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
         : Set (suc (suc c₁)) where
   field
@@ -362,8 +378,10 @@
   **    : {a b : Obj Sets} → FObj f a →  FObj f b →  FObj f ( a * b ) 
   ** x y  = φ ( x , y )
 
-lemma0 :  {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → HaskellMonoidalFunctor F → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
-lemma0 F mf = record {
+lemma0 :  {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : HaskellMonoidalFunctor F )
+   → IsHaskellMonoidalFunctor F ( HaskellMonoidalFunctor.unit mf ) ( HaskellMonoidalFunctor.φ mf ) 
+   → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
+lemma0 F mf ismf = record {
       MF = F
     ; ψ  = λ _ → HaskellMonoidalFunctor.unit mf
     ; isMonodailFunctor = record {
@@ -392,7 +410,7 @@
                  (FMap F ( f □ g ) ) (φ  (x , y))
              ≡⟨⟩
                  FMap F ( map f g ) (φ  (x , y))
-             ≡⟨ {!!} ⟩
+             ≡⟨ IsHaskellMonoidalFunctor.law1 ismf ⟩
                  φ (  FMap F  f x , FMap F g  y )
              ≡⟨⟩
                  φ ( (  FMap F  f □ FMap F g ) (x , y) )
@@ -400,8 +418,7 @@
                  φ ((FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) (x , y) )
              ∎ 
            where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
+                  open Relation.Binary.PropositionalEquality.≡-Reasoning
       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 )
@@ -411,14 +428,13 @@
                   φ  (( id1 Sets (FObj F x) □ φ  ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c)))
                ≡⟨⟩
                   φ  ( a , φ  (b , c)) 
-               ≡⟨ {!!}  ⟩
+               ≡⟨ IsHaskellMonoidalFunctor.law2 ismf ⟩
                  ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ  (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
+                  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) ] ]
         ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ  o  (φ  □ id1 Sets (FObj F c)) ] ] ]
@@ -428,14 +444,13 @@
              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 ) )
-               ≡⟨ {!!} ⟩
+               ≡⟨ IsHaskellMonoidalFunctor.law3 ismf ⟩
                  x
                ≡⟨⟩
                  Iso.≅→ (mρ-iso isM) ( x , OneObj )
              ∎ 
            where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
+                  open Relation.Binary.PropositionalEquality.≡-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) ]
@@ -445,40 +460,111 @@
              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 ) )
-               ≡⟨ {!!} ⟩
+               ≡⟨ IsHaskellMonoidalFunctor.law4 ismf ⟩
                  x
                ≡⟨⟩
                  Iso.≅→ (mλ-iso isM) (  OneObj , x )
              ∎ 
            where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
+                  open Relation.Binary.PropositionalEquality.≡-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  → comm30 {a} {b} x )
 
 
-record Applicative {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
+
+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
+          identity : { a : Obj Sets } { u : FObj f a } → pure ( id1 Sets a )  <*> u ≡ u
+          composition : { a b c : Obj Sets } { u : FObj f ( b → c ) } { v : FObj f (a → b ) } { w : FObj f a }
+              → (( pure _・_ <*> u ) <*> v ) <*> w  ≡ u  <*> (v  <*> w)
+          homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a }  → pure f <*> pure x ≡ pure (f x)
+          interchange : { a b : Obj Sets } { u : FObj f ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u
+
+record Applicative {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
         : Set (suc (suc c₁)) where
   field
-      pure  : {a : Obj Sets} → Hom Sets a ( FObj f a )
-      <*>   : {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b
+      pure  : {a : Obj Sets} → Hom Sets a ( FObj F a )
+      <*>   : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b
       --  should have Applicative law
 
-lemma1 : {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) → Applicative f → HaskellMonoidalFunctor f
-lemma1 f app = record { unit = unit ; φ = φ }
+lemma1 : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) → Applicative F → HaskellMonoidalFunctor F
+lemma1 F app = record { unit = unit ; φ = φ }
   where
      open Applicative
-     unit  :  FObj f One
+     unit  :  FObj F One
      unit = pure app OneObj
-     φ :  {a b : Obj Sets} → Hom Sets ((FObj f a) *  (FObj f b )) ( FObj f ( a * b ) )
-     φ {a} {b} ( x , y ) = <*> app (FMap f (λ j k → (j , k)) x) y
+     φ :  {a b : Obj Sets} → Hom Sets ((FObj F a) *  (FObj F b )) ( FObj F ( a * b ) )
+     φ {a} {b} ( x , y ) = <*> app (FMap F (λ j k → (j , k)) x) y
 
-lemma2 : {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) → HaskellMonoidalFunctor f → Applicative f 
-lemma2 f mono = record { pure = pure ; <*> = <*> }
+lemma2 : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) → HaskellMonoidalFunctor F → Applicative F 
+lemma2 F mono = record { pure = pure ; <*> = <*> }
   where
      open HaskellMonoidalFunctor
-     pure  :  {a : Obj Sets} → Hom Sets a ( FObj f a )
-     pure {a} x = FMap f ( λ y → x ) (unit mono)
-     <*> :   {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b        --  ** mono  x y 
-     <*> {a} {b} x y = FMap f ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b ) )  (φ mono ( x , y ))
+     pure  :  {a : Obj Sets} → Hom Sets a ( FObj F a )
+     pure {a} x = FMap F ( λ y → x ) (unit mono)
+     <*> :   {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b        --  ** mono  x y 
+     <*> {a} {b} x y = FMap F ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b ) )  (φ mono ( x , y ))
+
+open Relation.Binary.PropositionalEquality
+
+HaskellMonoidal→Applicative : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
+      ( unit  : FObj F One )
+      ( φ    : {a b : Obj Sets} → Hom Sets ((FObj F a) *  (FObj F b )) ( FObj F ( a * b ) ) )
+      ( mono : IsHaskellMonoidalFunctor F unit φ ) 
+         → IsApplicative F (λ x →  FMap F ( λ y → x ) unit) (λ x y → FMap F ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b ) )  (φ ( x , y )))
+HaskellMonoidal→Applicative {c₁} F unit φ mono = record {
+          identity = identity 
+        ; composition = composition
+        ; homomorphism = homomorphism
+        ; interchange = interchange
+        }
+     where 
+          isM  : IsMonoidal (Sets {c₁}) One SetsTensorProduct  
+          isM = Monoidal.isMonoidal MonoidalSets 
+          open IsMonoidal
+          pure  :  {a : Obj Sets} → Hom Sets a ( FObj F a )
+          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 ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b ) )  (φ ( x , y ))
+          _・_ : { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c
+          _・_ f g = λ x → f ( g x ) 
+          identity : { a : Obj Sets } { u : FObj F a } → pure ( id1 Sets a )  <*> u ≡ u
+          identity {a} {u} = begin 
+                 pure ( id1 Sets a )  <*> u
+               ≡⟨⟩
+                 ( FMap F ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b )) ) ( φ (  FMap F ( λ y → id1 Sets a ) unit  , u ) )
+               ≡⟨  sym ( ≡-cong ( λ k → ( FMap F ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b )) ) ( φ ( FMap F ( λ y → id1 Sets a ) unit  ,  k u )))
+                    (  IsFunctor.identity ( Functor.isFunctor F ) ) ) ⟩
+                 ( FMap F ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b )) ) ( φ (  FMap F ( λ y → id1 Sets a ) unit  , FMap F (id1 Sets a) u ) )
+               ≡⟨ sym ( ≡-cong ( λ k → ( FMap F ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b )) ) k  )  (  IsHaskellMonoidalFunctor.law1 mono  ) )  ⟩
+                   FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (FMap F (map (λ y → id1 Sets a) (λ x → x )) (φ (unit , u )))
+               ≡⟨  ≡-cong ( λ k → k  (φ (unit , u ) )) ( sym ( IsFunctor.distr ( Functor.isFunctor F ) ) )  ⟩
+                   FMap F (λ x →  (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) ((map (λ y → id1 Sets a) (λ x → x )) x )) (φ (unit , u ) )
+               ≡⟨⟩
+                   FMap F (λ x → proj₂ x ) (φ (unit , u ) )
+               ≡⟨⟩
+                   FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , u ))
+               ≡⟨  IsHaskellMonoidalFunctor.law4 mono   ⟩
+                  u
+             ∎ 
+           where
+                  open Relation.Binary.PropositionalEquality.≡-Reasoning
+          composition : { a b c : Obj Sets } { u : FObj F ( b → c ) } { v : FObj F (a → b ) } { w : FObj F a }
+              → (( pure _・_ <*> u ) <*> v ) <*> w  ≡ u  <*> (v  <*> w)
+          composition {a} {b} {c} {u} {v} {w} = begin
+                  ?
+                ≡⟨  ? ⟩
+                 ?
+              ∎ 
+           where
+                  open Relation.Binary.PropositionalEquality.≡-Reasoning
+          homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a }  → pure f <*> pure x ≡ pure (f x)
+          homomorphism = {!!}
+          interchange : { a b : Obj Sets } { u : FObj F ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u
+          interchange = {!!}