Mercurial > hg > Members > kono > Proof > category

changeset 700:cfd2d402c486

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
monodial cateogry and functor
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 21 Nov 2017 22:42:33 +0900
parents 10ab28030c20
children 7a729bb62ce3
files monoidal.agda
diffstat 1 files changed, 81 insertions(+), 28 deletions(-) [+]
line wrap: on
line diff
--- a/monoidal.agda	Tue Nov 21 10:28:53 2017 +0900
+++ b/monoidal.agda	Tue Nov 21 22:42:33 2017 +0900
@@ -24,13 +24,13 @@
 
 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 )
+  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 
+      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 
 
 record StrictMonoidal  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) 
         : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
@@ -44,28 +44,53 @@
 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 
-  infixr 9 _⊗_
-  _⊗_ : ( x y : Obj C ) → Obj C
-  _⊗_ x y = FObj BI ( x , y )
+  infixr 9 _□_ _■_
+  _□_ : ( x y : Obj C ) → Obj C
+  _□_ x y = FObj BI ( x , y )
+  _■_ : {a b c d : Obj C } ( f : Hom C a c ) ( g : Hom C b d ) → Hom C ( a □ b ) ( c □ d )
+  _■_ f g = FMap BI ( f , g )
   field
-      mα-iso : {a b c : Obj C} →  Iso C ( ( a ⊗ b) ⊗ c)  ( a ⊗ ( b ⊗ c ) ) 
-      mλ-iso : {a : Obj C} →  Iso C ( I ⊗ a)  a 
-      mσ-iso : {a : Obj C} →  Iso C ( a ⊗ I)  a 
+      mα-iso : {a b c : Obj C} →  Iso C ( ( a □ b) □ c)  ( a □ ( b □ c ) ) 
+      mλ-iso : {a : Obj C} →  Iso C ( I □ a)  a 
+      mρ-iso : {a : Obj C} →  Iso C ( a □ I)  a 
       mα→nat1 : {a a' b c : Obj C} →  ( f : Hom C a a' ) →
-         C [ C [ FMap BI ( f , id1 C ( b ⊗ c ))  o ≅→ (mα-iso {a} {b} {c}) ]  ≈
-            C [   ≅→ (mα-iso )  o FMap BI ( FMap BI (f , id1 C b ) , id1 C c )    ] ]
+         C [ C [ ( f ■ id1 C ( b □ c ))  o ≅→ (mα-iso {a} {b} {c}) ]  ≈
+            C [   ≅→ (mα-iso )  o ( (f ■ id1 C b ) ■ id1 C c )    ] ]
       mα→nat2 : {a b b' c : Obj C} →  ( f : Hom C b b' ) →
-         C [ C [ FMap BI ( id1 C a , FMap BI ( f , id1 C c ) ) o ≅→ (mα-iso {a} {b} {c} ) ]  ≈
-            C [   ≅→ (mα-iso )  o FMap BI ( FMap BI (id1 C a , f )  , id1 C c ) ] ]
+         C [ C [ ( id1 C a ■ ( f ■ id1 C c ) ) o ≅→ (mα-iso {a} {b} {c} ) ]  ≈
+            C [   ≅→ (mα-iso )  o ( (id1 C a ■ f )  ■ id1 C c ) ] ]
       mα→nat3 : {a b c c' : Obj C} →  ( f : Hom C c c' ) →
-         C [ C [ FMap BI ( id1 C a , FMap BI ( id1 C b , f ) ) o ≅→ (mα-iso {a} {b} {c} ) ]  ≈
-            C [   ≅→ (mα-iso )  o FMap BI ( id1 C ( a ⊗ b ) , f ) ] ]
+         C [ C [ ( id1 C a ■ ( id1 C b ■ f ) ) o ≅→ (mα-iso {a} {b} {c} ) ]  ≈
+            C [   ≅→ (mα-iso )  o ( id1 C ( a □ b ) ■ f ) ] ]
       mλ→nat : {a a' : Obj C} →  ( f : Hom C a a' ) →
          C [ C [ f o ≅→ (mλ-iso {a} ) ]  ≈
-            C [   ≅→ (mλ-iso )  o FMap BI ( id1 C I  , f )    ] ]
-      mσ→nat : {a a' : Obj C} →  ( f : Hom C a a' ) →
-         C [ C [ f o ≅→ (mσ-iso {a} ) ]  ≈
-            C [   ≅→ (mσ-iso )  o FMap BI ( f , id1 C I  )    ] ]
+            C [   ≅→ (mλ-iso )  o ( id1 C I  ■ f )    ] ]
+      mρ→nat : {a a' : Obj C} →  ( f : Hom C a a' ) →
+         C [ C [ f o ≅→ (mρ-iso {a} ) ]  ≈
+            C [   ≅→ (mρ-iso )  o ( f ■ id1 C I  )    ] ]
+  αABC□1D : {a b c d e : Obj C } → Hom C (((a □ b) □ c ) □ d) ((a □ (b □ c)) □ d)
+  αABC□1D = {!!}
+  αAB□CD : {a b c d e : Obj C } → Hom C  ((a □ (b □ c)) □ d) (a □ ((b □ c ) □ d))
+  αAB□CD = {!!}
+  1A□BCD : {a b c d e : Obj C } → Hom C  (a □ ((b □ c ) □ d)) (a □ (b □ ( c □ d) ))
+  1A□BCD = {!!}
+  αABC□D : {a b c d e : Obj C } → Hom C  (a □ (b □ ( c □ d) )) ((a □ b ) □ (c □ d))
+  αABC□D = {!!}
+  αA□BCD : {a b c d e : Obj C } → Hom C (((a □ b) □ c ) □ d) ((a □ b ) □ (c □ d))
+  αA□BCD = {!!}
+  αAIB :  {a b  : Obj C } →  Hom C (( a □ I ) □ b ) (a □ ( I □ b ))
+  αAIB = {!!}
+  1A□λB : {a b  : Obj C } →  Hom C  (a □ ( I □ b )) ( a □ b )
+  1A□λB = {!!}
+  ρA□IB : {a b  : Obj C } →  Hom C  (( a □ I ) □ b ) ( a □ b )
+  ρA□IB = {!!}
+
+  field
+      comm-penta : {a b c d e : Obj C}
+         → C [ C [ αABC□D {a} {b} {c} {d} {e} o  C [ 1A□BCD {a} {b} {c} {d} {e} o C [ αAB□CD {a} {b} {c} {d} {e} o αABC□1D {a} {b} {c} {d} {e} ] ] ]
+             ≈ αA□BCD {a} {b} {c} {d} {e} ]
+      comm-unit : {a b : Obj C}
+         → C [ C [ 1A□λB {a} {b} o  αAIB ] ≈ ρA□IB {a} {b} ]
 
 record Monoidal  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) 
         : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
