Mercurial > hg > Members > kono > Proof > category

changeset 705:73a998711118

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add Applicative and HaskellMonoidal Functor
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 22 Nov 2017 11:51:34 +0900
parents b48c2d1c0796
children dad072d52d0e
files monoidal.agda
diffstat 1 files changed, 82 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/monoidal.agda	Wed Nov 22 04:42:48 2017 +0900
+++ b/monoidal.agda	Wed Nov 22 11:51:34 2017 +0900
@@ -68,6 +68,7 @@
       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  )    ] ]
+      -- we should write naturalities for ≅← (maybe derived from above )
   αABC□1D : {a b c d e : Obj C } → Hom C (((a □ b) □ c ) □ d) ((a □ (b □ c)) □ d)
   αABC□1D {a} {b} {c} {d} {e} = (  ≅→ mα-iso  ■ id1 C d )
   αAB□CD : {a b c d e : Obj C } → Hom C  ((a □ (b □ c)) □ d) (a □ ((b □ c ) □ d))
@@ -99,11 +100,37 @@
       m-bi : Functor ( C × C ) C 
       isMonoidal : IsMonoidal C m-i m-bi
 
+---------
+--
+--  Lax Monoidal Functor
+--
+--    N → M
+--
+---------
+
+---------
+--
+-- Two implementations of Functor ( C × C ) → D from F : Functor C → D (given)
+--        dervied from F and two Monoidal Categories
+--
+--     F x ● F y
+--     F ( x ⊗  y )
+--
+-- and a given natural transformation for them 
+--
+--      φ : F x ● F y  → F ( x ⊗  y )
+--
+--      TMap φ : ( x y : Obj C ) →  Hom D ( F x ● F y ) ( F ( x ⊗ y ))
+--
+-- a given unit arrow
+--
+--      ψ : IN → IM
+
 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)  )
+     ; FMap = λ {x : Obj ( C × C ) } {y} f →  (  FMap MF  (proj₁  f ) ■ FMap MF (proj₂ f)  )
      ; isFunctor = record {
              ≈-cong   = ≈-cong
              ; identity = identity
@@ -147,7 +174,7 @@
       ( 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 →  F ( FMap (Monoidal.m-bi M) (  proj₁ f , proj₂ f) )
+     ; FMap = λ {a} {b} f →  F ( proj₁ f □ proj₂ f )
      ; isFunctor = record {
              ≈-cong   = ≈-cong
              ; identity = identity
@@ -244,17 +271,64 @@
   λ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}  ]
+     associativity : {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 ] ] ]
+     unitarity-idr : {a b : Obj C } → D [ D [ FρC  {a} {b}  o D [ φAIC {a} {b} o  1●ψ{a} {b} ] ]  ≈ ρD {a} {b}  ]
+     unitarity-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
+  field
+      MF : Functor C D
+      ψ  : Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) )
+      isMonodailFunctor : IsMonoidalFunctor  M N MF ψ
+
+record MonoidalFunctorWithoutCommutativities {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 : Obj D ) → Obj D
   _●_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y
   field
-      MF : Functor C D
-      ψ  : Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) )
-      isMonodailFunctor : IsMonoidalFunctor  M N MF ψ
+      MF    : Functor C D
+      unit  : Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) )
+      **    : {a b : Obj C} → Hom D ((FObj MF a) ●  (FObj MF b )) ( FObj MF ( a ⊗ b ) )
+
+open import Category.Sets
+
+data One {c : Level} : Set c where
+  OneObj : One   -- () in Haskell ( or any one object set )
+
+record HaskellMonoidalFunctor {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
+        : Set (suc (suc c₁)) where
+  field
+      unit  : Hom (Sets {c₁}) One One
+      φ    : {a b : Obj Sets} → Hom Sets ((FObj f a) *  (FObj f b )) ( FObj f ( a * b ) )
+      iso  : {a : Obj Sets} → Iso Sets One {!!}
+  **    : {a b : Obj Sets} → FObj f a →  FObj f b →  FObj f ( a * b ) 
+  ** x y  = φ ( x , y )
+
+--  HaskellMonoidalFunctor f → MonoidalFunctor
+
+record Applicative {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
+        : Set (suc (suc c₁)) where
+  field
+      pure  : {a : Obj Sets} → Hom Sets a ( FObj f a )
+      <*>   : {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b
+
+lemma1 : {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) → Applicative f → HaskellMonoidalFunctor f
+lemma1 f app = record { unit = unit ; φ = φ }
+  where
+     open Applicative
+     unit  :  Hom Sets One One
+     unit OneObj = OneObj
+     φ :  {a b : Obj Sets} → Hom Sets ((FObj f a) *  (FObj f b )) ( FObj f ( a * b ) )
+     φ {a} {b} ( x , y ) = <*> app {!!} {!!}
+
+lemma2 : {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) → HaskellMonoidalFunctor f → Applicative f 
+lemma2 f app = record { pure = pure ; <*> = <*> }
+  where
+     open HaskellMonoidalFunctor
+     pure  :  {a : Obj Sets} → Hom Sets a ( FObj f a )
+     pure {a} x = {!!}
+     <*> :   {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b
+     <*> {a} {b} x = {!!}