Mercurial > hg > Members > kono > Proof > category

changeset 769:43138aead09b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 12 Dec 2017 10:57:56 +0900
parents 9bcdbfbaaa39
children e5850e68be22
files applicative.agda monad→monoidal.agda monoidal.agda
diffstat 3 files changed, 88 insertions(+), 52 deletions(-) [+]
line wrap: on
line diff
--- a/applicative.agda	Tue Dec 12 10:25:59 2017 +0900
+++ b/applicative.agda	Tue Dec 12 10:57:56 2017 +0900
@@ -9,11 +9,50 @@
 open import Relation.Binary.Core
 open import Relation.Binary
 open import monoidal
+
+-----
+--
+--  Applicative Functor
+--
+--    is a monoidal functor on Sets and it can be constructoed from Haskell monoidal functor and vais versa
+--
+----
+
+-----
+--
+-- To show Applicative functor is monoidal functor, uniquness of Functor is necessary, which is derived from the free theorem.
+--
+-- they say it is not possible to prove FreeTheorem in Agda nor Coq
+--    https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities
+-- so we postulate this
+--    and we cannot indent a postulate ...
+
+open Functor
+
+postulate FreeTheorem : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') {a b c : Obj C } → (F : Functor C D ) →  ( fmap : {a : Obj C } {b : Obj C } → Hom C a b → Hom D (FObj F a) ( FObj F b) ) →  {h f : Hom C a b } →  {g k : Hom C b c } →  C [  C  [ g o h ]  ≈  C [ k o f ]  ] →  D [ D [ FMap F g o fmap h ]  ≈  D [ fmap k o FMap F f ] ]
+
+UniquenessOfFunctor :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ')  (F : Functor C D)
+  {a b : Obj C } { f : Hom C a b } → ( fmap : {a : Obj C } {b : Obj C } → Hom C a b → Hom D (FObj F a) ( FObj F b) )
+      → ( {b : Obj C } → D [ fmap  (id1 C b) ≈  id1 D (FObj F b) ] )
+      → D [ fmap f ≈  FMap F f ]
+UniquenessOfFunctor C D F {a} {b} {f} fmap eq = begin
+        fmap f 
+     ≈↑⟨ idL ⟩
+        id1 D (FObj F b)  o  fmap f 
+     ≈↑⟨ car ( IsFunctor.identity (isFunctor F )) ⟩
+        FMap F (id1 C b)  o  fmap f 
+     ≈⟨ FreeTheorem C D F  fmap (IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory C ))) ⟩ 
+        fmap  (id1 C b)  o  FMap F f  
+     ≈⟨ car eq ⟩
+        id1 D (FObj F b)  o  FMap F f  
+     ≈⟨ idL ⟩
+        FMap F f 
+     ∎  
+   where open ≈-Reasoning D 
+
 open import Category.Sets
 import Relation.Binary.PropositionalEquality
 
-open Functor
-
 
 _・_ : {c₁ : Level} { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c
 _・_ f g = λ x → f ( g x ) 
@@ -49,10 +88,10 @@
       MF = F
     ; ψ  = λ x → unit
     ; isMonodailFunctor = record {
-             φab  = record { TMap = λ x → φ ; isNTrans = record { commute = comm0 } }
-         ;   associativity  = λ {a b c} → comm1 {a} {b} {c}
-         ;   unitarity-idr = λ {a b} → comm2 {a} {b}
-         ;   unitarity-idl = λ {a b} → comm3 {a} {b}
+             φab  = record { TMap = λ x → φ ; isNTrans = record { commute = φab-comm } }
+         ;   associativity  = λ {a b c} → associativity {a} {b} {c}
+         ;   unitarity-idr = λ {a b} → unitarity-idr {a} {b}
+         ;   unitarity-idl = λ {a b} → unitarity-idl {a} {b}
       }
   } where
       open Monoidal 
@@ -104,9 +143,9 @@
       pureAssoc f g h = trans ( trans (sym comp) (left (left p*p) )) ( left p*p  )
            where
                   open Relation.Binary.PropositionalEquality
-      comm00 : {a b :  Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b}  (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) →
+      φab-comm0 : {a b :  Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b}  (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) →
          (Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]) x ≡ (Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ]) x
-      comm00 {a} {b} {(f , g)} (x , y) = begin
+      φab-comm0 {a} {b} {(f , g)} (x , y) = begin
                  ( FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) ( φ (x , y) )
              ≡⟨⟩
                  FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) ((FMap F (λ j k → j , k) x) <*> y)
@@ -148,12 +187,12 @@
            where
                   open Relation.Binary.PropositionalEquality
                   open Relation.Binary.PropositionalEquality.≡-Reasoning
