# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1511701061 -32400
# Node ID e4ef69bae0449111152b405a5e66caebe16c3ed7
# Parent  6bc9d68898ef53c8cbfb3c1f57e5da9a1d53ab86
clean up

diff -r 6bc9d68898ef -r e4ef69bae044 monoidal.agda
--- a/monoidal.agda	Sun Nov 26 17:12:00 2017 +0900
+++ b/monoidal.agda	Sun Nov 26 21:57:41 2017 +0900
@@ -20,25 +20,8 @@
          iso→  :  C [ C [ ≅← o ≅→  ] ≈  id1 C x ]
          iso←  :  C [ C [ ≅→ o ≅←  ] ≈  id1 C y ]
 
-record IsStrictMonoidal  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (I : Obj C) ( BI : Functor ( C × C ) C )
-        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
-  infixr 9 _□_
-  _□_ : ( x y : Obj C ) → Obj C
-  _□_ x y = FObj BI ( x , y )
-  field
-      mα : {a b c : Obj C} →  ( a □ b) □ c  ≡  a □ ( b □ c )
-      mλ : (a : Obj C) → I □ a  ≡ a 
-      mρ : (a : Obj C) → a □ I  ≡ a 
+-- Monoidal Category
 
-record StrictMonoidal  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) 
-        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
-  field
-      m-i : Obj C
-      m-bi : Functor ( C × C ) C 
-      isMonoidal : IsStrictMonoidal C m-i m-bi
-
-
---      non strict version includes 5 naturalities
 record IsMonoidal  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (I : Obj C) ( BI : Functor ( C × C ) C )
         : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
   open Iso 
@@ -280,25 +263,15 @@
       ψ  : Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) )
       isMonodailFunctor : IsMonoidalFunctor  M N MF ψ
 
-record MonoidalFunctorWithoutCommutativities {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ}  ( M : Monoidal C ) ( N : Monoidal D )
-        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
-  _⊗_ : (x y : Obj C ) → Obj C
-  _⊗_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
-  _●_ : (x y : Obj D ) → Obj D
-  _●_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y
-  field
-      MF    : Functor C D
-      unit  : Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) )
-      φ    : {a b : Obj C} → Hom D ((FObj MF a) ●  (FObj MF b )) ( FObj MF ( a ⊗ b ) )
-
 open import Category.Sets
 
 import Relation.Binary.PropositionalEquality
 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
