Mercurial > hg > Members > kono > Proof > category
annotate src/free-monoid.agda @ 1110:45de2b31bf02
add original library and fix for safe mode
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 07 Oct 2023 19:43:31 +0900 |
| parents | 40c39d3e6a75 |
| children |
| rev | line source |
|---|---|
|
167
c3863043c4a3
Free Monoid and Universal mapping problem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
166
diff
changeset
|
1 -- Free Monoid and it's Universal Mapping |
|
c3863043c4a3
Free Monoid and Universal mapping problem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
166
diff
changeset
|
2 ---- using Sets and forgetful functor |
| 155 | 3 |
| 162 | 4 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
| 5 | |
|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1034
diff
changeset
|
6 {-# OPTIONS --cubical-compatible --safe #-} |
|
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1034
diff
changeset
|
7 |
| 154 | 8 open import Category -- https://github.com/konn/category-agda |
| 9 open import Level | |
| 10 module free-monoid { c c₁ c₂ ℓ : Level } where | |
| 11 | |
|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1034
diff
changeset
|
12 open import Category.Sets hiding (_==_) |
| 154 | 13 open import Category.Cat |
| 14 open import HomReasoning | |
|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1034
diff
changeset
|
15 open import Definitions |
| 1034 | 16 open import Relation.Binary.Structures |
| 178 | 17 open import universal-mapping |
|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1034
diff
changeset
|
18 open import Relation.Binary.PropositionalEquality |
| 154 | 19 |
| 162 | 20 -- from https://github.com/danr/Agda-projects/blob/master/Category-Theory/FreeMonoid.agda |
| 154 | 21 |
| 1034 | 22 open import Algebra.Definitions -- using (Op₁; Op₂) |
| 23 open import Algebra.Core | |
| 342 | 24 open import Algebra.Structures |
| 25 open import Data.Product | |
| 26 | |
| 27 record ≡-Monoid : Set (suc c) where | |
| 28 infixr 9 _∙_ | |
| 29 field | |
| 30 Carrier : Set c | |
| 31 _∙_ : Op₂ Carrier | |
| 32 ε : Carrier | |
| 33 isMonoid : IsMonoid _≡_ _∙_ ε | |
| 34 | |
| 35 open ≡-Monoid | |
| 36 | |
| 37 ≡-cong = Relation.Binary.PropositionalEquality.cong | |
| 38 | |
| 39 -- module ≡-reasoning (m : ≡-Monoid ) where | |
| 40 | |
| 154 | 41 infixr 40 _::_ |
| 156 | 42 data List (A : Set c ) : Set c where |
| 154 | 43 [] : List A |
| 254 | 44 _::_ : A → List A → List A |
| 154 | 45 |
| 46 | |
| 47 infixl 30 _++_ | |
| 254 | 48 _++_ : {A : Set c } → List A → List A → List A |
| 154 | 49 [] ++ ys = ys |
| 50 (x :: xs) ++ ys = x :: (xs ++ ys) | |
| 51 | |
| 254 | 52 list-id-l : { A : Set c } → { x : List A } → [] ++ x ≡ x |
| 156 | 53 list-id-l {_} {_} = refl |
| 254 | 54 list-id-r : { A : Set c } → { x : List A } → x ++ [] ≡ x |
| 156 | 55 list-id-r {_} {[]} = refl |
| 254 | 56 list-id-r {A} {x :: xs} = ≡-cong ( λ y → x :: y ) ( list-id-r {A} {xs} ) |
| 57 list-assoc : {A : Set c} → { xs ys zs : List A } → | |
| 156 | 58 ( xs ++ ( ys ++ zs ) ) ≡ ( ( xs ++ ys ) ++ zs ) |
| 59 list-assoc {_} {[]} {_} {_} = refl | |
| 254 | 60 list-assoc {A} {x :: xs} {ys} {zs} = ≡-cong ( λ y → x :: y ) |
| 156 | 61 ( list-assoc {A} {xs} {ys} {zs} ) |
| 254 | 62 list-o-resp-≈ : {A : Set c} → {f g : List A } → {h i : List A } → |
| 156 | 63 f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g) |
| 64 list-o-resp-≈ {A} refl refl = refl | |
| 254 | 65 list-isEquivalence : {A : Set c} → IsEquivalence {_} {_} {List A } _≡_ |
| 156 | 66 list-isEquivalence {A} = -- this is the same function as A's equivalence but has different types |
| 67 record { refl = refl | |
| 68 ; sym = sym | |
| 69 ; trans = trans | |
| 70 } | |
| 154 | 71 |
| 72 | |
| 342 | 73 _<_∙_> : (m : ≡-Monoid) → Carrier m → Carrier m → Carrier m |
| 74 m < x ∙ y > = _∙_ m x y | |
| 154 | 75 |
| 342 | 76 infixr 9 _<_∙_> |
| 154 | 77 |
| 421 | 78 record Monomorph ( a b : ≡-Monoid ) : Set c where |
| 154 | 79 field |
| 254 | 80 morph : Carrier a → Carrier b |
| 154 | 81 identity : morph (ε a) ≡ ε b |
| 342 | 82 homo : ∀{x y} → morph ( a < x ∙ y > ) ≡ b < morph x ∙ morph y > |
| 154 | 83 |
| 84 open Monomorph | |
| 85 | |
| 254 | 86 _+_ : { a b c : ≡-Monoid } → Monomorph b c → Monomorph a b → Monomorph a c |
| 155 | 87 _+_ {a} {b} {c} f g = record { |
| 254 | 88 morph = λ x → morph f ( morph g x ) ; |
| 154 | 89 identity = identity1 ; |
| 168 | 90 homo = homo1 |
| 154 | 91 } where |
| 92 identity1 : morph f ( morph g (ε a) ) ≡ ε c | |
| 342 | 93 identity1 = let open ≡-Reasoning in begin |
| 94 morph f (morph g (ε a)) | |
| 95 ≡⟨ ≡-cong (morph f ) ( identity g ) ⟩ | |
| 96 morph f (ε b) | |
| 97 ≡⟨ identity f ⟩ | |
| 98 ε c | |
| 99 ∎ | |
| 100 homo1 : ∀{x y} → morph f ( morph g ( a < x ∙ y > )) ≡ ( c < (morph f (morph g x )) ∙(morph f (morph g y) ) > ) | |
| 101 homo1 {x} {y} = let open ≡-Reasoning in begin | |
| 102 morph f (morph g (a < x ∙ y >)) | |
| 103 ≡⟨ ≡-cong (morph f ) ( homo g) ⟩ | |
| 104 morph f (b < morph g x ∙ morph g y >) | |
| 105 ≡⟨ homo f ⟩ | |
| 106 c < morph f (morph g x) ∙ morph f (morph g y) > | |
| 107 ∎ | |
| 154 | 108 |
| 254 | 109 M-id : { a : ≡-Monoid } → Monomorph a a |
| 110 M-id = record { morph = λ x → x ; identity = refl ; homo = refl } | |
| 154 | 111 |
| 254 | 112 _==_ : { a b : ≡-Monoid } → Monomorph a b → Monomorph a b → Set c |
| 155 | 113 _==_ f g = morph f ≡ morph g |
| 114 | |
| 421 | 115 -- Functional Extensionality Axiom (We cannot prove this in Agda / Coq, just assumming ) |
| 116 -- postulate extensionality : { a b : Obj A } {f g : Hom A a b } → (∀ {x} → (f x ≡ g x)) → ( f ≡ g ) | |
| 1034 | 117 -- postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c |
| 421 | 118 |
| 168 | 119 isMonoids : IsCategory ≡-Monoid Monomorph _==_ _+_ (M-id) |
| 120 isMonoids = record { isEquivalence = isEquivalence1 | |
| 155 | 121 ; identityL = refl |
| 122 ; identityR = refl | |
| 123 ; associative = refl | |
| 254 | 124 ; o-resp-≈ = λ {a} {b} {c} {f} {g} {h} {i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} |
| 155 | 125 } |
| 126 where | |
| 254 | 127 isEquivalence1 : { a b : ≡-Monoid } → IsEquivalence {_} {_} {Monomorph a b} _==_ |
| 155 | 128 isEquivalence1 = -- this is the same function as A's equivalence but has different types |
| 129 record { refl = refl | |
| 130 ; sym = sym | |
| 131 ; trans = trans | |
| 132 } | |
| 421 | 133 o-resp-≈ : {a b c : ≡-Monoid } {f g : Monomorph a b } → {h i : Monomorph b c } → |
|
420
3e44951b9bdb
refl in free-monoid trouble
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
343
diff
changeset
|
134 f == g → h == i → (h + f) == (i + g) |
| 421 | 135 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f==g h==i = let open ≡-Reasoning in begin |
| 136 morph ( h + f ) | |
|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1034
diff
changeset
|
137 ≡⟨ ≡-cong ( λ g → ( ( λ (x : Carrier a ) → g x ) )) ? ⟩ -- (extensionality (Sets ) {Carrier a} lemma11) ⟩ |
| 421 | 138 morph ( i + g ) |
| 139 ∎ | |
| 140 where | |
| 141 lemma11 : (x : Carrier a) → morph (h + f) x ≡ morph (i + g) x | |
| 142 lemma11 x = let open ≡-Reasoning in begin | |
| 143 morph ( h + f ) x | |
| 144 ≡⟨⟩ | |
| 145 morph h ( ( morph f ) x ) | |
| 146 ≡⟨ ≡-cong ( \y -> morph h ( y x ) ) f==g ⟩ | |
| 147 morph h ( morph g x ) | |
| 148 ≡⟨ ≡-cong ( \y -> y ( morph g x ) ) h==i ⟩ | |
| 149 morph i ( morph g x ) | |
| 150 ≡⟨⟩ | |
| 151 morph ( i + g ) x | |
| 152 ∎ | |
| 153 | |
| 154 | |
| 155 | |
|
420
3e44951b9bdb
refl in free-monoid trouble
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
343
diff
changeset
|
156 |
| 168 | 157 Monoids : Category _ _ _ |
| 158 Monoids = | |
| 155 | 159 record { Obj = ≡-Monoid |
| 160 ; Hom = Monomorph | |
| 161 ; _o_ = _+_ | |
| 162 ; _≈_ = _==_ | |
| 163 ; Id = M-id | |
| 168 | 164 ; isCategory = isMonoids |
| 155 | 165 } |
| 154 | 166 |
| 156 | 167 A = Sets {c} |
| 168 | 168 B = Monoids |
| 154 | 169 |
| 156 | 170 open Functor |
| 154 | 171 |
| 156 | 172 U : Functor B A |
| 173 U = record { | |
| 254 | 174 FObj = λ m → Carrier m ; |
| 175 FMap = λ f → morph f ; | |
| 156 | 176 isFunctor = record { |
| 254 | 177 ≈-cong = λ x → x |
| 156 | 178 ; identity = refl |
| 179 ; distr = refl | |
| 180 } | |
| 181 } | |
| 154 | 182 |
| 156 | 183 -- FObj |
| 254 | 184 list : (a : Set c) → ≡-Monoid |
| 159 | 185 list a = record { |
| 186 Carrier = List a | |
| 342 | 187 ; _∙_ = _++_ |
| 159 | 188 ; ε = [] |
| 1034 | 189 ; isMonoid = record { isSemigroup = record { isMagma = record { |
| 190 isEquivalence = list-isEquivalence | |
| 191 ; ∙-cong = λ x → λ y → list-o-resp-≈ y x } | |
| 192 ; assoc = λ x → λ y → λ z → sym ( list-assoc {a} {x} {y} {z} ) } | |
| 193 ; identity = ( ( λ x → list-id-l {a} ) , ( λ x → list-id-r {a} ) ) | |
| 194 } } | |
| 159 | 195 |
| 254 | 196 Generator : Obj A → Obj B |
| 156 | 197 Generator s = list s |
| 198 | |
|
157
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
199 -- solution |
|
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
200 |
|
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
201 -- [a,b,c] → f(a) ∙ f(b) ∙ f(c) |
|
341
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
202 Φ : {a : Obj A } {b : Obj B} ( f : Hom A a (FObj U b) ) → List a → Carrier b |
|
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
203 Φ {a} {b} f [] = ε b |
| 342 | 204 Φ {a} {b} f ( x :: xs ) = b < ( f x ) ∙ (Φ {a} {b} f xs ) > |
| 161 | 205 |
| 206 solution : (a : Obj A ) (b : Obj B) ( f : Hom A a (FObj U b) ) → Hom B (Generator a ) b | |
| 207 solution a b f = record { | |
|
341
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
208 morph = λ (l : List a) → Φ f l ; |
|
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
209 identity = refl; |
| 254 | 210 homo = λ {x y} → homo1 x y |
| 161 | 211 } where |
| 254 | 212 _*_ : Carrier b → Carrier b → Carrier b |
| 342 | 213 _*_ f g = b < f ∙ g > |
| 214 homo1 : (x y : Carrier (Generator a)) → Φ f ( (Generator a) < x ∙ y > ) ≡ (Φ f x) * (Φ {a} {b} f y ) | |
|
341
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
215 homo1 [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ f y)) |
| 168 | 216 homo1 (x :: xs) y = let open ≡-Reasoning in |
| 161 | 217 sym ( begin |
|
341
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
218 (Φ {a} {b} f (x :: xs)) * (Φ f y) |
| 161 | 219 ≡⟨⟩ |
|
341
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
220 ((f x) * (Φ f xs)) * (Φ f y) |
| 161 | 221 ≡⟨ ( IsMonoid.assoc ( isMonoid b )) _ _ _ ⟩ |
|
341
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
222 (f x) * ( (Φ f xs) * (Φ f y) ) |
| 168 | 223 ≡⟨ sym ( (IsMonoid.∙-cong (isMonoid b)) refl (homo1 xs y )) ⟩ |
|
341
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
224 (f x) * ( Φ f ( xs ++ y ) ) |
| 161 | 225 ≡⟨⟩ |
|
341
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
226 Φ {a} {b} f ( x :: ( xs ++ y ) ) |
| 161 | 227 ≡⟨⟩ |
|
341
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
228 Φ {a} {b} f ( (x :: xs) ++ y ) |
| 161 | 229 ≡⟨⟩ |
| 342 | 230 Φ {a} {b} f ((Generator a) < ( x :: xs) ∙ y > ) |
| 161 | 231 ∎ ) |
| 232 | |
| 162 | 233 eta : (a : Obj A) → Hom A a ( FObj U (Generator a) ) |
| 254 | 234 eta a = λ ( x : a ) → x :: [] |
| 162 | 235 |
|
690
3d41a8edbf63
fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
689
diff
changeset
|
236 FreeMonoidUniveralMapping : UniversalMapping A B U |
| 162 | 237 FreeMonoidUniveralMapping = |
|
157
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
238 record { |
|
690
3d41a8edbf63
fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
689
diff
changeset
|
239 F = Generator ; |
|
3d41a8edbf63
fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
689
diff
changeset
|
240 η = eta ; |
| 254 | 241 _* = λ {a b} → λ f → solution a b f ; |
|
157
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
242 isUniversalMapping = record { |
| 254 | 243 universalMapping = λ {a b f} → universalMapping {a} {b} {f} ; |
| 244 uniquness = λ {a b f g} → uniquness {a} {b} {f} {g} | |
|
157
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
245 } |
| 159 | 246 } where |
|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1034
diff
changeset
|
247 universalMapping : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } → ? -- FMap U ( solution a b f ) o eta a ≡ f |
|
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1034
diff
changeset
|
248 universalMapping {a} {b} {f} = |
| 159 | 249 begin |
| 160 | 250 FMap U ( solution a b f ) o eta a |
|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1034
diff
changeset
|
251 ≡⟨ refl ⟩ |
|
341
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
252 ( λ (x : a ) → Φ {a} {b} f (eta a x) ) |
|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1034
diff
changeset
|
253 ≡⟨ refl ⟩ |
|
341
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
254 ( λ (x : a ) → Φ {a} {b} f ( x :: [] ) ) |
|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1034
diff
changeset
|
255 ≡⟨ refl ⟩ |
| 342 | 256 ( λ (x : a ) → b < ( f x ) ∙ (Φ {a} {b} f [] ) > ) |
|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1034
diff
changeset
|
257 ≡⟨ refl ⟩ |
| 342 | 258 ( λ (x : a ) → b < ( f x ) ∙ ( ε b ) > ) |
| 1034 | 259 ≡⟨ ≡-cong ( λ g → ( ( λ (x : a ) → g x ) )) (extensionality A {a} lemma-ext1) ⟩ |
| 162 | 260 ( λ (x : a ) → f x ) |
|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1034
diff
changeset
|
261 ≡⟨ refl ⟩ |
| 162 | 262 f |
| 263 ∎ where | |
|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1034
diff
changeset
|
264 open ≡-Reasoning |
| 342 | 265 lemma-ext1 : ∀( x : a ) → b < ( f x ) ∙ ( ε b ) > ≡ f x |
|
169
44bf6e78f891
builtin extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
168
diff
changeset
|
266 lemma-ext1 x = ( proj₂ ( IsMonoid.identity ( isMonoid b) ) ) (f x) |
| 159 | 267 uniquness : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } → |
| 160 | 268 { g : Hom B (Generator a) b } → (FMap U g) o (eta a ) ≡ f → B [ solution a b f ≈ g ] |
|
163
bc47179e3c9c
uniqueness continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
162
diff
changeset
|
269 uniquness {a} {b} {f} {g} eq = |
| 1034 | 270 extensionality A lemma-ext2 where |
| 254 | 271 lemma-ext2 : ( ∀( x : List a ) → (morph ( solution a b f)) x ≡ (morph g) x ) |
|
163
bc47179e3c9c
uniqueness continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
162
diff
changeset
|
272 -- (morph ( solution a b f)) [] ≡ (morph g) [] ) |
|
169
44bf6e78f891
builtin extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
168
diff
changeset
|
273 lemma-ext2 [] = let open ≡-Reasoning in |
| 164 | 274 begin |
| 275 (morph ( solution a b f)) [] | |
| 276 ≡⟨ identity ( solution a b f) ⟩ | |
| 277 ε b | |
| 278 ≡⟨ sym ( identity g ) ⟩ | |
| 279 (morph g) [] | |
| 280 ∎ | |
|
169
44bf6e78f891
builtin extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
168
diff
changeset
|
281 lemma-ext2 (x :: xs) = let open ≡-Reasoning in |
| 164 | 282 begin |
| 283 (morph ( solution a b f)) ( x :: xs ) | |
| 168 | 284 ≡⟨ homo ( solution a b f) {x :: []} {xs} ⟩ |
| 342 | 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 )) > )) ( | |
| 164 | 289 begin |
| 254 | 290 ( λ x → (morph ( solution a b f)) ( x :: [] ) ) |
| 1034 | 291 ≡⟨ extensionality A {a} lemma-ext3 ⟩ |
| 254 | 292 ( λ x → (morph g) ( x :: [] ) ) |
| 164 | 293 ∎ |
| 294 ) ⟩ | |
| 342 | 295 b < ((morph g) ( x :: [] )) ∙((morph g) ( xs )) > |
| 168 | 296 ≡⟨ sym ( homo g ) ⟩ |
| 164 | 297 (morph g) ( x :: xs ) |
| 298 ∎ where | |
| 254 | 299 lemma-ext3 : ∀( x : a ) → (morph ( solution a b f)) (x :: []) ≡ (morph g) ( x :: [] ) |
|
169
44bf6e78f891
builtin extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
168
diff
changeset
|
300 lemma-ext3 x = let open ≡-Reasoning in |
| 166 | 301 begin |
| 302 (morph ( solution a b f)) (x :: []) | |
| 303 ≡⟨ ( proj₂ ( IsMonoid.identity ( isMonoid b) )(f x) ) ⟩ | |
| 304 f x | |
| 254 | 305 ≡⟨ sym ( ≡-cong (λ f → f x ) eq ) ⟩ |
| 166 | 306 (morph g) ( x :: [] ) |
| 307 ∎ | |
| 308 | |
| 178 | 309 open NTrans |
| 310 -- fm-ε b = Φ | |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
421
diff
changeset
|
311 |
| 178 | 312 fm-ε : NTrans B B ( ( FunctorF A B FreeMonoidUniveralMapping) ○ U) identityFunctor |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
421
diff
changeset
|
313 fm-ε = nat-ε A B FreeMonoidUniveralMapping |
| 343 | 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 | |
|
157
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
340 |
|
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
341 -- A = Sets {c} |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
342 -- B = Monoids |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
343 -- U underline funcotr |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
344 -- F generator = x :: [] |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
345 -- Eta x :: [] |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
346 -- Epsiron morph = Φ |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
347 |
|
690
3d41a8edbf63
fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
689
diff
changeset
|
348 adj = UMAdjunction A B U FreeMonoidUniveralMapping |
|
167
c3863043c4a3
Free Monoid and Universal mapping problem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
166
diff
changeset
|
349 |
|
c3863043c4a3
Free Monoid and Universal mapping problem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
166
diff
changeset
|
350 |
|
c3863043c4a3
Free Monoid and Universal mapping problem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
166
diff
changeset
|
351 |
|
c3863043c4a3
Free Monoid and Universal mapping problem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
166
diff
changeset
|
352 |