@@ -86,12 +111,16 @@
       ( φ   :  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
+  _⊗_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
+  _□_ : {a b c d : Obj C } ( f : Hom C a c ) ( g : Hom C b d ) → Hom C ( a ⊗ b ) ( c ⊗ d )
+  _□_ f g = FMap (Monoidal.m-bi M) ( f , g )
   _●_ : (x y : Obj D ) → Obj D
-  _●_ x y =  (IsMonoidal._⊗_ (Monoidal.isMonoidal N) ) x y
+  _●_ 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 )
   open Iso
   open Monoidal
-  open IsMonoidal hiding ( _⊗_ )
+  open IsMonoidal 
   α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 ) )
@@ -100,15 +129,39 @@
   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 = {!!}
+  φAB●1 :  {a b c : Obj C} → Hom D  ( ( FObj MF a ●  FObj MF b ) ● FObj MF c ) ( FObj MF ( a ⊗ b ) ● FObj MF c )
+  φAB●1 = {!!}
+  φA⊗BC :  {a b c : Obj C} → Hom D  ( FObj MF ( a ⊗ b ) ● FObj MF c ) (FObj MF ( (a  ⊗  b ) ⊗ c ))
+  φA⊗BC = {!!}
+  FαC : {a b c : Obj C} → Hom D (FObj MF ( (a  ⊗  b ) ⊗ c )) (FObj MF ( a  ⊗ ( b  ⊗ c )))
+  FαC = {!!}
+  1●φ : { a b : Obj C } → Hom D (FObj MF a  ● Monoidal.m-i N ) ( FObj MF a ● FObj  MF ( Monoidal.m-i M ) )
+  1●φ = {!!}
+  φAIC : { a b : Obj C } → Hom D  ( FObj MF a ● FObj  MF ( Monoidal.m-i M ) ) (FObj MF ( a  ⊗ Monoidal.m-i M ))
+  φAIC = {!!}
+  FρC : { a b : Obj C } → Hom D   (FObj MF ( a  ⊗ Monoidal.m-i M ))( FObj MF a  )
+  FρC = {!!}
+  ρD : { a b : Obj C } → Hom D (FObj MF a  ● Monoidal.m-i N ) ( FObj MF a  )
+  ρD = {!!}
+  φ●1 : { a b : Obj C } → Hom D (Monoidal.m-i N ● FObj MF b  ) ( FObj  MF ( Monoidal.m-i M )  ● FObj MF b  )
+  φ●1 = {!!}
+  φICB : { a b : Obj C } → Hom D  ( FObj  MF ( Monoidal.m-i M )  ● FObj MF b  ) ( FObj MF (  ( Monoidal.m-i M )  ⊗ b ) )
+  φICB = {!!}
+  FλD : { a b : Obj C } → Hom D  ( FObj MF (  ( Monoidal.m-i M )  ⊗ b ) ) (FObj MF b ) 
+  FλD = {!!}
+  λD : { a b : Obj C } → Hom D  (Monoidal.m-i N ● FObj MF b  )  (FObj MF b ) 
+  λD = {!!}
   field
-     comm1 : D [ D [ φAB⊗C o D [ 1●φBC o αD ] ]  ≈ {!!} ]
+     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}  ]
 
 record MonoidalFunctor {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 =  (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
   _●_ : (x y : Obj D ) → Obj D
-  _●_ x y =  (IsMonoidal._⊗_ (Monoidal.isMonoidal N) ) x y
+  _●_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y
   field
       MF : Functor C D
   F● :  Functor ( C × C ) D