Mercurial > hg > Members > kono > Proof > category

changeset 342:a9711cf75a12

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
free-monoid fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 18 Apr 2014 16:58:54 +0900
parents 33bc037319fa
children d8cb7f9c7980
files free-monoid.agda
diffstat 1 files changed, 52 insertions(+), 37 deletions(-) [+]
line wrap: on
line diff
--- a/free-monoid.agda	Thu Apr 17 13:42:57 2014 +0900
+++ b/free-monoid.agda	Fri Apr 18 16:58:54 2014 +0900
@@ -12,11 +12,30 @@
 open import HomReasoning
 open import cat-utility
 open import Relation.Binary.Core
-open import  Relation.Binary.PropositionalEquality
 open import universal-mapping 
+open import  Relation.Binary.PropositionalEquality 
 
 -- from https://github.com/danr/Agda-projects/blob/master/Category-Theory/FreeMonoid.agda
 
+open import Algebra.FunctionProperties using (Op₁; Op₂)
+open import Algebra.Structures
+open import Data.Product
+
+
+record ≡-Monoid : Set (suc c) where
+  infixr 9 _∙_
+  field
+    Carrier  : Set c
+    _∙_      : Op₂ Carrier
+    ε        : Carrier
+    isMonoid : IsMonoid _≡_ _∙_ ε
+
+open ≡-Monoid
+
+≡-cong = Relation.Binary.PropositionalEquality.cong 
+
+-- module ≡-reasoning (m : ≡-Monoid ) where
+
 infixr 40 _::_
 data  List  (A : Set c ) : Set c where
    [] : List A
@@ -28,8 +47,6 @@
 []        ++ ys = ys
 (x :: xs) ++ ys = x :: (xs ++ ys)
 
-≡-cong = Relation.Binary.PropositionalEquality.cong 
-
 list-id-l : { A : Set c } → { x : List A } →  [] ++ x ≡ x
 list-id-l {_} {_} = refl
 list-id-r : { A : Set c } → { x : List A } →  x ++ [] ≡ x
@@ -50,26 +67,17 @@
      ; trans = trans
      } 
 
-open import Algebra.FunctionProperties using (Op₁; Op₂)
-open import Algebra.Structures
-open import Data.Product
-
 
-record ≡-Monoid : Set (suc c) where
-  infixl 7 _∙_
-  field
-    Carrier  : Set c
-    _∙_      : Op₂ Carrier
-    ε        : Carrier
-    isMonoid : IsMonoid _≡_ _∙_ ε
+_<_∙_> :  (m : ≡-Monoid)  →   Carrier m → Carrier m → Carrier m
+m < x ∙ y > = _∙_ m x y
 
-open ≡-Monoid
+infixr 9 _<_∙_>
 
 record Monomorph ( a b : ≡-Monoid )  : Set (suc c) where
   field
       morph : Carrier a → Carrier b  
       identity     :  morph (ε a)  ≡  ε b
-      homo :  ∀{x y} → morph ( _∙_ a x  y ) ≡ ( _∙_ b (morph  x ) (morph  y) )
+      homo :  ∀{x y} → morph ( a < x ∙ y > ) ≡ b < morph  x  ∙ morph  y >
 
 open Monomorph
 
@@ -80,14 +88,21 @@
       homo  = homo1 
    } where
       identity1 : morph f ( morph g (ε a) )  ≡  ε c
-      -- morph f (ε b) = ε c ,  morph g (ε a) ) ≡  ε b
-      -- morph f  morph g (ε a) ) ≡  morph f (ε b) = ε c
-      identity1 = trans ( ≡-cong (morph f ) ( identity g ) )  ( identity f )
-      homo1 :  ∀{x y} → morph f ( morph g ( _∙_ a x  y )) ≡ ( _∙_ c (morph f (morph  g x )) (morph f (morph  g y) ) )
-      --  ∀{x y} → morph f ( morph g ( _∙_ a x  y )) ≡ morph f ( ( _∙_ c  (morph  g x )) (morph  g y) ) 
-      --  ∀{x y} → morph f ( ( _∙_ c  (morph  g x )) (morph  g y) )  
-      --         ≡ ( _∙_ c (morph f (morph  g x )) (morph f (morph  g y) ) )
-      homo1 = trans  (≡-cong (morph f ) ( homo g) ) ( homo f ) 
+      identity1 = let open ≡-Reasoning in begin
+             morph f (morph g (ε a))
+         ≡⟨  ≡-cong (morph f ) ( identity g )  ⟩
+             morph f (ε b)
+         ≡⟨  identity f  ⟩
+             ε c
+         ∎ 
+      homo1 :  ∀{x y} → morph f ( morph g ( a < x ∙  y > )) ≡ ( c <   (morph f (morph  g x )) ∙(morph f (morph  g y) ) > )
+      homo1 {x} {y} = let open ≡-Reasoning in begin
+             morph f (morph g (a < x ∙ y >))
+         ≡⟨  ≡-cong (morph f ) ( homo g) ⟩
+             morph f (b < morph g x ∙ morph g y >)
+         ≡⟨  homo f ⟩
+              c < morph f (morph g x) ∙ morph f (morph g y) >
+         ∎ 
 
 M-id : { a : ≡-Monoid } → Monomorph a a 
 M-id = record { morph = λ x → x  ; identity = refl ; homo = refl }
