# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1511286936 -32400
# Node ID d16327b48b8333a4e8fc09024d74ca38afa062ab
# Parent  7a729bb62ce342d95d4c95b14d6fb115d200414d
Monoidal Functor ( two functor remains )

diff -r 7a729bb62ce3 -r d16327b48b83 monoidal.agda
--- a/monoidal.agda	Wed Nov 22 02:09:22 2017 +0900
+++ b/monoidal.agda	Wed Nov 22 02:55:36 2017 +0900
@@ -102,13 +102,9 @@
 
 open import Category.Cat
 
-
 record IsMonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ}  ( M : Monoidal C ) ( N : Monoidal D )
       ( MF :   Functor C D )
-      ( F● :   Functor ( C × C ) D )
-      ( F⊗ :   Functor ( C × C ) D )
-      ( φab :  NTrans  ( C × C ) D  F● F⊗ )
-      ( φ   :  Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) ) )
+      ( ψ  :  Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) ) )
         : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
   _⊗_ : (x y : Obj C ) → Obj C
   _⊗_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
@@ -118,6 +114,28 @@
   _●_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y
   _■_ : {a b c d : Obj D } ( f : Hom D a c ) ( g : Hom D b d ) → Hom D ( a ● b ) ( c ● d )
   _■_ f g = FMap (Monoidal.m-bi N) ( f , g )
+  F● :  Functor ( C × C ) D
+  F●  =  record {
+       FObj = λ x  → (FObj MF (proj₁ x) ) ●  (FObj MF (proj₂ x) )
+     ; FMap = λ {x : Obj ( C × C ) } {y} f → FMap (Monoidal.m-bi N) (  FMap MF  (proj₁  f ) , FMap MF (proj₂ f)  )
+     ; isFunctor = record {
+             ≈-cong   = {!!}
+             ; identity = {!!}
+             ; distr    = {!!}
+     }
+    }
+  F⊗ : Functor ( C × C ) D
+  F⊗  =  record {
+       FObj = λ x → FObj MF ( proj₁ x ⊗ proj₂ x )
+     ; FMap = λ {a} {b} f →  FMap MF ( FMap (Monoidal.m-bi M) (  proj₁ f , proj₂ f) )
+     ; isFunctor = record {
+             ≈-cong   = {!!}
+             ; identity = {!!}
+             ; distr    = {!!}
+     }
+    }
+  field
+      φab :  NTrans  ( C × C ) D  F● F⊗ 
   open Iso
   open Monoidal
   open IsMonoidal hiding ( _■_ ;  _□_ )
@@ -127,36 +145,39 @@
   αD {a} {b} {c} =  ≅→ (mα-iso (isMonoidal N) {a} {b} {c}) 
   F : Obj C → Obj D
   F x = FObj MF x
+  φ : ( x y : Obj C ) →  Hom D ( FObj  F● (x , y) ) ( FObj F⊗ ( x , y ))
+  φ x y = NTrans.TMap φab ( x , y )
   1●φBC :  {a b c : Obj C} → Hom D  ( F a ● ( F b ● F c ) ) ( F a ● ( F ( b ⊗ c ) ))
-  1●φBC {a} {b} {c} =  id1 D (F a) ■  {!!}
+  1●φBC {a} {b} {c} =  id1 D (F a) ■  φ b c
   φAB⊗C :  {a b c : Obj C} → Hom D  ( F a ● ( F ( b ⊗ c ) )) (F ( a  ⊗ ( b  ⊗ c )))
-  φAB⊗C {a} {b} {c} =  {!!}
+  φAB⊗C {a} {b} {c} =   φ  a  (b ⊗ c )
   φAB●1 :  {a b c : Obj C} → Hom D  ( ( F a ●  F b ) ● F c ) ( F ( a ⊗ b ) ● F c )
-  φAB●1 {a} {b} {c} =  {!!} ■ id1 D (F c)
+  φAB●1 {a} {b} {c} =  φ a b ■ id1 D (F c)
   φA⊗BC :  {a b c : Obj C} → Hom D  ( F ( a ⊗ b ) ● F c ) (F ( (a  ⊗  b ) ⊗ c ))
-  φA⊗BC {a} {b} {c} = {!!}
+  φA⊗BC {a} {b} {c} = φ ( a ⊗ b ) c
   FαC : {a b c : Obj C} → Hom D (F ( (a  ⊗  b ) ⊗ c )) (F ( a  ⊗ ( b  ⊗ c )))
   FαC {a} {b} {c} =  FMap MF ( ≅→ (mα-iso (isMonoidal M) {a} {b} {c}) )
