# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1513038344 -32400
# Node ID c30ca91f3a766ff9649da04dbff383b0f836c669
# Parent  171f5386e87ee8f8afec49ed07212e6047f1ec2b
Applicative all done

diff -r 171f5386e87e -r c30ca91f3a76 monad→monoidal.agda
--- a/monad→monoidal.agda	Tue Dec 12 00:20:07 2017 +0900
+++ b/monad→monoidal.agda	Tue Dec 12 09:25:44 2017 +0900
@@ -20,31 +20,24 @@
 import Relation.Binary.PropositionalEquality
 
 Monad→HaskellMonoidalFunctor : {l : Level } (m : Monad (Sets {l} ) ) → HaskellMonoidalFunctor ( Monad.T m )
-Monad→HaskellMonoidalFunctor monad = record {
+Monad→HaskellMonoidalFunctor {l} monad = record {
          unit = unit
        ; φ = φ
-   } where
-      F = Monad.T monad
-      η = NTrans.TMap (Monad.η monad ) 
-      unit  : FObj F One
-      unit  = η One OneObj 
-      φ    : {a b : Obj Sets} → Hom Sets ((FObj F a) *  (FObj F b )) ( FObj F ( a * b ) )
-      φ {a} {b} (x , y)  =  ( NTrans.TMap (Monad.μ monad ) (a * b) ) (FMap F ( λ f → FMap F ( λ g → ( f , g )) y ) x )
-
-Monad→IsHaskellMonoidalFunctor : {l : Level } (m : Monad (Sets {l} ) ) → IsHaskellMonoidalFunctor (  Monad.T m )
-     ( HaskellMonoidalFunctor.unit ( Monad→HaskellMonoidalFunctor m ) ) ( HaskellMonoidalFunctor.φ ( Monad→HaskellMonoidalFunctor m ) )
-Monad→IsHaskellMonoidalFunctor {l} monad = record {
+       ; isHaskellMonoidalFunctor = record {
           natφ = natφ 
         ; assocφ = assocφ  
         ; idrφ =  idrφ  
         ; idlφ = idlφ  
+       }
    } where
           F = Monad.T monad
-          unit = HaskellMonoidalFunctor.unit ( Monad→HaskellMonoidalFunctor monad ) 
-          φ =  HaskellMonoidalFunctor.φ ( Monad→HaskellMonoidalFunctor monad )
           isM = Monoidal.isMonoidal MonoidalSets 
           μ = NTrans.TMap (Monad.μ monad) 
           η = NTrans.TMap (Monad.η monad) 
+          unit  : FObj F One
+          unit  = η One OneObj 
+          φ    : {a b : Obj Sets} → Hom Sets ((FObj F a) *  (FObj F b )) ( FObj F ( a * b ) )
+          φ {a} {b} (x , y)  =  ( NTrans.TMap (Monad.μ monad ) (a * b) ) (FMap F ( λ f → FMap F ( λ g → ( f , g )) y ) x )
           open IsMonoidal
           id : { a : Obj (Sets {l}) } → a → a
           id x = x
@@ -255,31 +248,24 @@
                   open ≈-Reasoning Sets hiding ( _o_ )
 
 Monad→Applicative : {l : Level } (m : Monad (Sets {l} ) ) → Applicative ( Monad.T m )
-Monad→Applicative monad = record {
+Monad→Applicative {l} monad = record {
          pure = pure
-       ; <*> = <*>
-   } where
-      F = Monad.T monad
-      η = NTrans.TMap (Monad.η monad ) 
-      pure  : {a : Obj Sets} → Hom Sets a ( FObj F a )
-      pure {a}  = η a
-      <*>   : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b
-      <*> {a} {b} f x = ( NTrans.TMap (Monad.μ monad ) b ) ( (FMap F (λ k → FMap F k x )) f )
-
-Monad→IsApplicative : {l : Level } (m : Monad (Sets {l} ) ) → IsApplicative (  Monad.T m ) 
-          ( Applicative.pure (  Monad→Applicative m )  ) ( Applicative.<*> (  Monad→Applicative m ) )
-Monad→IsApplicative {l} monad = record {
-          identity = identity 
-       ;  composition = composition 
-       ;  homomorphism  = homomorphism 
-       ;  interchange  = interchange 
+       ; <*> = _<*>_
+       ; isApplicative = record {
+            identity = identity 
+         ;  composition = composition 
+         ;  homomorphism  = homomorphism 
+         ;  interchange  = interchange 
+      }
   } where
           F = Monad.T monad
-          pure = Applicative.pure (  Monad→Applicative monad ) 
-          _<*>_ = Applicative.<*> (  Monad→Applicative monad ) 
           isM = Monoidal.isMonoidal ( MonoidalSets {l} )
           η = NTrans.TMap (Monad.η monad ) 
           μ = NTrans.TMap (Monad.μ monad) 
+          pure  : {a : Obj Sets} → Hom Sets a ( FObj F a )
+          pure {a}  = η a
+          _<*>_   : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b
+          _<*>_ {a} {b} f x = ( NTrans.TMap (Monad.μ monad ) b ) ( (FMap F (λ k → FMap F k x )) f )
           open IsMonoidal
           id : { a : Obj (Sets {l}) } → a → a
           id x = x
@@ -455,3 +441,4 @@
                   open ≈-Reasoning Sets hiding ( _o_ )
 
 
+-- end
diff -r 171f5386e87e -r c30ca91f3a76 monoidal.agda
--- a/monoidal.agda	Tue Dec 12 00:20:07 2017 +0900
+++ b/monoidal.agda	Tue Dec 12 09:25:44 2017 +0900
@@ -394,11 +394,11 @@
   field
       unit  : FObj F One
       φ    : {a b : Obj Sets} → Hom Sets ((FObj F a) *  (FObj F b )) ( FObj F ( a * b ) )
+      isHaskellMonoidalFunctor : IsHaskellMonoidalFunctor F unit φ
 
 HaskellMonoidalFunctor→MonoidalFunctor :  {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : HaskellMonoidalFunctor F )
-   → IsHaskellMonoidalFunctor F ( HaskellMonoidalFunctor.unit mf ) ( HaskellMonoidalFunctor.φ mf ) 
    → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
-HaskellMonoidalFunctor→MonoidalFunctor {c} F mf ismf = record {
+HaskellMonoidalFunctor→MonoidalFunctor {c} F mf = record {
       MF = F
     ; ψ  = λ _ → HaskellMonoidalFunctor.unit mf
     ; isMonodailFunctor = record {
@@ -410,6 +410,8 @@
   } where
       open Monoidal 
       open IsMonoidal hiding ( _■_ ;  _□_ )
+      ismf : IsHaskellMonoidalFunctor F ( HaskellMonoidalFunctor.unit mf ) ( HaskellMonoidalFunctor.φ mf ) 
+      ismf = HaskellMonoidalFunctor.isHaskellMonoidalFunctor mf
       M : Monoidal (Sets {c})
       M = MonoidalSets
       isM  : IsMonoidal (Sets {c}) One SetsTensorProduct  
@@ -495,16 +497,16 @@
 _・_ : {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 )
+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
   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 }
+          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
+          interchange : { a b : Obj Sets } { u : FObj F ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u
           --  from  http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf
 
 record Applicative {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
@@ -512,30 +514,7 @@
   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
-
-------
---
---  Applicative ⇔ Monoidal
---
---
-
-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 = 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
-
-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  
-     <*> {a} {b} x y = FMap F ( λ r →  ( proj₁ r )  ( proj₂  r ) )  (φ mono ( x , y ))
+      isApplicative : IsApplicative F pure <*>
 
 ------
 --
@@ -780,17 +759,25 @@
 --
 
 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 ( λ r →  ( proj₁ r )  ( proj₂  r ) )  (φ ( x , y )))
-HaskellMonoidal→Applicative {c₁} F unit φ mono = record {
+      ( Mono : HaskellMonoidalFunctor F ) 
+         → Applicative F  
+HaskellMonoidal→Applicative {c₁} F Mono = record {
+        pure = pure ;
+        <*> = _<*>_ ;
+        isApplicative = record {
           identity = identity 
         ; composition = composition
         ; homomorphism = homomorphism
         ; interchange = interchange
         }
+     }
      where 
+          unit  : FObj F One 
+          unit = HaskellMonoidalFunctor.unit Mono
+          φ    : {a b : Obj Sets} → Hom Sets ((FObj F a) *  (FObj F b )) ( FObj F ( a * b ) ) 
+          φ = HaskellMonoidalFunctor.φ Mono
+          mono : IsHaskellMonoidalFunctor F unit φ 
+          mono = HaskellMonoidalFunctor.isHaskellMonoidalFunctor Mono
           id : { a : Obj Sets } → a → a 
           id x = x
           isM  : IsMonoidal (Sets {c₁}) One SetsTensorProduct  
@@ -985,31 +972,49 @@
 --
 
 Applicative→HaskellMonoidal : {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   )
-     ( app : IsApplicative F pure <*> )
-       → IsHaskellMonoidalFunctor F (pure OneObj) (λ x →  <*> (FMap F (λ j k → (j , k)) ( proj₁ x)) ( proj₂ x) )
-Applicative→HaskellMonoidal {l}  F pure <*> app = record {
+     ( App : Applicative F  )
+       → HaskellMonoidalFunctor F 
+Applicative→HaskellMonoidal {l}  F App = record {
+      unit = unit ;
+      φ = φ ;
+      isHaskellMonoidalFunctor = record {
           natφ = natφ 
         ; assocφ =  assocφ  
         ; idrφ = idrφ 
         ; idlφ = idlφ  
+      }
    } where
+          pure = Applicative.pure App
+          <*> = Applicative.<*> App
+          app = Applicative.isApplicative App
           unit  :  FObj F One
           unit = pure OneObj
           φ :  {a b : Obj Sets} → Hom Sets ((FObj F a) *  (FObj F b )) ( FObj F ( a * b ) )
           φ = λ x →  <*> (FMap F (λ j k → (j , k)) ( proj₁ x)) ( proj₂ x)
           isM  : IsMonoidal (Sets {l}) One SetsTensorProduct
           isM = Monoidal.isMonoidal MonoidalSets
+          MF :  MonoidalFunctor {_} {l} {_} {Sets} {Sets} MonoidalSets MonoidalSets
+          MF = Applicative→Monoidal F App  app
+          isMF = MonoidalFunctor.isMonodailFunctor MF
           natφ : { 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)
-          natφ = {!!}
+          natφ {a} {b} {c} {d} {x} {y} {f} {g} = begin
+                   FMap F (map f g) (φ (x , y))
+                ≡⟨⟩
+                   FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) (<*> (FMap F (λ j k → j , k) x) y)
+                ≡⟨  ≡-cong ( λ h → h (x , y)) (  IsNTrans.commute ( NTrans.isNTrans ( IsMonoidalFunctor.φab isMF  ))) ⟩
+                   <*> (FMap F (λ j k → j , k) (FMap F f x)) (FMap F g y)
+                ≡⟨⟩
+                   φ (FMap F f x , FMap F g y)
+             ∎   
+           where
+                  open Relation.Binary.PropositionalEquality.≡-Reasoning
           assocφ : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z }
              → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (IsMonoidal.mα-iso isM)) (φ (φ (a , b) , c))
-          assocφ = {!!}
+          assocφ {x} {y} {z} {a} {b} {c} = ≡-cong ( λ h → h ((a , b) , c ) ) ( IsMonoidalFunctor.associativity isMF )
           idrφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (IsMonoidal.mρ-iso isM)) (φ (x , unit)) ≡ x
-          idrφ = {!!}
+          idrφ {a} {x} =  ≡-cong ( λ h → h (x , OneObj ) ) ( IsMonoidalFunctor.unitarity-idr isMF {a} {One}  )
           idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (IsMonoidal.mλ-iso isM)) (φ (unit , x)) ≡ x
-          idlφ = {!!}
+          idlφ {a} {x} =  ≡-cong ( λ h → h (OneObj , x ) ) ( IsMonoidalFunctor.unitarity-idl isMF {One} {a}  )