-data One {c : Level} : Set c where
-  OneObj : One   -- () in Haskell ( or any one object set )
+------
+-- Data.Product as a Tensor Product for Monoidal Category
+--
 
 SetsTensorProduct : {c : Level} → Functor ( Sets {c} × Sets {c} )  (Sets {c})
 SetsTensorProduct =   record {
@@ -314,7 +287,17 @@
                 (Sets × Sets) [ f ≈ g ] → Sets [ map (proj₁ f) (proj₂ f) ≈ map (proj₁ g) (proj₂ g) ]
         ≈-cong (refl , refl) =  refl
 
+-----
+--
+-- Sets as Monoidal Category
+--
+--  almost all comutativities are refl
+--
+--
+--
 
+data One {c : Level} : Set c where
+  OneObj : One   -- () in Haskell ( or any one object set )
 
 MonoidalSets : {c : Level} → Monoidal (Sets {c})
 MonoidalSets {c} = record {
@@ -335,16 +318,19 @@
    } where
        _⊗_ : ( a b : Obj Sets ) → Obj Sets
        _⊗_ a b = FObj SetsTensorProduct (a , b )
+       --  association operations
        mα→ : {a b c : Obj Sets} →  Hom Sets ( ( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) )
        mα→ ((a , b) , c ) =  (a , ( b , c ) )
        mα← : {a b c : Obj Sets} →  Hom Sets ( a ⊗ ( b ⊗ c ) ) ( ( a ⊗ b ) ⊗ c )
        mα← (a , ( b , c ) ) =  ((a , b) , c )
+       --  (One , a) ⇔ a 
        mλ→ : {a  : Obj Sets} →  Hom Sets ( One ⊗ a ) a
        mλ→ (_ , a) =  a
        mλ← : {a  : Obj Sets} →  Hom Sets  a ( One ⊗ a )
        mλ←  a = ( OneObj , a )
        mλiso : {a : Obj Sets} (x : One ⊗ a) →  (Sets [ mλ← o mλ→ ]) x ≡ id1 Sets (One ⊗ a) x
        mλiso (OneObj , _ ) = refl
+       --  (a , One) ⇔ a 
        mρ→ : {a  : Obj Sets} →  Hom Sets ( a ⊗ One )  a
        mρ→ (a , _) =  a
        mρ← : {a  : Obj Sets} →  Hom Sets a ( a ⊗ One ) 
@@ -377,18 +363,16 @@
 -- associativity         fmap assoc  (φ u (φ v w)) = φ (φ u v) w
 
 
-record HaskellMonoidalFunctor {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
+record HaskellMonoidalFunctor {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
         : Set (suc (suc c₁)) where
   field
-      unit  : FObj f One
-      φ    : {a b : Obj Sets} → Hom Sets ((FObj f a) *  (FObj f b )) ( FObj f ( a * b ) )
-  **    : {a b : Obj Sets} → FObj f a →  FObj f b →  FObj f ( a * b ) 
-  ** x y  = φ ( x , y )
+      unit  : FObj F One
+      φ    : {a b : Obj Sets} → Hom Sets ((FObj F a) *  (FObj F b )) ( FObj F ( a * b ) )
 
-lemma0 :  {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : HaskellMonoidalFunctor F )
+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
-lemma0 F mf ismf = record {
+HaskellMonoidalFunctor→MonoidalFunctor {c} F mf ismf = record {
       MF = F
     ; ψ  = λ _ → HaskellMonoidalFunctor.unit mf
     ; isMonodailFunctor = record {
@@ -400,8 +384,11 @@
   } where
       open Monoidal 
       open IsMonoidal hiding ( _■_ ;  _□_ )
+      M : Monoidal (Sets {c})
       M = MonoidalSets
+      isM  : IsMonoidal (Sets {c}) One SetsTensorProduct  
       isM = Monoidal.isMonoidal MonoidalSets 
+      unit : FObj F One
       unit = HaskellMonoidalFunctor.unit mf
       _⊗_ : (x y : Obj Sets ) → Obj Sets
       _⊗_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
@@ -487,19 +474,24 @@
     ( _<*>_ : {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b )
         : Set (suc (suc c₁)) where
   field
-          --   http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf
           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
+          --  from  http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf
 
 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
-      --  should have Applicative law ( if we do we have to prove someting more )
+
+------
+--
+--  Applicative ⇔ Monoidal
+--
+--
 
 lemma1 : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) → Applicative F → HaskellMonoidalFunctor F
 lemma1 F app = record { unit = unit ; φ = φ }
@@ -516,9 +508,15 @@
      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 : 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 ))
 
+
+------
+--
+-- Appllicative Functor is a Monoidal Functor
+--
+
 Applicative→Monoidal :  {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : Applicative F )
    → IsApplicative F ( Applicative.pure mf ) ( Applicative.<*> mf ) 
    → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
@@ -565,8 +563,9 @@
                   open Relation.Binary.PropositionalEquality
                   open Relation.Binary.PropositionalEquality.≡-Reasoning
       -----
-      -- they say it not possible prove FreeTheorem in Agda nor Coq
+      -- they say it is not possible to prove FreeTheorem in Agda nor Coq
       --    https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities
+      -- so we postulate this
       --    and we cannot indent postulate ...
       postulate FreeTheorem : {l : Level } {a b c : Obj (Sets {l}) } → (F : Functor (Sets {l}) (Sets {l} ) ) →  ( fmap : {a : Obj Sets } {b : Obj Sets } → Hom Sets a b → Hom Sets (FObj F a) ( FObj F b) ) →  {h f : Hom Sets a b } →  {g k : Hom Sets b c } →  Sets [  g o h  ≈  k o f  ] →  Sets [ FMap F g o fmap h  ≈  fmap k o FMap F f  ]
       UniquenessOfFunctor :   (F : Functor Sets Sets)
@@ -774,7 +773,10 @@
         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 )
 
-
+----
+--
+-- Monoidal laws imples Applicative laws
+--
 
 HaskellMonoidal→Applicative : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
       ( unit  : FObj F One )
@@ -976,3 +978,4 @@
            where
                   open Relation.Binary.PropositionalEquality.≡-Reasoning
 
+--