Mercurial > hg > Members > kono > Proof > category

changeset 168:a9b4132d619b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 20 Aug 2013 17:57:22 +0900
parents c3863043c4a3
children 44bf6e78f891
files HomReasoning.agda free-monoid.agda list-monoid-cat.agda monoid-monad.agda
diffstat 4 files changed, 37 insertions(+), 39 deletions(-) [+]
line wrap: on
line diff
--- a/HomReasoning.agda	Mon Aug 19 18:14:19 2013 +0900
+++ b/HomReasoning.agda	Tue Aug 20 17:57:22 2013 +0900
@@ -117,6 +117,7 @@
 
   infixr  2 _∎
   infixr 2 _≈⟨_⟩_ _≈⟨⟩_ 
+  infixr 2 _≈↑⟨_⟩_ 
   infix  1 begin_
 
 ------ If we have this, for example, as an axiom of a category, we can use ≡-Reasoning directly
@@ -135,6 +136,10 @@
            x ≈ y → y IsRelatedTo z → x IsRelatedTo z
   _ ≈⟨ x≈y ⟩ relTo y≈z = relTo (trans-hom x≈y y≈z)
 
+  _≈↑⟨_⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } → 
+           y ≈ x → y IsRelatedTo z → x IsRelatedTo z
+  _ ≈↑⟨ y≈x ⟩ relTo y≈z = relTo (trans-hom ( sym y≈x ) y≈z)
+
   _≈⟨⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y : Hom A a b } → x IsRelatedTo y → x IsRelatedTo y
   _ ≈⟨⟩ x∼y = x∼y
 
--- a/free-monoid.agda	Mon Aug 19 18:14:19 2013 +0900
+++ b/free-monoid.agda	Tue Aug 20 17:57:22 2013 +0900
@@ -68,7 +68,7 @@
   field
       morph : Carrier a -> Carrier b  
       identity     :  morph (ε a)  ≡  ε b
-      mdistr :  ∀{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
 
@@ -76,25 +76,26 @@
 _+_ {a} {b} {c} f g =  record {
       morph = \x ->  morph  f ( morph g x ) ;
       identity  = identity1 ;
-      mdistr  = mdistr1 
+      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 )
-      mdistr1 :  ∀{x y} -> morph f ( morph g ( _∙_ a x  y )) ≡ ( _∙_ c (morph f (morph  g x )) (morph f (morph  g y) ) )
+      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) ) )
-      mdistr1 = trans  (≡-cong (morph f ) ( mdistr g) ) ( mdistr f ) 
+      --  ∀{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 ) 
 
 M-id : { a : ≡-Monoid } -> Monomorph a a 
-M-id = record { morph = \x -> x  ; identity = refl ; mdistr = refl }
+M-id = record { morph = \x -> x  ; identity = refl ; homo = refl }
 
 _==_ : { a b : ≡-Monoid } -> Monomorph a b -> Monomorph a b -> Set c 
 _==_  f g =  morph f ≡ morph g
 
-isMonoidCategory : IsCategory ≡-Monoid Monomorph _==_  _+_  (M-id)
-isMonoidCategory  = record  { isEquivalence =  isEquivalence1 
+isMonoids : IsCategory ≡-Monoid Monomorph _==_  _+_  (M-id)
+isMonoids  = record  { isEquivalence =  isEquivalence1 
                     ; identityL =  refl
                     ; identityR =  refl
                     ; associative = refl
@@ -110,18 +111,18 @@
              ; sym   = sym
              ; trans = trans
              } 
-MonoidCategory : Category _ _ _
-MonoidCategory  =
+Monoids : Category _ _ _
+Monoids  =
   record { Obj =  ≡-Monoid 
          ; Hom = Monomorph
          ; _o_ = _+_  
          ; _≈_ = _==_
          ; Id  =  M-id
-         ; isCategory = isMonoidCategory 
+         ; isCategory = isMonoids 
            }
 
 A = Sets {c}
-B = MonoidCategory  
+B = Monoids  
 
 open Functor
 
@@ -167,20 +168,20 @@
 solution a b f = record {
          morph = \(l : List a) -> Φ l   ;
          identity = refl ;
-         mdistr = \{x y} -> mdistr1 x y 
+         homo = \{x y} -> homo1 x y 
     } where
         _*_ : 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 
+        homo1 : (x y : Carrier (Generator a)) → Φ ((Generator a ∙ x) y) ≡ (b ∙ Φ x) (Φ y)
+        homo1 [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ y))
+        homo1 (x :: xs) y = let open ≡-Reasoning in 
              sym ( begin
                 (Φ {a} {b} {f} (x :: xs)) * (Φ {a} {b} {f} y)
              ≡⟨⟩
                  ((f x) * (Φ {a} {b} {f} xs)) * (Φ {a} {b} {f} y)
              ≡⟨ ( IsMonoid.assoc ( isMonoid b )) _ _ _ ⟩
                 (f x) * ( (Φ {a} {b} {f} xs)  * (Φ {a} {b} {f} y) )
-             ≡⟨ sym ( (IsMonoid.∙-cong (isMonoid b)) refl (mdistr1 xs y )) ⟩
+             ≡⟨ sym ( (IsMonoid.∙-cong (isMonoid b)) refl (homo1 xs y )) ⟩
                 (f x) * ( Φ {a} {b} {f} ( xs ++ y ) )
              ≡⟨⟩
                 Φ {a} {b} {f} ( x :: ( xs ++ y ) )
@@ -193,8 +194,8 @@
 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 ) 
