Mercurial > hg > Members > kono > Proof > category

changeset 699:10ab28030c20

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add definitions
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 21 Nov 2017 10:28:53 +0900
parents d648ebb8ac29
children cfd2d402c486
files monoidal.agda
diffstat 1 files changed, 9 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/monoidal.agda	Tue Nov 21 09:57:42 2017 +0900
+++ b/monoidal.agda	Tue Nov 21 10:28:53 2017 +0900
@@ -92,10 +92,16 @@
   open Iso
   open Monoidal
   open IsMonoidal hiding ( _⊗_ )
-  αD :  {a b c : Obj C} → Hom C (( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) )
-  αD {a} {b} {c} =  ≅→ (mα-iso (isMonoidal M) {a} {b} {c}) 
+  αC :  {a b c : Obj C} → Hom C (( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) )
+  αC {a} {b} {c} =  ≅→ (mα-iso (isMonoidal M) {a} {b} {c}) 
+  αD :  {a b c : Obj D} → Hom D (( a ● b ) ● c ) ( a ● ( b ● c ) )
+  αD {a} {b} {c} =  ≅→ (mα-iso (isMonoidal N) {a} {b} {c}) 
+  1●φBC :  {a b c : Obj C} → Hom D  ( FObj MF a ● ( FObj MF b ● FObj MF c ) ) ( FObj MF a ● ( FObj MF ( b ⊗ c ) ))
+  1●φBC = {!!} 
+  φAB⊗C :  {a b c : Obj C} → Hom D  ( FObj MF a ● ( FObj MF ( b ⊗ c ) )) (FObj MF ( a  ⊗ ( b  ⊗ c )))
+  φAB⊗C = {!!}
   field
-     comm1 :  {!!}
+     comm1 : D [ D [ φAB⊗C o D [ 1●φBC o αD ] ]  ≈ {!!} ]
 
 record MonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ}  ( M : Monoidal C ) ( N : Monoidal D )
         : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where