Mercurial > hg > Members > kono > Proof > category

comparison monoid-monad.agda @ 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 58ee98bbb333
comparison
equal deleted inserted replaced
169:44bf6e78f891 170:721cf9d9f5e3
98 Lemma-MM34 x = (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) x ) 98 Lemma-MM34 x = (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) x )
99 99
100 Lemma-MM35 : ∀( x : Carrier M ) → ((M ∙ x) (ε M)) ≡ x 100 Lemma-MM35 : ∀( x : Carrier M ) → ((M ∙ x) (ε M)) ≡ x
101 Lemma-MM35 x = ( proj₂ ( IsMonoid.identity ( isMonoid M )) ) x 101 Lemma-MM35 x = ( proj₂ ( IsMonoid.identity ( isMonoid M )) ) x
102 102
103 Lemma-MM36 : ∀{ x y z : Carrier M } → ((M ∙ (M ∙ x) y) z) ≡ (_∙_ M x (_∙_ M y z ) ) 103 Lemma-MM36 : ∀( x y z : Carrier M ) → ((M ∙ (M ∙ x) y) z) ≡ (_∙_ M x (_∙_ M y z ) )
104 Lemma-MM36 {x} {y} {z} = ( IsMonoid.assoc ( isMonoid M )) x y z 104 Lemma-MM36 x y z = ( IsMonoid.assoc ( isMonoid M )) x y z
105 105
106 -- Functional Extensionality Axiom (We cannot prove this in Agda / Coq, just assumming ) 106 -- Functional Extensionality Axiom (We cannot prove this in Agda / Coq, just assumming )
107 -- postulate extensionality : {f g : Carrier M → Carrier M } → (∀ {x} → (f x ≡ g x)) → ( f ≡ g )
108 import Relation.Binary.PropositionalEquality 107 import Relation.Binary.PropositionalEquality
109 postulate extensionality : { a b : Obj A } {f g : Hom A a b } → Relation.Binary.PropositionalEquality.Extensionality c c 108 -- postulate extensionality : { a b : Obj A } {f g : Hom A a b } → Relation.Binary.PropositionalEquality.Extensionality c c
109 postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c
110 110
111 postulate extensionality3 : {f g : Carrier M → Carrier M → Carrier M → Carrier M } → 111 -- Multi Arguments Functional Extensionality
112 (∀{x y z} → f x y z ≡ g x y z ) → ( f ≡ g ) 112 extensionality30 : {f g : Carrier M → Carrier M → Carrier M → Carrier M } →
113 (∀ x y z → f x y z ≡ g x y z ) → ( f ≡ g )
114 extensionality30 eq = extensionality ( \x -> extensionality ( \y -> extensionality (eq x y) ) )
113 115
114 Lemma-MM9 : ( λ(x : Carrier M) → ( M ∙ ε M ) x ) ≡ ( λ(x : Carrier M) → x ) 116 Lemma-MM9 : ( λ(x : Carrier M) → ( M ∙ ε M ) x ) ≡ ( λ(x : Carrier M) → x )
115 Lemma-MM9 = extensionality {Carrier M} {Carrier M} {(M ∙ ε M)} {\x -> x} Lemma-MM34 117 Lemma-MM9 = extensionality Lemma-MM34
116 118
117 Lemma-MM10 : ( λ x → ((M ∙ x) (ε M))) ≡ ( λ x → x ) 119 Lemma-MM10 : ( λ x → ((M ∙ x) (ε M))) ≡ ( λ x → x )
118 Lemma-MM10 = extensionality {Carrier M} {Carrier M} { \x -> ((M ∙ x) (ε M)) } {\x -> x} Lemma-MM35 120 Lemma-MM10 = extensionality Lemma-MM35
119 121
120 Lemma-MM11 : (λ x y z → ((M ∙ (M ∙ x) y) z)) ≡ (λ x y z → ( _∙_ M x (_∙_ M y z ) )) 122 Lemma-MM11 : (λ x y z → ((M ∙ (M ∙ x) y) z)) ≡ (λ x y z → ( _∙_ M x (_∙_ M y z ) ))
121 Lemma-MM11 = extensionality3 Lemma-MM36 123 Lemma-MM11 = extensionality30 Lemma-MM36
122 124
123 MonoidMonad : Monad A T η μ 125 MonoidMonad : Monad A T η μ
124 MonoidMonad = record { 126 MonoidMonad = record {
125 isMonad = record { 127 isMonad = record {
126 unity1 = Lemma-MM3 ; 128 unity1 = Lemma-MM3 ;