Mercurial > hg > Members > kono > Proof > category

comparison src/free-monoid.agda @ 949:ac53803b3b2a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reorganization for apkg
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 21 Dec 2020 16:40:15 +0900
parents free-monoid.agda@3d41a8edbf63
children 40c39d3e6a75
comparison
equal deleted inserted replaced
948:dca4b29553cb 949:ac53803b3b2a
1 -- Free Monoid and it's Universal Mapping
2 ---- using Sets and forgetful functor
3
4 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
5
6 open import Category -- https://github.com/konn/category-agda
7 open import Level
8 module free-monoid { c c₁ c₂ ℓ : Level } where
9
10 open import Category.Sets
11 open import Category.Cat
12 open import HomReasoning
13 open import cat-utility
14 open import Relation.Binary.Core
15 open import universal-mapping
16 open import Relation.Binary.PropositionalEquality
17
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
38
39 infixr 40 _::_
40 data List (A : Set c ) : Set c where
41 [] : List A
42 _::_ : A → List A → List A
43
44
45 infixl 30 _++_
46 _++_ : {A : Set c } → List A → List A → List A
47 [] ++ ys = ys
48 (x :: xs) ++ ys = x :: (xs ++ ys)
49
50 list-id-l : { A : Set c } → { x : List A } → [] ++ x ≡ x
51 list-id-l {_} {_} = refl
52 list-id-r : { A : Set c } → { x : List A } → x ++ [] ≡ x
53 list-id-r {_} {[]} = refl
54 list-id-r {A} {x :: xs} = ≡-cong ( λ y → x :: y ) ( list-id-r {A} {xs} )
55 list-assoc : {A : Set c} → { xs ys zs : List A } →
56 ( xs ++ ( ys ++ zs ) ) ≡ ( ( xs ++ ys ) ++ zs )
57 list-assoc {_} {[]} {_} {_} = refl
58 list-assoc {A} {x :: xs} {ys} {zs} = ≡-cong ( λ y → x :: y )
59 ( list-assoc {A} {xs} {ys} {zs} )
60 list-o-resp-≈ : {A : Set c} → {f g : List A } → {h i : List A } →
61 f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g)
62 list-o-resp-≈ {A} refl refl = refl
63 list-isEquivalence : {A : Set c} → IsEquivalence {_} {_} {List A } _≡_
64 list-isEquivalence {A} = -- this is the same function as A's equivalence but has different types
65 record { refl = refl
66 ; sym = sym
67 ; trans = trans
68 }
69
70
71 _<_∙_> : (m : ≡-Monoid) → Carrier m → Carrier m → Carrier m
72 m < x ∙ y > = _∙_ m x y
73
74 infixr 9 _<_∙_>
75
76 record Monomorph ( a b : ≡-Monoid ) : Set c where
77 field
78 morph : Carrier a → Carrier b
79 identity : morph (ε a) ≡ ε b
80 homo : ∀{x y} → morph ( a < x ∙ y > ) ≡ b < morph x ∙ morph y >
81
82 open Monomorph
83
84 _+_ : { a b c : ≡-Monoid } → Monomorph b c → Monomorph a b → Monomorph a c
85 _+_ {a} {b} {c} f g = record {
86 morph = λ x → morph f ( morph g x ) ;
87 identity = identity1 ;
88 homo = homo1
89 } where
90 identity1 : morph f ( morph g (ε a) ) ≡ ε c
91 identity1 = let open ≡-Reasoning in begin
92 morph f (morph g (ε a))
93 ≡⟨ ≡-cong (morph f ) ( identity g ) ⟩
94 morph f (ε b)
95 ≡⟨ identity f ⟩
96 ε c
97 ∎
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 ∎
106
107 M-id : { a : ≡-Monoid } → Monomorph a a
108 M-id = record { morph = λ x → x ; identity = refl ; homo = refl }
109
110 _==_ : { a b : ≡-Monoid } → Monomorph a b → Monomorph a b → Set c
111 _==_ f g = morph f ≡ morph g
112
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 )
115 postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c
116
117 isMonoids : IsCategory ≡-Monoid Monomorph _==_ _+_ (M-id)
118 isMonoids = record { isEquivalence = isEquivalence1
119 ; identityL = refl
120 ; identityR = refl
121 ; associative = refl
122 ; o-resp-≈ = λ {a} {b} {c} {f} {g} {h} {i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i}
123 }
124 where
125 isEquivalence1 : { a b : ≡-Monoid } → IsEquivalence {_} {_} {Monomorph a b} _==_
126 isEquivalence1 = -- this is the same function as A's equivalence but has different types
127 record { refl = refl
128 ; sym = sym
129 ; trans = trans
130 }
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)
133 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f==g h==i = let open ≡-Reasoning in begin
134 morph ( h + f )
135 ≡⟨ ≡-cong ( λ g → ( ( λ (x : Carrier a ) → g x ) )) (extensionality {Carrier a} lemma11) ⟩
136 morph ( i + g )
137 ∎
138 where
139 lemma11 : (x : Carrier a) → morph (h + f) x ≡ morph (i + g) x
140 lemma11 x = let open ≡-Reasoning in begin
141 morph ( h + f ) x
142 ≡⟨⟩
143 morph h ( ( morph f ) x )
144 ≡⟨ ≡-cong ( \y -> morph h ( y x ) ) f==g ⟩
145 morph h ( morph g x )
146 ≡⟨ ≡-cong ( \y -> y ( morph g x ) ) h==i ⟩
147 morph i ( morph g x )
148 ≡⟨⟩
149 morph ( i + g ) x
150 ∎
151
152
153
154
155 Monoids : Category _ _ _
156 Monoids =
157 record { Obj = ≡-Monoid
158 ; Hom = Monomorph
159 ; _o_ = _+_
160 ; _≈_ = _==_
161 ; Id = M-id
162 ; isCategory = isMonoids
163 }
164
165 A = Sets {c}
166 B = Monoids
167
168 open Functor
169
170 U : Functor B A
171 U = record {
172 FObj = λ m → Carrier m ;
173 FMap = λ f → morph f ;
174 isFunctor = record {
175 ≈-cong = λ x → x
176 ; identity = refl
177 ; distr = refl
178 }
179 }
180
181 -- FObj
182 list : (a : Set c) → ≡-Monoid
183 list a = record {
184 Carrier = List a
185 ; _∙_ = _++_
186 ; ε = []
187 ; isMonoid = record {
188 identity = ( ( λ x → list-id-l {a} ) , ( λ x → list-id-r {a} ) ) ;
189 isSemigroup = record {
190 assoc = λ x → λ y → λ z → sym ( list-assoc {a} {x} {y} {z} )
191 ; isEquivalence = list-isEquivalence
192 ; ∙-cong = λ x → λ y → list-o-resp-≈ y x
193 }
194 }
195 }
196
197 Generator : Obj A → Obj B
198 Generator s = list s
199
200 -- solution
201
202 -- [a,b,c] → f(a) ∙ f(b) ∙ f(c)
203 Φ : {a : Obj A } {b : Obj B} ( f : Hom A a (FObj U b) ) → List a → Carrier b
204 Φ {a} {b} f [] = ε b
205 Φ {a} {b} f ( x :: xs ) = b < ( f x ) ∙ (Φ {a} {b} f xs ) >
206
207 solution : (a : Obj A ) (b : Obj B) ( f : Hom A a (FObj U b) ) → Hom B (Generator a ) b
208 solution a b f = record {
209 morph = λ (l : List a) → Φ f l ;
210 identity = refl;
211 homo = λ {x y} → homo1 x y
212 } where
213 _*_ : Carrier b → Carrier b → Carrier b
214 _*_ f g = b < f ∙ g >
215 homo1 : (x y : Carrier (Generator a)) → Φ f ( (Generator a) < x ∙ y > ) ≡ (Φ f x) * (Φ {a} {b} f y )
216 homo1 [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ f y))
217 homo1 (x :: xs) y = let open ≡-Reasoning in
218 sym ( begin
219 (Φ {a} {b} f (x :: xs)) * (Φ f y)
220 ≡⟨⟩
221 ((f x) * (Φ f xs)) * (Φ f y)
222 ≡⟨ ( IsMonoid.assoc ( isMonoid b )) _ _ _ ⟩
223 (f x) * ( (Φ f xs) * (Φ f y) )
224 ≡⟨ sym ( (IsMonoid.∙-cong (isMonoid b)) refl (homo1 xs y )) ⟩
225 (f x) * ( Φ f ( xs ++ y ) )
226 ≡⟨⟩
227 Φ {a} {b} f ( x :: ( xs ++ y ) )
228 ≡⟨⟩
229 Φ {a} {b} f ( (x :: xs) ++ y )
230 ≡⟨⟩
231 Φ {a} {b} f ((Generator a) < ( x :: xs) ∙ y > )
232 ∎ )
233
234 eta : (a : Obj A) → Hom A a ( FObj U (Generator a) )
235 eta a = λ ( x : a ) → x :: []
236
237 FreeMonoidUniveralMapping : UniversalMapping A B U
238 FreeMonoidUniveralMapping =
239 record {
240 F = Generator ;
241 η = eta ;
242 _* = λ {a b} → λ f → solution a b f ;
243 isUniversalMapping = record {
244 universalMapping = λ {a b f} → universalMapping {a} {b} {f} ;
245 uniquness = λ {a b f g} → uniquness {a} {b} {f} {g}
246 }
247 } where
248 universalMapping : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } → FMap U ( solution a b f ) o eta a ≡ f
249 universalMapping {a} {b} {f} = let open ≡-Reasoning in
250 begin
251 FMap U ( solution a b f ) o eta a
252 ≡⟨⟩
253 ( λ (x : a ) → Φ {a} {b} f (eta a x) )
254 ≡⟨⟩
255 ( λ (x : a ) → Φ {a} {b} f ( x :: [] ) )
256 ≡⟨⟩
257 ( λ (x : a ) → b < ( f x ) ∙ (Φ {a} {b} f [] ) > )
258 ≡⟨⟩
259 ( λ (x : a ) → b < ( f x ) ∙ ( ε b ) > )
260 ≡⟨ ≡-cong ( λ g → ( ( λ (x : a ) → g x ) )) (extensionality {a} lemma-ext1) ⟩
261 ( λ (x : a ) → f x )
262 ≡⟨⟩
263 f
264 ∎ where
265 lemma-ext1 : ∀( x : a ) → b < ( f x ) ∙ ( ε b ) > ≡ f x
266 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) } →
268 { 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 =
270 extensionality lemma-ext2 where
271 lemma-ext2 : ( ∀( x : List a ) → (morph ( solution a b f)) x ≡ (morph g) x )
272 -- (morph ( solution a b f)) [] ≡ (morph g) [] )
273 lemma-ext2 [] = let open ≡-Reasoning in
274 begin
275 (morph ( solution a b f)) []
276 ≡⟨ identity ( solution a b f) ⟩
277 ε b
278 ≡⟨ sym ( identity g ) ⟩
279 (morph g) []
280 ∎
281 lemma-ext2 (x :: xs) = let open ≡-Reasoning in
282 begin
283 (morph ( solution a b f)) ( x :: xs )
284 ≡⟨ homo ( solution a b f) {x :: []} {xs} ⟩
285 b < ((morph ( solution a b f)) ( x :: []) ) ∙ ((morph ( solution a b f)) xs ) >
286 ≡⟨ ≡-cong ( λ k → (b < ((morph ( solution a b f)) ( x :: []) ) ∙ k > )) (lemma-ext2 xs ) ⟩
287 b < ((morph ( solution a b f)) ( x :: []) ) ∙((morph g) ( xs )) >
288 ≡⟨ ≡-cong ( λ k → ( b < ( k x ) ∙ ((morph g) ( xs )) > )) (
289 begin
290 ( λ x → (morph ( solution a b f)) ( x :: [] ) )
291 ≡⟨ extensionality {a} lemma-ext3 ⟩
292 ( λ x → (morph g) ( x :: [] ) )
293 ∎
294 ) ⟩
295 b < ((morph g) ( x :: [] )) ∙((morph g) ( xs )) >
296 ≡⟨ sym ( homo g ) ⟩
297 (morph g) ( x :: xs )
298 ∎ where
299 lemma-ext3 : ∀( x : a ) → (morph ( solution a b f)) (x :: []) ≡ (morph g) ( x :: [] )
300 lemma-ext3 x = let open ≡-Reasoning in
301 begin
302 (morph ( solution a b f)) (x :: [])
303 ≡⟨ ( proj₂ ( IsMonoid.identity ( isMonoid b) )(f x) ) ⟩
304 f x
305 ≡⟨ sym ( ≡-cong (λ f → f x ) eq ) ⟩
306 (morph g) ( x :: [] )
307 ∎
308
309 open NTrans
310 -- fm-ε b = Φ
311
312 fm-ε : NTrans B B ( ( FunctorF A B FreeMonoidUniveralMapping) ○ U) identityFunctor
313 fm-ε = nat-ε A B FreeMonoidUniveralMapping
314 -- TMap = λ a → solution (FObj U a) a (λ x → x ) ;
315 -- isNTrans = record {
316 -- commute = commute1
317 -- }
318 -- } where
319 -- commute1 : {a b : Obj B} {f : Hom B a b} → let open ≈-Reasoning B renaming (_o_ to _*_ ) in
320 -- ( FMap (identityFunctor {_} {_} {_} {B}) f * solution (FObj U a) a (λ x → x) ) ≈
321 -- ( solution (FObj U b) b (λ x → x) * FMap (FunctorF A B FreeMonoidUniveralMapping ○ U) f )
322 -- commute1 {a} {b} {f} = let open ≡-Reasoning in begin
323 -- morph ((B ≈-Reasoning.o FMap identityFunctor f) (solution (FObj U a) a (λ x → x)))
324 -- ≡⟨ {!!} ⟩
325 -- morph ((B ≈-Reasoning.o solution (FObj U b) b (λ x → x)) (FMap (FunctorF A B FreeMonoidUniveralMapping ○ U) f))
326 -- ∎
327
328
329 fm-η : NTrans A A identityFunctor ( U ○ ( FunctorF A B FreeMonoidUniveralMapping) )
330 fm-η = record {
331 TMap = λ a → λ (x : a) → x :: [] ;
332 isNTrans = record {
333 commute = commute1
334 }
335 } where
336 commute1 : {a b : Obj A} {f : Hom A a b} → let open ≈-Reasoning A renaming (_o_ to _*_ ) in
337 (( FMap (U ○ FunctorF A B FreeMonoidUniveralMapping) f ) * (λ x → x :: []) ) ≈ ( (λ x → x :: []) * (λ z → FMap (identityFunctor {_} {_} {_} {A}) f z ) )
338 commute1 {a} {b} {f} = refl -- λ (x : a ) → f x :: []
339
340
341 -- A = Sets {c}
342 -- B = Monoids
343 -- U underline funcotr
344 -- F generator = x :: []
345 -- Eta x :: []
346 -- Epsiron morph = Φ
347
348 adj = UMAdjunction A B U FreeMonoidUniveralMapping
349
350
351
352