Mercurial > hg > Members > kono > Proof > category
changeset 169:44bf6e78f891
builtin extensionality
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 21 Aug 2013 15:38:41 +0900 |
| parents | a9b4132d619b |
| children | 721cf9d9f5e3 |
| files | free-monoid.agda monoid-monad.agda |
| diffstat | 2 files changed, 24 insertions(+), 21 deletions(-) [+] |
line wrap: on
line diff
--- a/free-monoid.agda Tue Aug 20 17:57:22 2013 +0900 +++ b/free-monoid.agda Wed Aug 21 15:38:41 2013 +0900 @@ -195,7 +195,8 @@ eta a = \( x : a ) -> x :: [] -- 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 } → (∀ {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 FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta FreeMonoidUniveralMapping = @@ -218,20 +219,20 @@ ( λ (x : a ) → _∙_ b ( f x ) (Φ {a} {b} {f} [] ) ) ≡⟨⟩ ( λ (x : a ) → _∙_ b ( f x ) ( ε b ) ) - ≡⟨ ≡-cong ( \ g -> ( ( λ (x : a ) → g x ) )) (Extensionality lemma-ext1) ⟩ + ≡⟨ ≡-cong ( \ g -> ( ( λ (x : a ) → g x ) )) (extensionality {a} {FObj U b} {\x -> _∙_ b ( f x ) ( ε b ) } {f} 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) + 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 {a} {b} {f} {g} eq = - Extensionality ( lemma-ext2 ) where - lemma-ext2 : ( ∀{ x : List a } -> (morph ( solution a b f)) x ≡ (morph g) x ) + extensionality {List a} {FObj U b} {morph ( solution a b f)} {morph g} ( 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 + lemma-ext2 [] = let open ≡-Reasoning in begin (morph ( solution a b f)) [] ≡⟨ identity ( solution a b f) ⟩ @@ -239,17 +240,17 @@ ≡⟨ sym ( identity g ) ⟩ (morph g) [] ∎ - lemma-ext2 {x :: xs} = let open ≡-Reasoning in + lemma-ext2 (x :: xs) = let open ≡-Reasoning in 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} ) ⟩ + ≡⟨ ≡-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 lemma-ext3 ⟩ + ≡⟨ extensionality {a} {Carrier b} { \x -> (morph ( solution a b f)) (x :: [])} {\x -> (morph g) ( x :: [] )} lemma-ext3 ⟩ ( \x -> (morph g) ( x :: [] ) ) ∎ ) ⟩ @@ -257,8 +258,8 @@ ≡⟨ sym ( homo g ) ⟩ (morph g) ( x :: xs ) ∎ where - lemma-ext3 : ∀{ x : a } -> (morph ( solution a b f)) (x :: []) ≡ (morph g) ( x :: [] ) - lemma-ext3 {x} = let open ≡-Reasoning in + lemma-ext3 : ∀( x : a ) -> (morph ( solution a b f)) (x :: []) ≡ (morph g) ( x :: [] ) + lemma-ext3 x = let open ≡-Reasoning in begin (morph ( solution a b f)) (x :: []) ≡⟨ ( proj₂ ( IsMonoid.identity ( isMonoid b) )(f x) ) ⟩
--- a/monoid-monad.agda Tue Aug 20 17:57:22 2013 +0900 +++ b/monoid-monad.agda Wed Aug 21 15:38:41 2013 +0900 @@ -94,29 +94,31 @@ Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b} {x : Σ A B } → (((proj₁ x) , proj₂ x ) ≡ x ) Lemma-MM33 = _≡_.refl -Lemma-MM34 : ∀{ x : Carrier M } → ( (M ∙ ε M) x ≡ x ) -Lemma-MM34 {x} = (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) x ) +Lemma-MM34 : ∀( x : Carrier M ) → ( (M ∙ ε M) x ≡ x ) +Lemma-MM34 x = (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) x ) -Lemma-MM35 : ∀{ x : Carrier M } → ((M ∙ x) (ε M)) ≡ x -Lemma-MM35 {x} = ( proj₂ ( IsMonoid.identity ( isMonoid M )) ) x +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 -- 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 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 Extensionality3 : {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 = Extensionality Lemma-MM34 +Lemma-MM9 = extensionality {Carrier M} {Carrier M} {(M ∙ ε M)} {\x -> x} Lemma-MM34 Lemma-MM10 : ( λ x → ((M ∙ x) (ε M))) ≡ ( λ x → x ) -Lemma-MM10 = Extensionality Lemma-MM35 +Lemma-MM10 = extensionality {Carrier M} {Carrier M} { \x -> ((M ∙ x) (ε M)) } {\x -> x} 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 = extensionality3 Lemma-MM36 MonoidMonad : Monad A T η μ MonoidMonad = record {