# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1511291534 -32400
# Node ID df3f1aae984f13ca8bc2cab6ff2655ed457e85a6
# Parent  d16327b48b8333a4e8fc09024d74ca38afa062ab
Monidal functor done.

diff -r d16327b48b83 -r df3f1aae984f monoidal.agda
--- a/monoidal.agda	Wed Nov 22 02:55:36 2017 +0900
+++ b/monoidal.agda	Wed Nov 22 04:12:14 2017 +0900
@@ -99,8 +99,87 @@
       m-bi : Functor ( C × C ) C 
       isMonoidal : IsMonoidal C m-i m-bi
 
+Functor● :  {c₁ c₂ ℓ : Level} (C D : Category c₁ c₂ ℓ) ( N : Monoidal D )
+      ( MF :   Functor C D ) →  Functor ( C × C ) D
+Functor● C D N MF =  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   = ≈-cong
+             ; identity = identity
+             ; distr    = distr
+     }
+    } where
+  _●_ : (x y : Obj D ) → Obj D
+  _●_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y
+  ≈-cong : {a b : Obj (C × C)} {f g : Hom (C × C) a b} → (C × C) [ f ≈ g ] →
+        D [ FMap (Monoidal.m-bi N) (FMap MF (proj₁ f) , FMap MF (proj₂ f))
+        ≈ FMap (Monoidal.m-bi N) (FMap MF (proj₁ g) , FMap MF (proj₂ g)) ]
+  ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning D in begin
+       FMap (Monoidal.m-bi N) (FMap MF (proj₁ f) , FMap MF (proj₂ f))
+     ≈⟨ fcong (Monoidal.m-bi N) (  fcong MF (  proj₁ f≈g ) , fcong MF ( proj₂ f≈g ))  ⟩
+       FMap (Monoidal.m-bi N) (FMap MF (proj₁ g) , FMap MF (proj₂ g))
+     ∎ 
+  identity : {a : Obj (C × C)} → D [ FMap (Monoidal.m-bi N) (FMap MF (proj₁ (id1 (C × C) a)) , FMap MF (proj₂ (id1 (C × C) a)))
+        ≈ id1 D (FObj MF (proj₁ a) ● FObj MF (proj₂ a)) ]
+  identity {a} =   let open ≈-Reasoning D in begin
+        FMap (Monoidal.m-bi N) (FMap MF (proj₁ (id1 (C × C) a)) , FMap MF (proj₂ (id1 (C × C) a)))
+     ≈⟨ fcong  (Monoidal.m-bi N) (  IsFunctor.identity (isFunctor MF )  ,  IsFunctor.identity (isFunctor MF ))  ⟩
+        FMap (Monoidal.m-bi N) ( id1 D (FObj MF (proj₁ a)) , id1 D (FObj MF (proj₂ a)))
+     ≈⟨ IsFunctor.identity (isFunctor  (Monoidal.m-bi N)) ⟩
+        id1 D (FObj MF (proj₁ a) ● FObj MF (proj₂ a))
+     ∎
+  distr : {a b c : Obj (C × C)} {f : Hom (C × C) a b} {g : Hom (C × C) b c} →
+     D [ FMap (Monoidal.m-bi N) (FMap MF (proj₁ ((C × C) [ g o f ])) , FMap MF (proj₂ ((C × C) [ g o f ])))
+       ≈ D [ FMap (Monoidal.m-bi N) (FMap MF (proj₁ g) , FMap MF (proj₂ g)) o FMap (Monoidal.m-bi N) (FMap MF (proj₁ f) , FMap MF (proj₂ f)) ] ]
+  distr {a} {b} {c} {f} {g} =  let open ≈-Reasoning D in begin
+       FMap (Monoidal.m-bi N) (FMap MF (proj₁ ((C × C) [ g o f ])) , FMap MF (proj₂ ((C × C) [ g o f ])))
+     ≈⟨ fcong (Monoidal.m-bi N) (  IsFunctor.distr ( isFunctor  MF) ,  IsFunctor.distr ( isFunctor MF )) ⟩
+        FMap (Monoidal.m-bi N) ( D [  FMap MF (proj₁ g)  o FMap MF (proj₁ f) ]  , D [ FMap MF (proj₂ g) o FMap MF (proj₂ f) ] )
+     ≈⟨ IsFunctor.distr ( isFunctor  (Monoidal.m-bi N)) ⟩
+       FMap (Monoidal.m-bi N) (FMap MF (proj₁ g) , FMap MF (proj₂ g)) o FMap (Monoidal.m-bi N) (FMap MF (proj₁ f) , FMap MF (proj₂ f))
+     ∎
 
