Mercurial > hg > Members > kono > Proof > category
annotate free-monoid.agda @ 478:dc24ac6ebdb3
Comma category
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 09 Mar 2017 09:03:07 +0900 |
| parents | 06ffcad985ac |
| children | a5f2ca67e7c5 |
| 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 | |
| 154 | 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 | |
| 178 | 15 open import universal-mapping |
| 342 | 16 open import Relation.Binary.PropositionalEquality |
| 154 | 17 |
| 162 | 18 -- from https://github.com/danr/Agda-projects/blob/master/Category-Theory/FreeMonoid.agda |
| 154 | 19 |
| 342 | 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 | |
| 154 | 39 infixr 40 _::_ |
| 156 | 40 data List (A : Set c ) : Set c where |
| 154 | 41 [] : List A |
| 254 | 42 _::_ : A → List A → List A |
| 154 | 43 |
| 44 | |
| 45 infixl 30 _++_ | |
| 254 | 46 _++_ : {A : Set c } → List A → List A → List A |
| 154 | 47 [] ++ ys = ys |
| 48 (x :: xs) ++ ys = x :: (xs ++ ys) | |
| 49 | |
| 254 | 50 list-id-l : { A : Set c } → { x : List A } → [] ++ x ≡ x |
| 156 | 51 list-id-l {_} {_} = refl |
| 254 | 52 list-id-r : { A : Set c } → { x : List A } → x ++ [] ≡ x |
| 156 | 53 list-id-r {_} {[]} = refl |
| 254 | 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 } → | |
| 156 | 56 ( xs ++ ( ys ++ zs ) ) ≡ ( ( xs ++ ys ) ++ zs ) |
| 57 list-assoc {_} {[]} {_} {_} = refl | |
| 254 | 58 list-assoc {A} {x :: xs} {ys} {zs} = ≡-cong ( λ y → x :: y ) |
| 156 | 59 ( list-assoc {A} {xs} {ys} {zs} ) |
| 254 | 60 list-o-resp-≈ : {A : Set c} → {f g : List A } → {h i : List A } → |
| 156 | 61 f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g) |
| 62 list-o-resp-≈ {A} refl refl = refl | |
| 254 | 63 list-isEquivalence : {A : Set c} → IsEquivalence {_} {_} {List A } _≡_ |
| 156 | 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 } | |
| 154 | 69 |
| 70 | |
| 342 | 71 _<_∙_> : (m : ≡-Monoid) → Carrier m → Carrier m → Carrier m |
| 72 m < x ∙ y > = _∙_ m x y | |
| 154 | 73 |
| 342 | 74 infixr 9 _<_∙_> |
| 154 | 75 |
| 421 | 76 record Monomorph ( a b : ≡-Monoid ) : Set c where |
| 154 | 77 field |
| 254 | 78 morph : Carrier a → Carrier b |
| 154 | 79 identity : morph (ε a) ≡ ε b |
| 342 | 80 homo : ∀{x y} → morph ( a < x ∙ y > ) ≡ b < morph x ∙ morph y > |
| 154 | 81 |
| 82 open Monomorph | |
| 83 | |
| 254 | 84 _+_ : { a b c : ≡-Monoid } → Monomorph b c → Monomorph a b → Monomorph a c |
| 155 | 85 _+_ {a} {b} {c} f g = record { |
| 254 | 86 morph = λ x → morph f ( morph g x ) ; |
| 154 | 87 identity = identity1 ; |
| 168 | 88 homo = homo1 |
| 154 | 89 } where |
| 90 identity1 : morph f ( morph g (ε a) ) ≡ ε c | |
| 342 | 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 ∎ | |
| 154 | 106 |
| 254 | 107 M-id : { a : ≡-Monoid } → Monomorph a a |
| 108 M-id = record { morph = λ x → x ; identity = refl ; homo = refl } | |
| 154 | 109 |
| 254 | 110 _==_ : { a b : ≡-Monoid } → Monomorph a b → Monomorph a b → Set c |
| 155 | 111 _==_ f g = morph f ≡ morph g |
| 112 | |
| 421 | 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 | |
| 168 | 117 isMonoids : IsCategory ≡-Monoid Monomorph _==_ _+_ (M-id) |
| 118 isMonoids = record { isEquivalence = isEquivalence1 | |
| 155 | 119 ; identityL = refl |
| 120 ; identityR = refl | |
| 121 ; associative = refl | |
| 254 | 122 ; o-resp-≈ = λ {a} {b} {c} {f} {g} {h} {i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} |
| 155 | 123 } |
| 124 where | |
| 254 | 125 isEquivalence1 : { a b : ≡-Monoid } → IsEquivalence {_} {_} {Monomorph a b} _==_ |
| 155 | 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 } | |
| 421 | 131 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
|
132 f == g → h == i → (h + f) == (i + g) |
| 421 | 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 | |
|
420
3e44951b9bdb
refl in free-monoid trouble
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
343
diff
changeset
|
154 |
| 168 | 155 Monoids : Category _ _ _ |
| 156 Monoids = | |
| 155 | 157 record { Obj = ≡-Monoid |
| 158 ; Hom = Monomorph | |
| 159 ; _o_ = _+_ | |
| 160 ; _≈_ = _==_ | |
| 161 ; Id = M-id | |
| 168 | 162 ; isCategory = isMonoids |
| 155 | 163 } |
| 154 | 164 |
| 156 | 165 A = Sets {c} |
| 168 | 166 B = Monoids |
| 154 | 167 |
| 156 | 168 open Functor |
| 154 | 169 |
| 156 | 170 U : Functor B A |
| 171 U = record { | |
| 254 | 172 FObj = λ m → Carrier m ; |
| 173 FMap = λ f → morph f ; | |
| 156 | 174 isFunctor = record { |
| 254 | 175 ≈-cong = λ x → x |
| 156 | 176 ; identity = refl |
| 177 ; distr = refl | |
| 178 } | |
| 179 } | |
| 154 | 180 |
| 156 | 181 -- FObj |
| 254 | 182 list : (a : Set c) → ≡-Monoid |
| 159 | 183 list a = record { |
| 184 Carrier = List a | |
| 342 | 185 ; _∙_ = _++_ |
| 159 | 186 ; ε = [] |
| 187 ; isMonoid = record { | |
| 254 | 188 identity = ( ( λ x → list-id-l {a} ) , ( λ x → list-id-r {a} ) ) ; |
| 159 | 189 isSemigroup = record { |
| 254 | 190 assoc = λ x → λ y → λ z → sym ( list-assoc {a} {x} {y} {z} ) |
| 159 | 191 ; isEquivalence = list-isEquivalence |
| 254 | 192 ; ∙-cong = λ x → λ y → list-o-resp-≈ y x |
| 159 | 193 } |
| 194 } | |
| 195 } | |
| 196 | |
| 254 | 197 Generator : Obj A → Obj B |
| 156 | 198 Generator s = list s |
| 199 | |
|
157
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
200 -- solution |
|
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
201 |
| 159 | 202 open UniversalMapping |
| 158 | 203 |
|
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
204 -- [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
|
205 Φ : {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
|
206 Φ {a} {b} f [] = ε b |
| 342 | 207 Φ {a} {b} f ( x :: xs ) = b < ( f x ) ∙ (Φ {a} {b} f xs ) > |
| 161 | 208 |
| 209 solution : (a : Obj A ) (b : Obj B) ( f : Hom A a (FObj U b) ) → Hom B (Generator a ) b | |
| 210 solution a b f = record { | |
|
341
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
211 morph = λ (l : List a) → Φ f l ; |
|
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
212 identity = refl; |
| 254 | 213 homo = λ {x y} → homo1 x y |
| 161 | 214 } where |
| 254 | 215 _*_ : Carrier b → Carrier b → Carrier b |
| 342 | 216 _*_ f g = b < f ∙ g > |
| 217 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
|
218 homo1 [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ f y)) |
| 168 | 219 homo1 (x :: xs) y = let open ≡-Reasoning in |
| 161 | 220 sym ( begin |
|
341
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
221 (Φ {a} {b} f (x :: xs)) * (Φ f y) |
| 161 | 222 ≡⟨⟩ |
|
341
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
223 ((f x) * (Φ f xs)) * (Φ f y) |
| 161 | 224 ≡⟨ ( IsMonoid.assoc ( isMonoid b )) _ _ _ ⟩ |
|
341
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
225 (f x) * ( (Φ f xs) * (Φ f y) ) |
| 168 | 226 ≡⟨ 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
|
227 (f x) * ( Φ f ( xs ++ y ) ) |
| 161 | 228 ≡⟨⟩ |
|
341
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
229 Φ {a} {b} f ( x :: ( xs ++ y ) ) |
| 161 | 230 ≡⟨⟩ |
|
341
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
231 Φ {a} {b} f ( (x :: xs) ++ y ) |
| 161 | 232 ≡⟨⟩ |
| 342 | 233 Φ {a} {b} f ((Generator a) < ( x :: xs) ∙ y > ) |
| 161 | 234 ∎ ) |
| 235 | |
| 162 | 236 eta : (a : Obj A) → Hom A a ( FObj U (Generator a) ) |
| 254 | 237 eta a = λ ( x : a ) → x :: [] |
| 162 | 238 |
| 159 | 239 FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta |
| 162 | 240 FreeMonoidUniveralMapping = |
|
157
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
241 record { |
| 254 | 242 _* = λ {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
|
243 isUniversalMapping = record { |
| 254 | 244 universalMapping = λ {a b f} → universalMapping {a} {b} {f} ; |
| 245 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
|
246 } |
| 159 | 247 } where |
| 160 | 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 |
| 159 | 249 universalMapping {a} {b} {f} = let open ≡-Reasoning in |
| 250 begin | |
| 160 | 251 FMap U ( solution a b f ) o eta a |
| 161 | 252 ≡⟨⟩ |
|
341
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
253 ( λ (x : a ) → Φ {a} {b} f (eta a x) ) |
| 162 | 254 ≡⟨⟩ |
|
341
33bc037319fa
minor fix on free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
254
diff
changeset
|
255 ( λ (x : a ) → Φ {a} {b} f ( x :: [] ) ) |
| 162 | 256 ≡⟨⟩ |
| 342 | 257 ( λ (x : a ) → b < ( f x ) ∙ (Φ {a} {b} f [] ) > ) |
| 162 | 258 ≡⟨⟩ |
| 342 | 259 ( λ (x : a ) → b < ( f x ) ∙ ( ε b ) > ) |
| 254 | 260 ≡⟨ ≡-cong ( λ g → ( ( λ (x : a ) → g x ) )) (extensionality {a} lemma-ext1) ⟩ |
| 162 | 261 ( λ (x : a ) → f x ) |
| 262 ≡⟨⟩ | |
| 263 f | |
| 264 ∎ where | |
| 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 = |
|
170
721cf9d9f5e3
use functional extensionality in library
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
169
diff
changeset
|
270 extensionality 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 :: [] ) ) |
|
170
721cf9d9f5e3
use functional extensionality in library
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
169
diff
changeset
|
291 ≡⟨ extensionality {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 = Φ | |
| 311 fm-ε : NTrans B B ( ( FunctorF A B FreeMonoidUniveralMapping) ○ U) identityFunctor | |
| 312 fm-ε = nat-ε A B {U} {Generator} {eta} FreeMonoidUniveralMapping | |
| 343 | 313 -- TMap = λ a → solution (FObj U a) a (λ x → x ) ; |
| 314 -- isNTrans = record { | |
| 315 -- commute = commute1 | |
| 316 -- } | |
| 317 -- } where | |
| 318 -- commute1 : {a b : Obj B} {f : Hom B a b} → let open ≈-Reasoning B renaming (_o_ to _*_ ) in | |
| 319 -- ( FMap (identityFunctor {_} {_} {_} {B}) f * solution (FObj U a) a (λ x → x) ) ≈ | |
| 320 -- ( solution (FObj U b) b (λ x → x) * FMap (FunctorF A B FreeMonoidUniveralMapping ○ U) f ) | |
| 321 -- commute1 {a} {b} {f} = let open ≡-Reasoning in begin | |
| 322 -- morph ((B ≈-Reasoning.o FMap identityFunctor f) (solution (FObj U a) a (λ x → x))) | |
| 323 -- ≡⟨ {!!} ⟩ | |
| 324 -- morph ((B ≈-Reasoning.o solution (FObj U b) b (λ x → x)) (FMap (FunctorF A B FreeMonoidUniveralMapping ○ U) f)) | |
| 325 -- ∎ | |
| 326 | |
| 327 | |
| 328 fm-η : NTrans A A identityFunctor ( U ○ ( FunctorF A B FreeMonoidUniveralMapping) ) | |
| 329 fm-η = record { | |
| 330 TMap = λ a → λ (x : a) → x :: [] ; | |
| 331 isNTrans = record { | |
| 332 commute = commute1 | |
| 333 } | |
| 334 } where | |
| 335 commute1 : {a b : Obj A} {f : Hom A a b} → let open ≈-Reasoning A renaming (_o_ to _*_ ) in | |
| 336 (( FMap (U ○ FunctorF A B FreeMonoidUniveralMapping) f ) * (λ x → x :: []) ) ≈ ( (λ x → x :: []) * (λ z → FMap (identityFunctor {_} {_} {_} {A}) f z ) ) | |
| 337 commute1 {a} {b} {f} = refl -- λ (x : a ) → f x :: [] | |
| 338 | |
|
157
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
339 |
|
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
340 open Adjunction |
|
167
c3863043c4a3
Free Monoid and Universal mapping problem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
166
diff
changeset
|
341 |
|
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
342 -- A = Sets {c} |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
343 -- B = Monoids |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
344 -- U underline funcotr |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
345 -- F generator = x :: [] |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
346 -- Eta x :: [] |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
347 -- Epsiron morph = Φ |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
348 |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
349 adj = UMAdjunction A B U Generator eta FreeMonoidUniveralMapping |
|
167
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 |
|
c3863043c4a3
Free Monoid and Universal mapping problem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
166
diff
changeset
|
353 |