Mercurial > hg > Members > kono > Proof > category

changeset 162:18ab1be1ebb5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
mapping done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 19 Aug 2013 12:34:08 +0900
parents ffeb33698173
children bc47179e3c9c
files free-monoid.agda
diffstat 1 files changed, 35 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/free-monoid.agda	Mon Aug 19 05:05:04 2013 +0900
+++ b/free-monoid.agda	Mon Aug 19 12:34:08 2013 +0900
@@ -1,5 +1,7 @@
 -- {-# OPTIONS --universe-polymorphism #-}
 
+-- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
+
 open import Category -- https://github.com/konn/category-agda                                                                                     
 open import Level
 module free-monoid { c c₁ c₂ ℓ : Level }   where
@@ -11,7 +13,7 @@
 open import Relation.Binary.Core
 open import  Relation.Binary.PropositionalEquality
 
-
+-- from https://github.com/danr/Agda-projects/blob/master/Category-Theory/FreeMonoid.agda
 
 infixr 40 _::_
 data  List  (A : Set c ) : Set c where
@@ -117,7 +119,6 @@
          ; isCategory = isMonoidCategory 
            }
 
-
 A = Sets {c}
 B = MonoidCategory  
 
@@ -135,7 +136,6 @@
    } 
 
 -- FObj 
-
 list  : (a : Set c) -> ≡-Monoid
 list a = record {
     Carrier    =  List a
@@ -154,10 +154,6 @@
 Generator : Obj A -> Obj B
 Generator s =  list s
 
--- η
-
-postulate eta :  (a : Obj A) → Hom A a ( FObj U (Generator a) )
-
 -- solution
 
 open UniversalMapping
@@ -170,19 +166,21 @@
 solution a b f = record {
          morph = \(l : List a) -> Φ l   ;
          identity = refl ;
-         mdistr = \{x y} -> lemma-fm-1 x y 
+         mdistr = \{x y} -> mdistr1 x y 
     } where
-        lemma-fm-1 : (x y : Carrier (Generator a)) → Φ ((Generator a ∙ x) y) ≡ (b ∙ Φ x) (Φ y)
-        lemma-fm-1 [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ y))
-        lemma-fm-1 (x :: xs) y = let open ≡-Reasoning in 
+        _*_ : Carrier b -> Carrier b -> Carrier b
+        _*_  f g = _∙_ b f g
+        mdistr1 : (x y : Carrier (Generator a)) → Φ ((Generator a ∙ x) y) ≡ (b ∙ Φ x) (Φ y)
+        mdistr1 [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ y))
+        mdistr1 (x :: xs) y = let open ≡-Reasoning in 
              sym ( begin
-                _∙_ b  (Φ {a} {b} {f} (x :: xs)) (Φ {a} {b} {f} y)
+                (Φ {a} {b} {f} (x :: xs)) * (Φ {a} {b} {f} y)
              ≡⟨⟩
-                _∙_ b ( _∙_ b (f x) (Φ {a} {b} {f} xs)) (Φ {a} {b} {f} y)
+                 ((f x) * (Φ {a} {b} {f} xs)) * (Φ {a} {b} {f} y)
              ≡⟨ ( IsMonoid.assoc ( isMonoid b )) _ _ _ ⟩
-                _∙_ b (f x) ( _∙_ b  (Φ {a} {b} {f} xs) (Φ {a} {b} {f} y) )
-             ≡⟨ sym ( (IsMonoid.∙-cong (isMonoid b)) refl (lemma-fm-1 xs y )) ⟩
-                _∙_ b (f x) ( Φ {a} {b} {f} ( xs ++ y ) )
+                (f x) * ( (Φ {a} {b} {f} xs)  * (Φ {a} {b} {f} y) )
+             ≡⟨ sym ( (IsMonoid.∙-cong (isMonoid b)) refl (mdistr1 xs y )) ⟩
+                (f x) * ( Φ {a} {b} {f} ( xs ++ y ) )
              ≡⟨⟩
                 Φ {a} {b} {f} ( x :: ( xs ++ y ) )
              ≡⟨⟩
@@ -191,8 +189,14 @@
                 Φ {a} {b} {f} ((Generator a ∙ x :: xs) y) 
              ∎ )
 
+eta :  (a : Obj A) → Hom A a ( FObj U (Generator a) )
+eta  a = \( x : a ) ->  x :: []
+
+-- Functional Extensionarity Axiom (We cannot prove this in Agda / Coq, just assumming )
+postulate Extensionarity : { a b : Obj A } {f g : Hom A a b } → (∀ {x} → (f x ≡ g x))  → ( f ≡ g ) 
+
 FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta  
-FreeMonoidUniveralMapping  = 
+FreeMonoidUniveralMapping = 
     record {
        _* = \{a b} -> \f -> solution a b f ; 
        isUniversalMapping = record {
@@ -205,10 +209,20 @@
                      begin
                          FMap U ( solution a b f ) o eta a   
                      ≡⟨⟩
-                         ( λ x → Φ (eta a x) )
-                     ≡⟨ {!!} ⟩
-                         f
-                     ∎ 
+                         ( λ (x : a ) → Φ {a} {b} {f} (eta a x) )
+                     ≡⟨⟩
+                         ( λ (x : a ) → Φ {a} {b} {f} ( x :: [] ) )
+                     ≡⟨⟩
+                         ( λ (x : a ) →  _∙_ b  ( f x ) (Φ {a} {b} {f} [] ) )
+                     ≡⟨⟩
+                         ( λ (x : a ) →  _∙_ b  ( f x ) ( ε b ) )
+                     ≡⟨ ≡-cong ( \ g -> ( ( λ (x : a ) →  g x ) )) (Extensionarity lemma-ext1) ⟩
+                         ( λ (x : a ) →  f x  )
+                     ≡⟨⟩
+                          f
+                     ∎  where
+                        lemma-ext1 : ∀{ x : a } ->  _∙_ b  ( f x ) ( ε b )  ≡ f x
+                        lemma-ext1 {x} = ( proj₂ ( IsMonoid.identity ( isMonoid b) ) ) (f x)
         uniquness :  {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } →
              { g :  Hom B (Generator a) b } → (FMap U g) o (eta a )  ≡ f  → B [ solution a b f ≈ g ]
         uniquness = {!!}