@@ -142,7 +157,7 @@
 list  : (a : Set c) → ≡-Monoid
 list a = record {
     Carrier    =  List a
-    ; _∙_      = _++_
+    ;  _∙_ = _++_
     ; ε        = []
     ; isMonoid = record {
           identity = ( ( λ x → list-id-l {a}  ) , ( λ x → list-id-r {a} ) ) ;
@@ -164,7 +179,7 @@
 --   [a,b,c] → f(a) ∙ f(b) ∙ f(c)
 Φ :  {a : Obj A } {b : Obj B} ( f : Hom A a (FObj U b) ) →  List a → Carrier b
 Φ {a} {b} f [] = ε b
-Φ {a} {b} f ( x :: xs ) = _∙_ b  ( f x ) (Φ {a} {b} f xs )
+Φ {a} {b} f ( x :: xs ) = b < ( f x ) ∙ (Φ {a} {b} f xs ) >
 
 solution : (a : Obj A ) (b : Obj B) ( f : Hom A a (FObj U b) ) →  Hom B (Generator a ) b 
 solution a b f = record {
@@ -173,8 +188,8 @@
          homo = λ {x y} → homo1 x y 
     } where
         _*_ : Carrier b → Carrier b → Carrier b
-        _*_  f g = _∙_ b f g
-        homo1 : (x y : Carrier (Generator a)) → Φ f ((Generator a ∙ x) y) ≡ (b ∙ Φ f x) (Φ {a} {b} f y)
+        _*_  f g = b <  f ∙ g >
+        homo1 : (x y : Carrier (Generator a)) → Φ f ( (Generator a) < x ∙  y > ) ≡ (Φ f x) * (Φ {a} {b} f y )
         homo1 [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ f y))
         homo1 (x :: xs) y = let open ≡-Reasoning in 
              sym ( begin
@@ -190,7 +205,7 @@
              ≡⟨⟩
                 Φ {a} {b} f ( (x ::  xs) ++ y ) 
              ≡⟨⟩
-                Φ {a} {b} f ((Generator a ∙ x :: xs) y) 
+                Φ {a} {b} f ((Generator a) < ( x :: xs) ∙ y > ) 
              ∎ )
 
 eta :  (a : Obj A) → Hom A a ( FObj U (Generator a) )
@@ -218,15 +233,15 @@
                      ≡⟨⟩
                          ( λ (x : a ) → Φ {a} {b} f ( x :: [] ) )
                      ≡⟨⟩
-                         ( λ (x : a ) →  _∙_ b  ( f x ) (Φ {a} {b} f [] ) )
+                         ( λ (x : a ) →  b < ( f x ) ∙ (Φ {a} {b} f [] ) > )
                      ≡⟨⟩
-                         ( λ (x : a ) →  _∙_ b  ( f x ) ( ε b ) )
+                         ( λ (x : a ) →  b <    ( f x ) ∙ ( ε b ) > )
                      ≡⟨ ≡-cong ( λ  g → ( ( λ (x : a ) →  g x ) )) (extensionality {a} lemma-ext1) ⟩
                          ( λ (x : a ) →  f x  )
                      ≡⟨⟩
                           f
                      ∎  where
-                        lemma-ext1 : ∀( x : a ) →  _∙_ b  ( f x ) ( ε b )  ≡ f x
+                        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 ]
@@ -246,17 +261,17 @@
                              begin
                                 (morph ( solution a b f)) ( x :: xs )
                              ≡⟨ homo ( solution a b f) {x :: []} {xs} ⟩
-                                 _∙_ b ((morph ( solution a b f)) ( x :: []) )  ((morph ( solution a b f)) xs )
-                             ≡⟨  ≡-cong ( λ  k → (_∙_ b ((morph ( solution a b f)) ( x :: []) ) k )) (lemma-ext2 xs )   ⟩
-                                 _∙_ b ((morph ( solution a b f)) ( x :: []) )  ((morph g) ( xs ))
-                             ≡⟨  ≡-cong ( λ k → ( _∙_ b ( k x ) ((morph g) ( xs )) )) (
+                                 b <   ((morph ( solution a b f)) ( x :: []) ) ∙ ((morph ( solution a b f)) xs ) >
+                             ≡⟨  ≡-cong ( λ  k → (b <   ((morph ( solution a b f)) ( x :: []) ) ∙ k > )) (lemma-ext2 xs )   ⟩
+                                 b <   ((morph ( solution a b f)) ( x :: []) )  ∙((morph g) ( xs )) >
+                             ≡⟨  ≡-cong ( λ k → ( b <   ( k x ) ∙ ((morph g) ( xs )) >  )) (
                                  begin
                                      ( λ x → (morph ( solution a b f)) ( x :: [] ) )
                                  ≡⟨ extensionality {a} lemma-ext3 ⟩
                                      ( λ x → (morph g) ( x :: [] ) )
                                  ∎  
                              ) ⟩
-                                 _∙_ b ((morph g) ( x :: [] )) ((morph g) ( xs ))
+                                 b <   ((morph g) ( x :: [] )) ∙((morph g) ( xs )) >
                              ≡⟨ sym ( homo g ) ⟩
                                 (morph g) ( x :: xs )
                              ∎   where