Mercurial > hg > Members > kono > Proof > category

comparison src/free-monoid.agda @ 1034:40c39d3e6a75

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 31 Mar 2021 15:58:02 +0900
parents ac53803b3b2a
children 45de2b31bf02
comparison
equal deleted inserted replaced
1033:a59c51b541a2 1034:40c39d3e6a75
9 9
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.Structures
15 open import universal-mapping 15 open import universal-mapping
16 open import Relation.Binary.PropositionalEquality 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 19
20 open import Algebra.FunctionProperties using (Op₁; Op₂) 20 open import Algebra.Definitions -- using (Op₁; Op₂)
21 open import Algebra.Core
21 open import Algebra.Structures 22 open import Algebra.Structures
22 open import Data.Product 23 open import Data.Product
23
24 24
25 record ≡-Monoid : Set (suc c) where 25 record ≡-Monoid : Set (suc c) where
26 infixr 9 _∙_ 26 infixr 9 _∙_
27 field 27 field
28 Carrier : Set c 28 Carrier : Set c
110 _==_ : { a b : ≡-Monoid } → Monomorph a b → Monomorph a b → Set c 110 _==_ : { a b : ≡-Monoid } → Monomorph a b → Monomorph a b → Set c
111 _==_ f g = morph f ≡ morph g 111 _==_ f g = morph f ≡ morph g
112 112
113 -- Functional Extensionality Axiom (We cannot prove this in Agda / Coq, just assumming ) 113 -- Functional Extensionality Axiom (We cannot prove this in Agda / Coq, just assumming )
114 -- postulate extensionality : { a b : Obj A } {f g : Hom A a b } → (∀ {x} → (f x ≡ g x)) → ( f ≡ g ) 114 -- postulate extensionality : { a b : Obj A } {f g : Hom A a b } → (∀ {x} → (f x ≡ g x)) → ( f ≡ g )
115 postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c 115 -- postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c
116 116
117 isMonoids : IsCategory ≡-Monoid Monomorph _==_ _+_ (M-id) 117 isMonoids : IsCategory ≡-Monoid Monomorph _==_ _+_ (M-id)
118 isMonoids = record { isEquivalence = isEquivalence1 118 isMonoids = record { isEquivalence = isEquivalence1
119 ; identityL = refl 119 ; identityL = refl
120 ; identityR = refl 120 ; identityR = refl
130 } 130 }
131 o-resp-≈ : {a b c : ≡-Monoid } {f g : Monomorph a b } → {h i : Monomorph b c } → 131 o-resp-≈ : {a b c : ≡-Monoid } {f g : Monomorph a b } → {h i : Monomorph b c } →
132 f == g → h == i → (h + f) == (i + g) 132 f == g → h == i → (h + f) == (i + g)
133 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f==g h==i = let open ≡-Reasoning in begin 133 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f==g h==i = let open ≡-Reasoning in begin
134 morph ( h + f ) 134 morph ( h + f )
135 ≡⟨ ≡-cong ( λ g → ( ( λ (x : Carrier a ) → g x ) )) (extensionality {Carrier a} lemma11) ⟩ 135 ≡⟨ ≡-cong ( λ g → ( ( λ (x : Carrier a ) → g x ) )) (extensionality (Sets ) {Carrier a} lemma11) ⟩
136 morph ( i + g ) 136 morph ( i + g )
137 ∎ 137 ∎
138 where 138 where
139 lemma11 : (x : Carrier a) → morph (h + f) x ≡ morph (i + g) x 139 lemma11 : (x : Carrier a) → morph (h + f) x ≡ morph (i + g) x
140 lemma11 x = let open ≡-Reasoning in begin 140 lemma11 x = let open ≡-Reasoning in begin
182 list : (a : Set c) → ≡-Monoid 182 list : (a : Set c) → ≡-Monoid
183 list a = record { 183 list a = record {
184 Carrier = List a 184 Carrier = List a
185 ; _∙_ = _++_ 185 ; _∙_ = _++_
186 ; ε = [] 186 ; ε = []
187 ; isMonoid = record { 187 ; isMonoid = record { isSemigroup = record { isMagma = record {
188 identity = ( ( λ x → list-id-l {a} ) , ( λ x → list-id-r {a} ) ) ; 188 isEquivalence = list-isEquivalence
189 isSemigroup = record { 189 ; ∙-cong = λ x → λ y → list-o-resp-≈ y x }
190 assoc = λ x → λ y → λ z → sym ( list-assoc {a} {x} {y} {z} ) 190 ; assoc = λ x → λ y → λ z → sym ( list-assoc {a} {x} {y} {z} ) }
191 ; isEquivalence = list-isEquivalence 191 ; identity = ( ( λ x → list-id-l {a} ) , ( λ x → list-id-r {a} ) )
192 ; ∙-cong = λ x → λ y → list-o-resp-≈ y x 192 } }
193 }
194 }
195 }
196 193
197 Generator : Obj A → Obj B 194 Generator : Obj A → Obj B
198 Generator s = list s 195 Generator s = list s
199 196
200 -- solution 197 -- solution
255 ( λ (x : a ) → Φ {a} {b} f ( x :: [] ) ) 252 ( λ (x : a ) → Φ {a} {b} f ( x :: [] ) )
256 ≡⟨⟩ 253 ≡⟨⟩
257 ( λ (x : a ) → b < ( f x ) ∙ (Φ {a} {b} f [] ) > ) 254 ( λ (x : a ) → b < ( f x ) ∙ (Φ {a} {b} f [] ) > )
258 ≡⟨⟩ 255 ≡⟨⟩
259 ( λ (x : a ) → b < ( f x ) ∙ ( ε b ) > ) 256 ( λ (x : a ) → b < ( f x ) ∙ ( ε b ) > )
260 ≡⟨ ≡-cong ( λ g → ( ( λ (x : a ) → g x ) )) (extensionality {a} lemma-ext1) ⟩ 257 ≡⟨ ≡-cong ( λ g → ( ( λ (x : a ) → g x ) )) (extensionality A {a} lemma-ext1) ⟩
261 ( λ (x : a ) → f x ) 258 ( λ (x : a ) → f x )
262 ≡⟨⟩ 259 ≡⟨⟩
263 f 260 f
264 ∎ where 261 ∎ where
265 lemma-ext1 : ∀( x : a ) → b < ( f x ) ∙ ( ε b ) > ≡ f x 262 lemma-ext1 : ∀( x : a ) → b < ( f x ) ∙ ( ε b ) > ≡ f x
266 lemma-ext1 x = ( proj₂ ( IsMonoid.identity ( isMonoid b) ) ) (f x) 263 lemma-ext1 x = ( proj₂ ( IsMonoid.identity ( isMonoid b) ) ) (f x)
267 uniquness : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } → 264 uniquness : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } →
268 { g : Hom B (Generator a) b } → (FMap U g) o (eta a ) ≡ f → B [ solution a b f ≈ g ] 265 { g : Hom B (Generator a) b } → (FMap U g) o (eta a ) ≡ f → B [ solution a b f ≈ g ]
269 uniquness {a} {b} {f} {g} eq = 266 uniquness {a} {b} {f} {g} eq =
270 extensionality lemma-ext2 where 267 extensionality A lemma-ext2 where
271 lemma-ext2 : ( ∀( x : List a ) → (morph ( solution a b f)) x ≡ (morph g) x ) 268 lemma-ext2 : ( ∀( x : List a ) → (morph ( solution a b f)) x ≡ (morph g) x )
272 -- (morph ( solution a b f)) [] ≡ (morph g) [] ) 269 -- (morph ( solution a b f)) [] ≡ (morph g) [] )
273 lemma-ext2 [] = let open ≡-Reasoning in 270 lemma-ext2 [] = let open ≡-Reasoning in
274 begin 271 begin
275 (morph ( solution a b f)) [] 272 (morph ( solution a b f)) []
286 ≡⟨ ≡-cong ( λ k → (b < ((morph ( solution a b f)) ( x :: []) ) ∙ k > )) (lemma-ext2 xs ) ⟩ 283 ≡⟨ ≡-cong ( λ k → (b < ((morph ( solution a b f)) ( x :: []) ) ∙ k > )) (lemma-ext2 xs ) ⟩
287 b < ((morph ( solution a b f)) ( x :: []) ) ∙((morph g) ( xs )) > 284 b < ((morph ( solution a b f)) ( x :: []) ) ∙((morph g) ( xs )) >
288 ≡⟨ ≡-cong ( λ k → ( b < ( k x ) ∙ ((morph g) ( xs )) > )) ( 285 ≡⟨ ≡-cong ( λ k → ( b < ( k x ) ∙ ((morph g) ( xs )) > )) (
289 begin 286 begin
290 ( λ x → (morph ( solution a b f)) ( x :: [] ) ) 287 ( λ x → (morph ( solution a b f)) ( x :: [] ) )
291 ≡⟨ extensionality {a} lemma-ext3 ⟩ 288 ≡⟨ extensionality A {a} lemma-ext3 ⟩
292 ( λ x → (morph g) ( x :: [] ) ) 289 ( λ x → (morph g) ( x :: [] ) )
293 ∎ 290 ∎
294 ) ⟩ 291 ) ⟩
295 b < ((morph g) ( x :: [] )) ∙((morph g) ( xs )) > 292 b < ((morph g) ( x :: [] )) ∙((morph g) ( xs )) >
296 ≡⟨ sym ( homo g ) ⟩ 293 ≡⟨ sym ( homo g ) ⟩