-  1●φ : { a b : Obj C } → Hom D (F a  ● Monoidal.m-i N ) ( F a ● F ( Monoidal.m-i M ) )
-  1●φ {a} {b} =  id1 D (F a)  ■  φ 
+  1●ψ : { a b : Obj C } → Hom D (F a  ● Monoidal.m-i N ) ( F a ● F ( Monoidal.m-i M ) )
+  1●ψ{a} {b} =  id1 D (F a)  ■  ψ
   φAIC : { a b : Obj C } → Hom D  ( F a ● F ( Monoidal.m-i M ) ) (F ( a  ⊗ Monoidal.m-i M ))
-  φAIC {a} {b} = {!!}
+  φAIC {a} {b} = φ a (  Monoidal.m-i M )
   FρC : { a b : Obj C } → Hom D   (F ( a  ⊗ Monoidal.m-i M ))( F a  )
   FρC {a} {b} = FMap MF (  ≅→ (mρ-iso (isMonoidal M) {a} ) )
   ρD : { a b : Obj C } → Hom D (F a  ● Monoidal.m-i N ) ( F a  )
   ρD {a} {b} =  ≅→ (mρ-iso (isMonoidal N) {F a} )
-  φ●1 : { a b : Obj C } → Hom D (Monoidal.m-i N ● F b  ) ( F ( Monoidal.m-i M )  ● F b  )
-  φ●1 {a} {b} =  φ  ■ id1 D (F b)
+  ψ●1 : { a b : Obj C } → Hom D (Monoidal.m-i N ● F b  ) ( F ( Monoidal.m-i M )  ● F b  )
+  ψ●1 {a} {b} =  ψ ■ id1 D (F b)
   φICB : { a b : Obj C } → Hom D  ( F ( Monoidal.m-i M )  ● F b  ) ( F (  ( Monoidal.m-i M )  ⊗ b ) )
-  φICB {a} {b} = {!!}
+  φICB {a} {b} = φ  ( Monoidal.m-i M ) b
   FλD : { a b : Obj C } → Hom D  ( F (  ( Monoidal.m-i M )  ⊗ b ) ) (F b ) 
   FλD {a} {b} = FMap MF ( ≅→ (mλ-iso (isMonoidal M) {b} ) )
   λD : { a b : Obj C } → Hom D  (Monoidal.m-i N ● F b  )  (F b ) 
   λD {a} {b} = ≅→ (mλ-iso (isMonoidal N) {F b} )
   field
      comm1 : {a b c : Obj C } → D [ D [ φAB⊗C {a} {b} {c} o D [ 1●φBC o αD ] ]  ≈ D [ FαC  o  D [ φA⊗BC o φAB●1 ] ] ]
-     comm-idr : {a b : Obj C } → D [ D [ FρC  {a} {b}  o D [ φAIC {a} {b} o  1●φ {a} {b} ] ]  ≈ ρD {a} {b}  ]
-     comm-idl : {a b : Obj C } → D [ D [ FλD  {a} {b}  o D [ φICB {a} {b} o  φ●1 {a} {b} ] ]  ≈ λD {a} {b}  ]
+     comm-idr : {a b : Obj C } → D [ D [ FρC  {a} {b}  o D [ φAIC {a} {b} o  1●ψ{a} {b} ] ]  ≈ ρD {a} {b}  ]
+     comm-idl : {a b : Obj C } → D [ D [ FλD  {a} {b}  o D [ φICB {a} {b} o  ψ●1 {a} {b} ] ]  ≈ λD {a} {b}  ]
+    where
 
 record MonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ}  ( M : Monoidal C ) ( N : Monoidal D )
         : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
@@ -166,21 +187,5 @@
   _●_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y
   field
       MF : Functor C D
-  F● :  Functor ( C × C ) D
-  F●  =  record {
-       FObj = λ x  → (FObj MF (proj₁ x) ) ●  (FObj MF (proj₂ x) )
-     ; FMap = λ {x : Obj ( C × C ) } {y} f → FMap (Monoidal.m-bi N) (  FMap MF  (proj₁  f ) , FMap MF (proj₂ f)  )
-     ; isFunctor = record {
-     }
-    }
-  F⊗ : Functor ( C × C ) D
-  F⊗  =  record {
-       FObj = λ x → FObj MF ( proj₁ x ⊗ proj₂ x )
-     ; FMap = λ {a} {b} f →  FMap MF ( FMap (Monoidal.m-bi M) (  proj₁ f , proj₂ f) )
-     ; isFunctor = record {
-     }
-    }
-  field
-      φab :  NTrans  ( C × C ) D  F● F⊗ 
-      φ   : Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) )
-      isMonodailFunctor : IsMonoidalFunctor  M N MF F● F⊗ φab φ
+      ψ  : Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) )
+      isMonodailFunctor : IsMonoidalFunctor  M N MF ψ