-      comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ  ]
+      φab-comm : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ  ]
         ≈ Sets [ φ  o FMap (Functor● Sets Sets MonoidalSets F) f ] ]
-      comm0 {a} {b} {f} =  extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → comm00 x )
-      comm10 :  {a b c : Obj Sets} → (x : ((FObj F a ⊗ FObj F b) ⊗ FObj F c) ) → (Sets [ φ  o Sets [ id1 Sets (FObj F a) □ φ  o Iso.≅→ (mα-iso isM) ] ]) x ≡
+      φab-comm {a} {b} {f} =  extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → φab-comm0 x )
+      associativity0 :  {a b c : Obj Sets} → (x : ((FObj F a ⊗ FObj F b) ⊗ FObj F c) ) → (Sets [ φ  o Sets [ id1 Sets (FObj F a) □ φ  o Iso.≅→ (mα-iso isM) ] ]) x ≡
                 (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ  o φ  □ id1 Sets (FObj F c) ] ]) x
-      comm10 {x} {y} {f} ((a , b) , c ) = begin
+      associativity0 {x} {y} {f} ((a , b) , c ) = begin
                   φ  (( id □ φ  ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c)))
                ≡⟨⟩
                  (FMap F (λ j k → j , k) a) <*> ( (FMap F (λ j k → j , k) b) <*> c)
@@ -212,14 +251,14 @@
            where
                   open Relation.Binary.PropositionalEquality
                   open Relation.Binary.PropositionalEquality.≡-Reasoning
-      comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ 
+      associativity : {a b c : Obj Sets} → Sets [ Sets [ φ 
            o Sets [  (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ]
         ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ  o  (φ  □ id1 Sets (FObj F c)) ] ] ]
