Mercurial > hg > Members > kono > Proof > category

changeset 731:117e5b392673

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Generalize Free Theorem
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 27 Nov 2017 14:42:49 +0900
parents e4ef69bae044
children 2439a142aba2
files cat-utility.agda monoidal.agda
diffstat 2 files changed, 44 insertions(+), 34 deletions(-) [+]
line wrap: on
line diff
--- a/cat-utility.agda	Sun Nov 26 21:57:41 2017 +0900
+++ b/cat-utility.agda	Mon Nov 27 14:42:49 2017 +0900
@@ -13,6 +13,16 @@
         id1 A a =  (Id {_} {_} {_} {A} a)
         -- We cannot make A implicit
 
+        record Iso  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ)
+                 (x y : Obj C )
+                : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
+           field
+                 ≅→ :  Hom C x y
+                 ≅← :  Hom C y x
+                 iso→  :  C [ C [ ≅← o ≅→  ] ≈  id1 C x ]
+                 iso←  :  C [ C [ ≅→ o ≅←  ] ≈  id1 C y ]
+
+
         record IsUniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                          ( U : Functor B A )
                          ( F : Obj A → Obj B )
--- a/monoidal.agda	Sun Nov 26 21:57:41 2017 +0900
+++ b/monoidal.agda	Mon Nov 27 14:42:49 2017 +0900
@@ -11,14 +11,14 @@
 
 open Functor
 
-record Iso  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) 
-         (x y : Obj C )
-        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
-   field
-         ≅→ :  Hom C x y 
-         ≅← :  Hom C y x 
-         iso→  :  C [ C [ ≅← o ≅→  ] ≈  id1 C x ]
-         iso←  :  C [ C [ ≅→ o ≅←  ] ≈  id1 C y ]
+-- record Iso  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) 
+--          (x y : Obj C )
+--         : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
+--    field
+--          ≅→ :  Hom C x y 
+--          ≅← :  Hom C y x 
+--          iso→  :  C [ C [ ≅← o ≅→  ] ≈  id1 C x ]
+--          iso←  :  C [ C [ ≅→ o ≅←  ] ≈  id1 C y ]
 
 -- Monoidal Category
 
@@ -263,6 +263,31 @@
       ψ  : 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
 
 import Relation.Binary.PropositionalEquality
@@ -511,7 +536,6 @@
      <*> :   {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b  
      <*> {a} {b} x y = FMap F ( λ r →  ( proj₁ r )  ( proj₂  r ) )  (φ mono ( x , y ))
 
-
 ------
 --
 -- Appllicative Functor is a Monoidal Functor
@@ -562,34 +586,10 @@
            where
                   open Relation.Binary.PropositionalEquality
                   open Relation.Binary.PropositionalEquality.≡-Reasoning
-      -----
-      -- 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 : {l : Level } {a b c : Obj (Sets {l}) } → (F : Functor (Sets {l}) (Sets {l} ) ) →  ( fmap : {a : Obj Sets } {b : Obj Sets } → Hom Sets a b → Hom Sets (FObj F a) ( FObj F b) ) →  {h f : Hom Sets a b } →  {g k : Hom Sets b c } →  Sets [  g o h  ≈  k o f  ] →  Sets [ FMap F g o fmap h  ≈  fmap k o FMap F f  ]
-      UniquenessOfFunctor :   (F : Functor Sets Sets)
-          {a b : Obj Sets } { f : Hom Sets a b } → ( fmap : {a : Obj Sets } {b : Obj Sets } → Hom Sets a b → Hom Sets (FObj F a) ( FObj F b) )
-              → ( {b : Obj Sets } → Sets [ fmap  (id1 Sets b) ≈  id1 Sets (FObj F b) ] )
-              → Sets [ fmap f ≈  FMap F f ]
-      UniquenessOfFunctor F {a} {b} {f} fmap eq = begin
-                fmap f 
-             ≈↑⟨ idL ⟩
-                id1 Sets (FObj F b)  o  fmap f 
-             ≈↑⟨ car ( IsFunctor.identity (isFunctor F )) ⟩
-                FMap F (id1 Sets b)  o  fmap f 
-             ≈⟨ FreeTheorem F  fmap refl-hom ⟩ 
-                fmap  (id1 Sets b)  o  FMap F f  
-             ≈⟨ car eq ⟩
-                id1 Sets (FObj F b)  o  FMap F f  
-             ≈⟨ idL ⟩
-                FMap F f 
-             ∎  
-           where open ≈-Reasoning Sets hiding ( _o_ )
       F→pure : {a b : Obj Sets } → { f : a → b } → {x : FObj F a } →  FMap F f x ≡ pure f <*> x
       F→pure {a} {b} {f} {x} = sym ( begin
                  pure f <*> x
-             ≡⟨ ≡-cong ( λ k → k x ) (UniquenessOfFunctor F ( λ f x → pure f <*> x ) ( extensionality Sets ( λ x →  IsApplicative.identity ismf  ))) ⟩
+             ≡⟨ ≡-cong ( λ k → k x ) (UniquenessOfFunctor Sets Sets F ( λ f x → pure f <*> x ) ( extensionality Sets ( λ x →  IsApplicative.identity ismf  ))) ⟩
                  FMap F f x
              ∎ )
            where