Mercurial > hg > Members > kono > Proof > category

changeset 697:c68ba494abfd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 21 Nov 2017 00:11:10 +0900
parents 10ccac3bc285
children d648ebb8ac29
files monoidal.agda
diffstat 1 files changed, 9 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/monoidal.agda	Mon Nov 20 22:52:55 2017 +0900
+++ b/monoidal.agda	Tue Nov 21 00:11:10 2017 +0900
@@ -64,21 +64,21 @@
   _●_ x y =  (IsMonoidal._⊗_ (Monoidal.isMonoidal N) ) x y
   field
       MF : Functor C D
-  F● : (a b : Obj C ) → Functor ( C × C ) D
-  F● a b =  record {
-       FObj = λ x  → (FObj MF a) ●  (FObj MF b)
-     ; FMap = λ {a} {b} f → FMap (Monoidal.m-bi N) (  FMap MF  ? , FMap MF {!!} )
+  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⊗ : (a b : Obj C ) → Functor ( C × C ) D
-  F⊗ a b =  record {
-       FObj = λ x → FObj MF ( a ⊗ b )
-     ; FMap = λ {a} {b} f →  FMap MF ( FMap (Monoidal.m-bi M) (  {!!}  , {!!} ) )
+  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 : {a b : Obj C} → NTrans  ( C × C ) D  (F● a b) (F⊗ a b )
+      φab :  NTrans  ( C × C ) D  F● F⊗ 
       φ   : Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) )
       isMonodailFunctor : IsMonoidalFunctor  M N