+-- Functional Extensionality Axiom (We cannot prove this in Agda / Coq, just assumming )
+postulate Extensionality : { 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 = 
@@ -217,7 +218,7 @@
                          ( λ (x : a ) →  _∙_ b  ( f x ) (Φ {a} {b} {f} [] ) )
                      ≡⟨⟩
                          ( λ (x : a ) →  _∙_ b  ( f x ) ( ε b ) )
-                     ≡⟨ ≡-cong ( \ g -> ( ( λ (x : a ) →  g x ) )) (Extensionarity lemma-ext1) ⟩
+                     ≡⟨ ≡-cong ( \ g -> ( ( λ (x : a ) →  g x ) )) (Extensionality lemma-ext1) ⟩
                          ( λ (x : a ) →  f x  )
                      ≡⟨⟩
                           f
@@ -227,7 +228,7 @@
         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 {a} {b} {f} {g} eq =  
-                     Extensionarity  ( lemma-ext2 ) where
+                     Extensionality  ( lemma-ext2 ) where
                         lemma-ext2 : ( ∀{ x : List a } -> (morph ( solution a b f)) x  ≡ (morph g) x  )
                         -- (morph ( solution a b f)) []  ≡ (morph g) []  )
                         lemma-ext2 {[]} = let open ≡-Reasoning in
@@ -241,19 +242,19 @@
                         lemma-ext2 {x :: xs}  = let open ≡-Reasoning in
                              begin
                                 (morph ( solution a b f)) ( x :: xs )
-                             ≡⟨ mdistr ( 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 )) )) (
                                  begin
                                      ( \x -> (morph ( solution a b f)) ( x :: [] ) )
-                                 ≡⟨ Extensionarity lemma-ext3 ⟩
+                                 ≡⟨ Extensionality lemma-ext3 ⟩
                                      ( \x -> (morph g) ( x :: [] ) )
                                  ∎  
                              ) ⟩
                                  _∙_ b ((morph g) ( x :: [] )) ((morph g) ( xs ))
-                             ≡⟨ sym ( mdistr g ) ⟩
+                             ≡⟨ sym ( homo g ) ⟩
                                 (morph g) ( x :: xs )
                              ∎   where
                          lemma-ext3 :  ∀{ x : a } -> (morph ( solution a b f)) (x :: [])  ≡ (morph g) ( x :: []  )
--- a/list-monoid-cat.agda	Mon Aug 19 18:14:19 2013 +0900
+++ b/list-monoid-cat.agda	Tue Aug 20 17:57:22 2013 +0900
@@ -3,13 +3,7 @@
 open import HomReasoning
 open import cat-utility
 
-module free-monoid (c : Level ) where
-
-postulate A : Set
-
-postulate a : A
-postulate b : A
-
+module list-monoid-cat (c : Level ) where
 
 infixr 40 _::_
 data  List  (A : Set ) : Set  where
@@ -111,5 +105,3 @@
          ; isCategory = ( isMonoidCategory M )
           }
 
-
-
--- a/monoid-monad.agda	Mon Aug 19 18:14:19 2013 +0900
+++ b/monoid-monad.agda	Tue Aug 20 17:57:22 2013 +0900
@@ -103,20 +103,20 @@
 Lemma-MM36 : ∀{ x y z : Carrier M } → ((M ∙ (M ∙ x) y) z)  ≡ (_∙_ M  x (_∙_ M y z ) )
 Lemma-MM36  {x} {y} {z} = ( IsMonoid.assoc ( isMonoid M ))  x y z
 
--- Functional Extensionarity Axiom (We cannot prove this in Agda / Coq, just assumming )
-postulate Extensionarity : {f g : Carrier M → Carrier M } → (∀ {x} → (f x ≡ g x))  → ( f ≡ g ) 
+-- Functional Extensionality Axiom (We cannot prove this in Agda / Coq, just assumming )
+postulate Extensionality : {f g : Carrier M → Carrier M } → (∀ {x} → (f x ≡ g x))  → ( f ≡ g ) 
 
-postulate Extensionarity3 : {f g : Carrier M → Carrier M → Carrier M → Carrier M } → 
+postulate Extensionality3 : {f g : Carrier M → Carrier M → Carrier M → Carrier M } → 
                (∀{x y z} → f x y z ≡ g x y z )  → ( f ≡ g ) 
 
 Lemma-MM9  : ( λ(x : Carrier M) → ( M ∙ ε M ) x )  ≡ ( λ(x : Carrier M) → x ) 
-Lemma-MM9  = Extensionarity Lemma-MM34
+Lemma-MM9  = Extensionality Lemma-MM34
 
 Lemma-MM10 : ( λ x →   ((M ∙ x) (ε M)))  ≡ ( λ x → x ) 
-Lemma-MM10 = Extensionarity Lemma-MM35
+Lemma-MM10 = Extensionality Lemma-MM35
 
 Lemma-MM11 : (λ x y z → ((M ∙ (M ∙ x) y) z))  ≡ (λ x y z → ( _∙_ M  x (_∙_ M y z ) ))
-Lemma-MM11 = Extensionarity3 Lemma-MM36 
+Lemma-MM11 = Extensionality3 Lemma-MM36 
 
 MonoidMonad : Monad A T η μ 
 MonoidMonad = record {