Mercurial > hg > Members > kono > Proof > category

changeset 170:721cf9d9f5e3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use functional extensionality in library
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 21 Aug 2013 18:33:03 +0900
parents 44bf6e78f891
children d25b0948e006
files free-monoid.agda monoid-monad.agda
diffstat 2 files changed, 15 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/free-monoid.agda	Wed Aug 21 15:38:41 2013 +0900
+++ b/free-monoid.agda	Wed Aug 21 18:33:03 2013 +0900
@@ -196,7 +196,7 @@
 
 -- 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 ) 
-postulate extensionality : { a b : Obj A } {f g : Hom A a b } →  Relation.Binary.PropositionalEquality.Extensionality c c 
+postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c 
 
 FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta  
 FreeMonoidUniveralMapping = 
@@ -219,7 +219,7 @@
                          ( λ (x : a ) →  _∙_ b  ( f x ) (Φ {a} {b} {f} [] ) )
                      ≡⟨⟩
                          ( λ (x : a ) →  _∙_ b  ( f x ) ( ε b ) )
-                     ≡⟨ ≡-cong ( \ g -> ( ( λ (x : a ) →  g x ) )) (extensionality {a} {FObj U b} {\x ->  _∙_ b  ( f x ) ( ε b ) } {f} lemma-ext1) ⟩
+                     ≡⟨ ≡-cong ( \ g -> ( ( λ (x : a ) →  g x ) )) (extensionality {a} lemma-ext1) ⟩
                          ( λ (x : a ) →  f x  )
                      ≡⟨⟩
                           f
@@ -229,7 +229,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 =  
-                     extensionality  {List a} {FObj U b} {morph ( solution a b f)} {morph g} ( 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
@@ -250,7 +250,7 @@
                              ≡⟨  ≡-cong ( \k -> ( _∙_ b ( k x ) ((morph g) ( xs )) )) (
                                  begin
                                      ( \x -> (morph ( solution a b f)) ( x :: [] ) )
-                                 ≡⟨ extensionality {a} {Carrier b} { \x -> (morph ( solution a b f)) (x :: [])} {\x -> (morph g) ( x :: []  )} lemma-ext3 ⟩
+                                 ≡⟨ extensionality {a} lemma-ext3 ⟩
                                      ( \x -> (morph g) ( x :: [] ) )
                                  ∎  
                              ) ⟩
--- a/monoid-monad.agda	Wed Aug 21 15:38:41 2013 +0900
+++ b/monoid-monad.agda	Wed Aug 21 18:33:03 2013 +0900
@@ -100,25 +100,27 @@
 Lemma-MM35 : ∀( x : Carrier M  ) → ((M ∙ x) (ε M))  ≡ x
 Lemma-MM35  x = ( proj₂  ( IsMonoid.identity ( isMonoid M )) ) x
 
-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
+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 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 ) 
 import Relation.Binary.PropositionalEquality
-postulate extensionality : { a b : Obj A } {f g : Hom A a b } →  Relation.Binary.PropositionalEquality.Extensionality c c
+-- postulate extensionality : { a b : Obj A } {f g : Hom A a b } →  Relation.Binary.PropositionalEquality.Extensionality c c
+postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c
 
-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 ) 
+-- Multi Arguments Functional Extensionality
+extensionality30 : {f g : Carrier M → Carrier M → Carrier M → Carrier M } → 
+               (∀ x y z  → f x y z ≡ g x y z )  → ( f ≡ g ) 
+extensionality30 eq = extensionality ( \x -> extensionality ( \y -> extensionality (eq x y) ) )
 
 Lemma-MM9  : ( λ(x : Carrier M) → ( M ∙ ε M ) x )  ≡ ( λ(x : Carrier M) → x ) 
-Lemma-MM9  = extensionality {Carrier M} {Carrier M} {(M ∙ ε M)} {\x -> x} Lemma-MM34
+Lemma-MM9  = extensionality Lemma-MM34
 
 Lemma-MM10 : ( λ x →   ((M ∙ x) (ε M)))  ≡ ( λ x → x ) 
-Lemma-MM10  = extensionality {Carrier M} {Carrier M} { \x -> ((M ∙ x) (ε M)) } {\x -> x} 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 = extensionality3 Lemma-MM36 
+Lemma-MM11 = extensionality30 Lemma-MM36 
 
 MonoidMonad : Monad A T η μ 
 MonoidMonad = record {