Mercurial > hg > Members > kono > Proof > category

comparison free-monoid.agda @ 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
comparison
equal deleted inserted replaced
341:33bc037319fa 342:a9711cf75a12
10 open import Category.Sets 10 open import Category.Sets
11 open import Category.Cat 11 open import Category.Cat
12 open import HomReasoning 12 open import HomReasoning
13 open import cat-utility 13 open import cat-utility
14 open import Relation.Binary.Core 14 open import Relation.Binary.Core
15 open import Relation.Binary.PropositionalEquality
16 open import universal-mapping 15 open import universal-mapping
16 open import Relation.Binary.PropositionalEquality
17 17
18 -- from https://github.com/danr/Agda-projects/blob/master/Category-Theory/FreeMonoid.agda 18 -- from https://github.com/danr/Agda-projects/blob/master/Category-Theory/FreeMonoid.agda
19
20 open import Algebra.FunctionProperties using (Op₁; Op₂)
21 open import Algebra.Structures
22 open import Data.Product
23
24
25 record ≡-Monoid : Set (suc c) where
26 infixr 9 _∙_
27 field
28 Carrier : Set c
29 _∙_ : Op₂ Carrier
30 ε : Carrier
31 isMonoid : IsMonoid _≡_ _∙_ ε
32
33 open ≡-Monoid
34
35 ≡-cong = Relation.Binary.PropositionalEquality.cong
36
37 -- module ≡-reasoning (m : ≡-Monoid ) where
19 38
20 infixr 40 _::_ 39 infixr 40 _::_
21 data List (A : Set c ) : Set c where 40 data List (A : Set c ) : Set c where
22 [] : List A 41 [] : List A
23 _::_ : A → List A → List A 42 _::_ : A → List A → List A
25 44
26 infixl 30 _++_ 45 infixl 30 _++_
27 _++_ : {A : Set c } → List A → List A → List A 46 _++_ : {A : Set c } → List A → List A → List A
28 [] ++ ys = ys 47 [] ++ ys = ys
29 (x :: xs) ++ ys = x :: (xs ++ ys) 48 (x :: xs) ++ ys = x :: (xs ++ ys)
30
31 ≡-cong = Relation.Binary.PropositionalEquality.cong
32 49
33 list-id-l : { A : Set c } → { x : List A } → [] ++ x ≡ x 50 list-id-l : { A : Set c } → { x : List A } → [] ++ x ≡ x
34 list-id-l {_} {_} = refl 51 list-id-l {_} {_} = refl
35 list-id-r : { A : Set c } → { x : List A } → x ++ [] ≡ x 52 list-id-r : { A : Set c } → { x : List A } → x ++ [] ≡ x
36 list-id-r {_} {[]} = refl 53 list-id-r {_} {[]} = refl
48 record { refl = refl 65 record { refl = refl
49 ; sym = sym 66 ; sym = sym
50 ; trans = trans 67 ; trans = trans
51 } 68 }
52 69
53 open import Algebra.FunctionProperties using (Op₁; Op₂) 70
54 open import Algebra.Structures 71 _<_∙_> : (m : ≡-Monoid) → Carrier m → Carrier m → Carrier m
55 open import Data.Product 72 m < x ∙ y > = _∙_ m x y
56 73
57 74 infixr 9 _<_∙_>
58 record ≡-Monoid : Set (suc c) where
59 infixl 7 _∙_
60 field
61 Carrier : Set c
62 _∙_ : Op₂ Carrier
63 ε : Carrier
64 isMonoid : IsMonoid _≡_ _∙_ ε
65
66 open ≡-Monoid
67 75
68 record Monomorph ( a b : ≡-Monoid ) : Set (suc c) where 76 record Monomorph ( a b : ≡-Monoid ) : Set (suc c) where
69 field 77 field
70 morph : Carrier a → Carrier b 78 morph : Carrier a → Carrier b
71 identity : morph (ε a) ≡ ε b 79 identity : morph (ε a) ≡ ε b
72 homo : ∀{x y} → morph ( _∙_ a x y ) ≡ ( _∙_ b (morph x ) (morph y) ) 80 homo : ∀{x y} → morph ( a < x ∙ y > ) ≡ b < morph x ∙ morph y >
73 81
74 open Monomorph 82 open Monomorph
75 83
76 _+_ : { a b c : ≡-Monoid } → Monomorph b c → Monomorph a b → Monomorph a c 84 _+_ : { a b c : ≡-Monoid } → Monomorph b c → Monomorph a b → Monomorph a c
77 _+_ {a} {b} {c} f g = record { 85 _+_ {a} {b} {c} f g = record {
78 morph = λ x → morph f ( morph g x ) ; 86 morph = λ x → morph f ( morph g x ) ;
79 identity = identity1 ; 87 identity = identity1 ;
80 homo = homo1 88 homo = homo1
81 } where 89 } where
82 identity1 : morph f ( morph g (ε a) ) ≡ ε c 90 identity1 : morph f ( morph g (ε a) ) ≡ ε c
83 -- morph f (ε b) = ε c , morph g (ε a) ) ≡ ε b 91 identity1 = let open ≡-Reasoning in begin
84 -- morph f morph g (ε a) ) ≡ morph f (ε b) = ε c 92 morph f (morph g (ε a))
85 identity1 = trans ( ≡-cong (morph f ) ( identity g ) ) ( identity f ) 93 ≡⟨ ≡-cong (morph f ) ( identity g ) ⟩
86 homo1 : ∀{x y} → morph f ( morph g ( _∙_ a x y )) ≡ ( _∙_ c (morph f (morph g x )) (morph f (morph g y) ) ) 94 morph f (ε b)
87 -- ∀{x y} → morph f ( morph g ( _∙_ a x y )) ≡ morph f ( ( _∙_ c (morph g x )) (morph g y) ) 95 ≡⟨ identity f ⟩
88 -- ∀{x y} → morph f ( ( _∙_ c (morph g x )) (morph g y) ) 96 ε c
89 -- ≡ ( _∙_ c (morph f (morph g x )) (morph f (morph g y) ) ) 97 ∎
90 homo1 = trans (≡-cong (morph f ) ( homo g) ) ( homo f ) 98 homo1 : ∀{x y} → morph f ( morph g ( a < x ∙ y > )) ≡ ( c < (morph f (morph g x )) ∙(morph f (morph g y) ) > )
99 homo1 {x} {y} = let open ≡-Reasoning in begin
100 morph f (morph g (a < x ∙ y >))
101 ≡⟨ ≡-cong (morph f ) ( homo g) ⟩
102 morph f (b < morph g x ∙ morph g y >)
103 ≡⟨ homo f ⟩
104 c < morph f (morph g x) ∙ morph f (morph g y) >
105 ∎
91 106
92 M-id : { a : ≡-Monoid } → Monomorph a a 107 M-id : { a : ≡-Monoid } → Monomorph a a
93 M-id = record { morph = λ x → x ; identity = refl ; homo = refl } 108 M-id = record { morph = λ x → x ; identity = refl ; homo = refl }
94 109
95 _==_ : { a b : ≡-Monoid } → Monomorph a b → Monomorph a b → Set c 110 _==_ : { a b : ≡-Monoid } → Monomorph a b → Monomorph a b → Set c
140 155
141 -- FObj 156 -- FObj
142 list : (a : Set c) → ≡-Monoid 157 list : (a : Set c) → ≡-Monoid
143 list a = record { 158 list a = record {
144 Carrier = List a 159 Carrier = List a
145 ; _∙_ = _++_ 160 ; _∙_ = _++_
146 ; ε = [] 161 ; ε = []
147 ; isMonoid = record { 162 ; isMonoid = record {
148 identity = ( ( λ x → list-id-l {a} ) , ( λ x → list-id-r {a} ) ) ; 163 identity = ( ( λ x → list-id-l {a} ) , ( λ x → list-id-r {a} ) ) ;
149 isSemigroup = record { 164 isSemigroup = record {
150 assoc = λ x → λ y → λ z → sym ( list-assoc {a} {x} {y} {z} ) 165 assoc = λ x → λ y → λ z → sym ( list-assoc {a} {x} {y} {z} )
162 open UniversalMapping 177 open UniversalMapping
163 178
164 -- [a,b,c] → f(a) ∙ f(b) ∙ f(c) 179 -- [a,b,c] → f(a) ∙ f(b) ∙ f(c)
165 Φ : {a : Obj A } {b : Obj B} ( f : Hom A a (FObj U b) ) → List a → Carrier b 180 Φ : {a : Obj A } {b : Obj B} ( f : Hom A a (FObj U b) ) → List a → Carrier b
166 Φ {a} {b} f [] = ε b 181 Φ {a} {b} f [] = ε b
167 Φ {a} {b} f ( x :: xs ) = _∙_ b ( f x ) (Φ {a} {b} f xs ) 182 Φ {a} {b} f ( x :: xs ) = b < ( f x ) ∙ (Φ {a} {b} f xs ) >
168 183
169 solution : (a : Obj A ) (b : Obj B) ( f : Hom A a (FObj U b) ) → Hom B (Generator a ) b 184 solution : (a : Obj A ) (b : Obj B) ( f : Hom A a (FObj U b) ) → Hom B (Generator a ) b
170 solution a b f = record { 185 solution a b f = record {
171 morph = λ (l : List a) → Φ f l ; 186 morph = λ (l : List a) → Φ f l ;
172 identity = refl; 187 identity = refl;
173 homo = λ {x y} → homo1 x y 188 homo = λ {x y} → homo1 x y
174 } where 189 } where
175 _*_ : Carrier b → Carrier b → Carrier b 190 _*_ : Carrier b → Carrier b → Carrier b
176 _*_ f g = _∙_ b f g 191 _*_ f g = b < f ∙ g >
177 homo1 : (x y : Carrier (Generator a)) → Φ f ((Generator a ∙ x) y) ≡ (b ∙ Φ f x) (Φ {a} {b} f y) 192 homo1 : (x y : Carrier (Generator a)) → Φ f ( (Generator a) < x ∙ y > ) ≡ (Φ f x) * (Φ {a} {b} f y )
178 homo1 [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ f y)) 193 homo1 [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ f y))
179 homo1 (x :: xs) y = let open ≡-Reasoning in 194 homo1 (x :: xs) y = let open ≡-Reasoning in
180 sym ( begin 195 sym ( begin
181 (Φ {a} {b} f (x :: xs)) * (Φ f y) 196 (Φ {a} {b} f (x :: xs)) * (Φ f y)
182 ≡⟨⟩ 197 ≡⟨⟩
188 ≡⟨⟩ 203 ≡⟨⟩
189 Φ {a} {b} f ( x :: ( xs ++ y ) ) 204 Φ {a} {b} f ( x :: ( xs ++ y ) )
190 ≡⟨⟩ 205 ≡⟨⟩
191 Φ {a} {b} f ( (x :: xs) ++ y ) 206 Φ {a} {b} f ( (x :: xs) ++ y )
192 ≡⟨⟩ 207 ≡⟨⟩
193 Φ {a} {b} f ((Generator a ∙ x :: xs) y) 208 Φ {a} {b} f ((Generator a) < ( x :: xs) ∙ y > )
194 ∎ ) 209 ∎ )
195 210
196 eta : (a : Obj A) → Hom A a ( FObj U (Generator a) ) 211 eta : (a : Obj A) → Hom A a ( FObj U (Generator a) )
197 eta a = λ ( x : a ) → x :: [] 212 eta a = λ ( x : a ) → x :: []
198 213
216 ≡⟨⟩ 231 ≡⟨⟩
217 ( λ (x : a ) → Φ {a} {b} f (eta a x) ) 232 ( λ (x : a ) → Φ {a} {b} f (eta a x) )
218 ≡⟨⟩ 233 ≡⟨⟩
219 ( λ (x : a ) → Φ {a} {b} f ( x :: [] ) ) 234 ( λ (x : a ) → Φ {a} {b} f ( x :: [] ) )
220 ≡⟨⟩ 235 ≡⟨⟩
221 ( λ (x : a ) → _∙_ b ( f x ) (Φ {a} {b} f [] ) ) 236 ( λ (x : a ) → b < ( f x ) ∙ (Φ {a} {b} f [] ) > )
222 ≡⟨⟩ 237 ≡⟨⟩
223 ( λ (x : a ) → _∙_ b ( f x ) ( ε b ) ) 238 ( λ (x : a ) → b < ( f x ) ∙ ( ε b ) > )
224 ≡⟨ ≡-cong ( λ g → ( ( λ (x : a ) → g x ) )) (extensionality {a} lemma-ext1) ⟩ 239 ≡⟨ ≡-cong ( λ g → ( ( λ (x : a ) → g x ) )) (extensionality {a} lemma-ext1) ⟩
225 ( λ (x : a ) → f x ) 240 ( λ (x : a ) → f x )
226 ≡⟨⟩ 241 ≡⟨⟩
227 f 242 f
228 ∎ where 243 ∎ where
229 lemma-ext1 : ∀( x : a ) → _∙_ b ( f x ) ( ε b ) ≡ f x 244 lemma-ext1 : ∀( x : a ) → b < ( f x ) ∙ ( ε b ) > ≡ f x
230 lemma-ext1 x = ( proj₂ ( IsMonoid.identity ( isMonoid b) ) ) (f x) 245 lemma-ext1 x = ( proj₂ ( IsMonoid.identity ( isMonoid b) ) ) (f x)
231 uniquness : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } → 246 uniquness : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } →
232 { g : Hom B (Generator a) b } → (FMap U g) o (eta a ) ≡ f → B [ solution a b f ≈ g ] 247 { g : Hom B (Generator a) b } → (FMap U g) o (eta a ) ≡ f → B [ solution a b f ≈ g ]
233 uniquness {a} {b} {f} {g} eq = 248 uniquness {a} {b} {f} {g} eq =
234 extensionality lemma-ext2 where 249 extensionality lemma-ext2 where
244 ∎ 259 ∎
245 lemma-ext2 (x :: xs) = let open ≡-Reasoning in 260 lemma-ext2 (x :: xs) = let open ≡-Reasoning in
246 begin 261 begin
247 (morph ( solution a b f)) ( x :: xs ) 262 (morph ( solution a b f)) ( x :: xs )
248 ≡⟨ homo ( solution a b f) {x :: []} {xs} ⟩ 263 ≡⟨ homo ( solution a b f) {x :: []} {xs} ⟩
249 _∙_ b ((morph ( solution a b f)) ( x :: []) ) ((morph ( solution a b f)) xs ) 264 b < ((morph ( solution a b f)) ( x :: []) ) ∙ ((morph ( solution a b f)) xs ) >
250 ≡⟨ ≡-cong ( λ k → (_∙_ b ((morph ( solution a b f)) ( x :: []) ) k )) (lemma-ext2 xs ) ⟩ 265 ≡⟨ ≡-cong ( λ k → (b < ((morph ( solution a b f)) ( x :: []) ) ∙ k > )) (lemma-ext2 xs ) ⟩
251 _∙_ b ((morph ( solution a b f)) ( x :: []) ) ((morph g) ( xs )) 266 b < ((morph ( solution a b f)) ( x :: []) ) ∙((morph g) ( xs )) >
252 ≡⟨ ≡-cong ( λ k → ( _∙_ b ( k x ) ((morph g) ( xs )) )) ( 267 ≡⟨ ≡-cong ( λ k → ( b < ( k x ) ∙ ((morph g) ( xs )) > )) (
253 begin 268 begin
254 ( λ x → (morph ( solution a b f)) ( x :: [] ) ) 269 ( λ x → (morph ( solution a b f)) ( x :: [] ) )
255 ≡⟨ extensionality {a} lemma-ext3 ⟩ 270 ≡⟨ extensionality {a} lemma-ext3 ⟩
256 ( λ x → (morph g) ( x :: [] ) ) 271 ( λ x → (morph g) ( x :: [] ) )
257 ∎ 272 ∎
258 ) ⟩ 273 ) ⟩
259 _∙_ b ((morph g) ( x :: [] )) ((morph g) ( xs )) 274 b < ((morph g) ( x :: [] )) ∙((morph g) ( xs )) >
260 ≡⟨ sym ( homo g ) ⟩ 275 ≡⟨ sym ( homo g ) ⟩
261 (morph g) ( x :: xs ) 276 (morph g) ( x :: xs )
262 ∎ where 277 ∎ where
263 lemma-ext3 : ∀( x : a ) → (morph ( solution a b f)) (x :: []) ≡ (morph g) ( x :: [] ) 278 lemma-ext3 : ∀( x : a ) → (morph ( solution a b f)) (x :: []) ≡ (morph g) ( x :: [] )
264 lemma-ext3 x = let open ≡-Reasoning in 279 lemma-ext3 x = let open ≡-Reasoning in