-open import Category.Cat
+Functor⊗ :  {c₁ c₂ ℓ : Level} (C D : Category c₁ c₂ ℓ) ( M : Monoidal C ) 
+      ( MF :   Functor C D ) →  Functor ( C × C ) D
+Functor⊗ C D M MF =  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   = ≈-cong
+             ; identity = identity
+             ; distr    = distr
+     }
+    } where
+  _⊗_ : (x y : Obj C ) → Obj C
+  _⊗_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
+  ≈-cong : {a b : Obj (C × C)} {f g : Hom (C × C) a b} → (C × C) [ f ≈ g ] →
+     D [ FMap MF (FMap (Monoidal.m-bi M) (proj₁ f , proj₂ f)) ≈ FMap MF (FMap (Monoidal.m-bi M) (proj₁ g , proj₂ g)) ]
+  ≈-cong {a} {b} {f} {g} f≈g = IsFunctor.≈-cong (isFunctor MF ) ( IsFunctor.≈-cong (isFunctor  (Monoidal.m-bi M) ) f≈g  )
+  identity : {a : Obj (C × C)} → D [ FMap MF (FMap (Monoidal.m-bi M) (proj₁ (id1 (C × C) a) , proj₂ (id1 (C × C) a)))
+      ≈ id1 D (FObj MF (proj₁ a ⊗ proj₂ a)) ]
+  identity {a} = let open ≈-Reasoning D in begin
+        FMap MF (FMap (Monoidal.m-bi M) (proj₁ (id1 (C × C) a) , proj₂ (id1 (C × C) a)))
+     ≈⟨⟩
+        FMap MF (FMap (Monoidal.m-bi M) (id1 (C × C) a ) )
+     ≈⟨ fcong MF ( IsFunctor.identity (isFunctor (Monoidal.m-bi M) )) ⟩
+        FMap MF (id1 C (proj₁ a ⊗ proj₂ a))
+     ≈⟨ IsFunctor.identity (isFunctor MF) ⟩
+        id1 D (FObj MF (proj₁ a ⊗ proj₂ a))
+     ∎
+  distr : {a b c : Obj (C × C)} {f : Hom (C × C) a b} {g : Hom (C × C) b c} → D [
+        FMap MF (FMap (Monoidal.m-bi M) (proj₁ ((C × C) [ g o f ]) , proj₂ ((C × C) [ g o f ])))
+    ≈ D [ FMap MF (FMap (Monoidal.m-bi M) (proj₁ g , proj₂ g)) o FMap MF (FMap (Monoidal.m-bi M) (proj₁ f , proj₂ f)) ] ]
+  distr {a} {b} {c} {f} {g} =  let open ≈-Reasoning D in begin
+        FMap MF (FMap (Monoidal.m-bi M) (proj₁ ((C × C) [ g o f ]) , proj₂ ((C × C) [ g o f ])))
+     ≈⟨⟩
+        FMap MF (FMap (Monoidal.m-bi M) ( (C × C)  [ g o f ] ))
+     ≈⟨ fcong MF ( IsFunctor.distr (isFunctor (Monoidal.m-bi M))) ⟩
+        FMap MF (C [ FMap (Monoidal.m-bi M) g o FMap (Monoidal.m-bi M) f ])
+     ≈⟨ IsFunctor.distr ( isFunctor MF ) ⟩
+        FMap MF (FMap (Monoidal.m-bi M) (proj₁ g , proj₂ g)) o FMap MF (FMap (Monoidal.m-bi M) (proj₁ f , proj₂ f)) 
+     ∎
+
 
 record IsMonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ}  ( M : Monoidal C ) ( N : Monoidal D )
       ( MF :   Functor C D )
@@ -115,25 +194,9 @@
   _■_ : {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 D N MF
   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    = {!!}
-     }
-    }
+  F⊗  =  Functor⊗  C D M MF
   field
       φab :  NTrans  ( C × C ) D  F● F⊗ 
   open Iso
@@ -177,7 +240,6 @@
      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}  ]
-    where
 
 record MonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ}  ( M : Monoidal C ) ( N : Monoidal D )
         : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where