-      comm1 {a} {b} {c} =  extensionality Sets ( λ x  → comm10 x )
-      comm20 : {a b : Obj Sets} ( x : FObj F a * One )  → (  Sets [
+      associativity {a} {b} {c} =  extensionality Sets ( λ x  → associativity0 x )
+      unitarity-idr0 : {a b : Obj Sets} ( x : FObj F a * One )  → (  Sets [
          FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ  o
              FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x  ≡ Iso.≅→ (mρ-iso isM) x
-      comm20 {a} {b} (x , OneObj ) =  begin 
+      unitarity-idr0 {a} {b} (x , OneObj ) =  begin 
                  (FMap F (Iso.≅→ (mρ-iso isM))) ( φ ((  FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit))) (x , OneObj) ))
                ≡⟨⟩
                  FMap F proj₁ ((FMap F (λ j k → j , k) x) <*> (pure OneObj))
@@ -243,14 +282,14 @@
            where
                   open Relation.Binary.PropositionalEquality
                   open Relation.Binary.PropositionalEquality.≡-Reasoning
-      comm2 : {a b : Obj Sets} → Sets [ Sets [
+      unitarity-idr : {a b : Obj Sets} → Sets [ Sets [
          FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ  o
              FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ]
-      comm2 {a} {b} =  extensionality Sets ( λ x  → comm20 {a} {b} x )
-      comm30 : {a b : Obj Sets} ( x : One * FObj F b )  → (  Sets [
+      unitarity-idr {a} {b} =  extensionality Sets ( λ x  → unitarity-idr0 {a} {b} x )
+      unitarity-idl0 : {a b : Obj Sets} ( x : One * FObj F b )  → (  Sets [
          FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ  o
              FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x  ≡ Iso.≅→ (mλ-iso isM) x
-      comm30 {a} {b} ( OneObj , x) =  begin 
+      unitarity-idl0 {a} {b} ( OneObj , x) =  begin 
                  (FMap F (Iso.≅→ (mλ-iso isM))) ( φ  ( unit , x ) )
                ≡⟨⟩
                   FMap F proj₂ ((FMap F (λ j k → j , k) (pure OneObj)) <*> x)
@@ -270,9 +309,9 @@
            where
                   open Relation.Binary.PropositionalEquality
                   open Relation.Binary.PropositionalEquality.≡-Reasoning
-      comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o
+      unitarity-idl : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o
         Sets [ φ  o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ]
-      comm3 {a} {b} =  extensionality Sets ( λ x  → comm30 {a} {b} x )
+      unitarity-idl {a} {b} =  extensionality Sets ( λ x  → unitarity-idl0 {a} {b} x )
 
 ----
 --
@@ -489,7 +528,8 @@
 
 ----
 --
--- Applicative laws imples Monoidal laws
+-- Applicative functor implements Haskell Monoidal functor  
+--    Haskell Monoidal functor is directly represents monoidal functor, it is easy to make it from a monoidal functor
 --
 
 Applicative→HaskellMonoidal : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
@@ -538,4 +578,4 @@
           idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (IsMonoidal.mλ-iso isM)) (φ (unit , x)) ≡ x
           idlφ {a} {x} =  ≡-cong ( λ h → h (OneObj , x ) ) ( IsMonoidalFunctor.unitarity-idl isMF {One} {a}  )
 
-
+-- end
--- a/monad→monoidal.agda	Tue Dec 12 10:25:59 2017 +0900
+++ b/monad→monoidal.agda	Tue Dec 12 10:57:56 2017 +0900
@@ -15,11 +15,15 @@
 open import monoidal 
 open import applicative 
 open import Category.Cat
-
-
 open import Category.Sets
 import Relation.Binary.PropositionalEquality
 
+-----
+--
+--  Monad on Sets implies Applicative and Haskell Monidal Functor
+--
+--
+
 Monad→HaskellMonoidalFunctor : {l : Level } (m : Monad (Sets {l} ) ) → HaskellMonoidalFunctor ( Monad.T m )
 Monad→HaskellMonoidalFunctor {l} monad = record {
          unit = unit
@@ -441,5 +445,9 @@
              where
                   open ≈-Reasoning Sets hiding ( _o_ )
 
+-- an easy one ( we already have HaskellMonoidal→Applicative )
+
+Monad→Applicative' : {l : Level } (m : Monad (Sets {l} ) ) → Applicative ( Monad.T m )
+Monad→Applicative' {l} m =  HaskellMonoidal→Applicative ( Monad.T m ) (  Monad→HaskellMonoidalFunctor m )
 
 -- end
--- a/monoidal.agda	Tue Dec 12 10:25:59 2017 +0900
+++ b/monoidal.agda	Tue Dec 12 10:57:56 2017 +0900
@@ -263,31 +263,6 @@
       ψ  : Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) )
       isMonodailFunctor : IsMonoidalFunctor  M N MF ψ
 
------
--- they say it is not possible to prove FreeTheorem in Agda nor Coq
---    https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities
--- so we postulate this
---    and we cannot indent postulate ...
-postulate FreeTheorem : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') {a b c : Obj C } → (F : Functor C D ) →  ( fmap : {a : Obj C } {b : Obj C } → Hom C a b → Hom D (FObj F a) ( FObj F b) ) →  {h f : Hom C a b } →  {g k : Hom C b c } →  C [  C  [ g o h ]  ≈  C [ k o f ]  ] →  D [ D [ FMap F g o fmap h ]  ≈  D [ fmap k o FMap F f ] ]
-
-UniquenessOfFunctor :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ')  (F : Functor C D)
-  {a b : Obj C } { f : Hom C a b } → ( fmap : {a : Obj C } {b : Obj C } → Hom C a b → Hom D (FObj F a) ( FObj F b) )
-      → ( {b : Obj C } → D [ fmap  (id1 C b) ≈  id1 D (FObj F b) ] )
-      → D [ fmap f ≈  FMap F f ]
-UniquenessOfFunctor C D F {a} {b} {f} fmap eq = begin
-        fmap f 
-     ≈↑⟨ idL ⟩
-        id1 D (FObj F b)  o  fmap f 
-     ≈↑⟨ car ( IsFunctor.identity (isFunctor F )) ⟩
-        FMap F (id1 C b)  o  fmap f 
-     ≈⟨ FreeTheorem C D F  fmap (IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory C ))) ⟩ 
-        fmap  (id1 C b)  o  FMap F f  
-     ≈⟨ car eq ⟩
-        id1 D (FObj F b)  o  FMap F f  
-     ≈⟨ idL ⟩
-        FMap F f 
-     ∎  
-   where open ≈-Reasoning D 
 
 open import Category.Sets
 
@@ -366,6 +341,12 @@
 
 ≡-cong = Relation.Binary.PropositionalEquality.cong 
 
+----
+--
+--  HaskellMonoidalFunctor is a monoidal functor on Sets
+--
+--
+
 
 record IsHaskellMonoidalFunctor {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
       ( unit  : FObj F One )
@@ -396,6 +377,13 @@
       φ    : {a b : Obj Sets} → Hom Sets ((FObj F a) *  (FObj F b )) ( FObj F ( a * b ) )
       isHaskellMonoidalFunctor : IsHaskellMonoidalFunctor F unit φ
 
+
+----
+--
+--  laws of HaskellMonoidalFunctor are directly mapped to the laws of Monoidal Functor
+--
+--
+
 HaskellMonoidalFunctor→MonoidalFunctor :  {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : HaskellMonoidalFunctor F )
    → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
 HaskellMonoidalFunctor→MonoidalFunctor {c} F mf = record {
@@ -493,4 +481,4 @@
         Sets [ φ  o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ]
       comm3 {a} {b} =  extensionality Sets ( λ x  → comm30 {a} {b} x )
 
-
+-- end