Mercurial > hg > Members > kono > Proof > category
annotate free-monoid.agda @ 254:45b81fcb8a64
equalizer fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 14 Sep 2013 10:04:18 +0900 |
| parents | 58ee98bbb333 |
| children | 33bc037319fa |
| 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 | |
| 15 open import Relation.Binary.PropositionalEquality | |
| 178 | 16 open import universal-mapping |
| 154 | 17 |
| 162 | 18 -- from https://github.com/danr/Agda-projects/blob/master/Category-Theory/FreeMonoid.agda |
| 154 | 19 |
| 20 infixr 40 _::_ | |
| 156 | 21 data List (A : Set c ) : Set c where |
| 154 | 22 [] : List A |
| 254 | 23 _::_ : A → List A → List A |
| 154 | 24 |
| 25 | |
| 26 infixl 30 _++_ | |
| 254 | 27 _++_ : {A : Set c } → List A → List A → List A |
| 154 | 28 [] ++ ys = ys |
| 29 (x :: xs) ++ ys = x :: (xs ++ ys) | |
| 30 | |
| 31 ≡-cong = Relation.Binary.PropositionalEquality.cong | |
| 32 | |
| 254 | 33 list-id-l : { A : Set c } → { x : List A } → [] ++ x ≡ x |
| 156 | 34 list-id-l {_} {_} = refl |
| 254 | 35 list-id-r : { A : Set c } → { x : List A } → x ++ [] ≡ x |
| 156 | 36 list-id-r {_} {[]} = refl |
| 254 | 37 list-id-r {A} {x :: xs} = ≡-cong ( λ y → x :: y ) ( list-id-r {A} {xs} ) |
| 38 list-assoc : {A : Set c} → { xs ys zs : List A } → | |
| 156 | 39 ( xs ++ ( ys ++ zs ) ) ≡ ( ( xs ++ ys ) ++ zs ) |
| 40 list-assoc {_} {[]} {_} {_} = refl | |
| 254 | 41 list-assoc {A} {x :: xs} {ys} {zs} = ≡-cong ( λ y → x :: y ) |
| 156 | 42 ( list-assoc {A} {xs} {ys} {zs} ) |
| 254 | 43 list-o-resp-≈ : {A : Set c} → {f g : List A } → {h i : List A } → |
| 156 | 44 f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g) |
| 45 list-o-resp-≈ {A} refl refl = refl | |
| 254 | 46 list-isEquivalence : {A : Set c} → IsEquivalence {_} {_} {List A } _≡_ |
| 156 | 47 list-isEquivalence {A} = -- this is the same function as A's equivalence but has different types |
| 48 record { refl = refl | |
| 49 ; sym = sym | |
| 50 ; trans = trans | |
| 51 } | |
| 154 | 52 |
| 53 open import Algebra.FunctionProperties using (Op₁; Op₂) | |
| 156 | 54 open import Algebra.Structures |
| 55 open import Data.Product | |
| 154 | 56 |
| 57 | |
| 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 | |
| 68 record Monomorph ( a b : ≡-Monoid ) : Set (suc c) where | |
| 69 field | |
| 254 | 70 morph : Carrier a → Carrier b |
| 154 | 71 identity : morph (ε a) ≡ ε b |
| 254 | 72 homo : ∀{x y} → morph ( _∙_ a x y ) ≡ ( _∙_ b (morph x ) (morph y) ) |
| 154 | 73 |
| 74 open Monomorph | |
| 75 | |
| 254 | 76 _+_ : { a b c : ≡-Monoid } → Monomorph b c → Monomorph a b → Monomorph a c |
| 155 | 77 _+_ {a} {b} {c} f g = record { |
| 254 | 78 morph = λ x → morph f ( morph g x ) ; |
| 154 | 79 identity = identity1 ; |
| 168 | 80 homo = homo1 |
| 154 | 81 } where |
| 82 identity1 : morph f ( morph g (ε a) ) ≡ ε c | |
| 83 -- morph f (ε b) = ε c , morph g (ε a) ) ≡ ε b | |
| 84 -- morph f morph g (ε a) ) ≡ morph f (ε b) = ε c | |
| 85 identity1 = trans ( ≡-cong (morph f ) ( identity g ) ) ( identity f ) | |
| 254 | 86 homo1 : ∀{x y} → morph f ( morph g ( _∙_ a x y )) ≡ ( _∙_ c (morph f (morph g x )) (morph f (morph g y) ) ) |
| 87 -- ∀{x y} → morph f ( morph g ( _∙_ a x y )) ≡ morph f ( ( _∙_ c (morph g x )) (morph g y) ) | |
| 88 -- ∀{x y} → morph f ( ( _∙_ c (morph g x )) (morph g y) ) | |
| 168 | 89 -- ≡ ( _∙_ c (morph f (morph g x )) (morph f (morph g y) ) ) |
| 90 homo1 = trans (≡-cong (morph f ) ( homo g) ) ( homo f ) | |
| 154 | 91 |
| 254 | 92 M-id : { a : ≡-Monoid } → Monomorph a a |
| 93 M-id = record { morph = λ x → x ; identity = refl ; homo = refl } | |
| 154 | 94 |
| 254 | 95 _==_ : { a b : ≡-Monoid } → Monomorph a b → Monomorph a b → Set c |
| 155 | 96 _==_ f g = morph f ≡ morph g |
| 97 | |
| 168 | 98 isMonoids : IsCategory ≡-Monoid Monomorph _==_ _+_ (M-id) |
| 99 isMonoids = record { isEquivalence = isEquivalence1 | |
| 155 | 100 ; identityL = refl |
| 101 ; identityR = refl | |
| 102 ; associative = refl | |
| 254 | 103 ; o-resp-≈ = λ {a} {b} {c} {f} {g} {h} {i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} |
| 155 | 104 } |
| 105 where | |
| 106 o-resp-≈ : {a b c : ≡-Monoid } {f g : Monomorph a b } → {h i : Monomorph b c } → | |
| 107 f == g → h == i → (h + f) == (i + g) | |
| 108 o-resp-≈ {A} refl refl = refl | |
| 254 | 109 isEquivalence1 : { a b : ≡-Monoid } → IsEquivalence {_} {_} {Monomorph a b} _==_ |
| 155 | 110 isEquivalence1 = -- this is the same function as A's equivalence but has different types |
| 111 record { refl = refl | |
| 112 ; sym = sym | |
| 113 ; trans = trans | |
| 114 } | |
| 168 | 115 Monoids : Category _ _ _ |
| 116 Monoids = | |
| 155 | 117 record { Obj = ≡-Monoid |
| 118 ; Hom = Monomorph | |
| 119 ; _o_ = _+_ | |
| 120 ; _≈_ = _==_ | |
| 121 ; Id = M-id | |
| 168 | 122 ; isCategory = isMonoids |
| 155 | 123 } |
| 154 | 124 |
| 156 | 125 A = Sets {c} |
| 168 | 126 B = Monoids |
| 154 | 127 |
| 156 | 128 open Functor |
| 154 | 129 |
| 156 | 130 U : Functor B A |
| 131 U = record { | |
| 254 | 132 FObj = λ m → Carrier m ; |
| 133 FMap = λ f → morph f ; | |
| 156 | 134 isFunctor = record { |
| 254 | 135 ≈-cong = λ x → x |
| 156 | 136 ; identity = refl |
| 137 ; distr = refl | |
| 138 } | |
| 139 } | |
| 154 | 140 |
| 156 | 141 -- FObj |
| 254 | 142 list : (a : Set c) → ≡-Monoid |
| 159 | 143 list a = record { |
| 144 Carrier = List a | |
| 145 ; _∙_ = _++_ | |
| 146 ; ε = [] | |
| 147 ; isMonoid = record { | |
| 254 | 148 identity = ( ( λ x → list-id-l {a} ) , ( λ x → list-id-r {a} ) ) ; |
| 159 | 149 isSemigroup = record { |
| 254 | 150 assoc = λ x → λ y → λ z → sym ( list-assoc {a} {x} {y} {z} ) |
| 159 | 151 ; isEquivalence = list-isEquivalence |
| 254 | 152 ; ∙-cong = λ x → λ y → list-o-resp-≈ y x |
| 159 | 153 } |
| 154 } | |
| 155 } | |
| 156 | |
| 254 | 157 Generator : Obj A → Obj B |
| 156 | 158 Generator s = list s |
| 159 | |
|
157
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
160 -- solution |
|
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
161 |
| 159 | 162 open UniversalMapping |
| 158 | 163 |
|
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
164 -- [a,b,c] → f(a) ∙ f(b) ∙ f(c) |
| 254 | 165 Φ : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } → List a → Carrier b |
| 161 | 166 Φ {a} {b} {f} [] = ε b |
| 167 Φ {a} {b} {f} ( x :: xs ) = _∙_ b ( f x ) (Φ {a} {b} {f} xs ) | |
| 168 | |
| 169 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 { | |
| 254 | 171 morph = λ (l : List a) → Φ l ; |
| 161 | 172 identity = refl ; |
| 254 | 173 homo = λ {x y} → homo1 x y |
| 161 | 174 } where |
| 254 | 175 _*_ : Carrier b → Carrier b → Carrier b |
| 162 | 176 _*_ f g = _∙_ b f g |
| 168 | 177 homo1 : (x y : Carrier (Generator a)) → Φ ((Generator a ∙ x) y) ≡ (b ∙ Φ x) (Φ y) |
| 178 homo1 [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ y)) | |
| 179 homo1 (x :: xs) y = let open ≡-Reasoning in | |
| 161 | 180 sym ( begin |
| 162 | 181 (Φ {a} {b} {f} (x :: xs)) * (Φ {a} {b} {f} y) |
| 161 | 182 ≡⟨⟩ |
| 162 | 183 ((f x) * (Φ {a} {b} {f} xs)) * (Φ {a} {b} {f} y) |
| 161 | 184 ≡⟨ ( IsMonoid.assoc ( isMonoid b )) _ _ _ ⟩ |
| 162 | 185 (f x) * ( (Φ {a} {b} {f} xs) * (Φ {a} {b} {f} y) ) |
| 168 | 186 ≡⟨ sym ( (IsMonoid.∙-cong (isMonoid b)) refl (homo1 xs y )) ⟩ |
| 162 | 187 (f x) * ( Φ {a} {b} {f} ( xs ++ y ) ) |
| 161 | 188 ≡⟨⟩ |
| 189 Φ {a} {b} {f} ( x :: ( xs ++ y ) ) | |
| 190 ≡⟨⟩ | |
| 191 Φ {a} {b} {f} ( (x :: xs) ++ y ) | |
| 192 ≡⟨⟩ | |
| 193 Φ {a} {b} {f} ((Generator a ∙ x :: xs) y) | |
| 194 ∎ ) | |
| 195 | |
| 162 | 196 eta : (a : Obj A) → Hom A a ( FObj U (Generator a) ) |
| 254 | 197 eta a = λ ( x : a ) → x :: [] |
| 162 | 198 |
| 168 | 199 -- Functional Extensionality Axiom (We cannot prove this in Agda / Coq, just assumming ) |
|
169
44bf6e78f891
builtin extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
168
diff
changeset
|
200 -- postulate extensionality : { a b : Obj A } {f g : Hom A a b } → (∀ {x} → (f x ≡ g x)) → ( f ≡ g ) |
|
170
721cf9d9f5e3
use functional extensionality in library
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
169
diff
changeset
|
201 postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c |
| 162 | 202 |
| 159 | 203 FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta |
| 162 | 204 FreeMonoidUniveralMapping = |
|
157
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
205 record { |
| 254 | 206 _* = λ {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
|
207 isUniversalMapping = record { |
| 254 | 208 universalMapping = λ {a b f} → universalMapping {a} {b} {f} ; |
| 209 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
|
210 } |
| 159 | 211 } where |
| 160 | 212 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 | 213 universalMapping {a} {b} {f} = let open ≡-Reasoning in |
| 214 begin | |
| 160 | 215 FMap U ( solution a b f ) o eta a |
| 161 | 216 ≡⟨⟩ |
| 162 | 217 ( λ (x : a ) → Φ {a} {b} {f} (eta a x) ) |
| 218 ≡⟨⟩ | |
| 219 ( λ (x : a ) → Φ {a} {b} {f} ( x :: [] ) ) | |
| 220 ≡⟨⟩ | |
| 221 ( λ (x : a ) → _∙_ b ( f x ) (Φ {a} {b} {f} [] ) ) | |
| 222 ≡⟨⟩ | |
| 223 ( λ (x : a ) → _∙_ b ( f x ) ( ε b ) ) | |
| 254 | 224 ≡⟨ ≡-cong ( λ g → ( ( λ (x : a ) → g x ) )) (extensionality {a} lemma-ext1) ⟩ |
| 162 | 225 ( λ (x : a ) → f x ) |
| 226 ≡⟨⟩ | |
| 227 f | |
| 228 ∎ where | |
| 254 | 229 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
|
230 lemma-ext1 x = ( proj₂ ( IsMonoid.identity ( isMonoid b) ) ) (f x) |
| 159 | 231 uniquness : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } → |
| 160 | 232 { 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
|
233 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
|
234 extensionality lemma-ext2 where |
| 254 | 235 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
|
236 -- (morph ( solution a b f)) [] ≡ (morph g) [] ) |
|
169
44bf6e78f891
builtin extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
168
diff
changeset
|
237 lemma-ext2 [] = let open ≡-Reasoning in |
| 164 | 238 begin |
| 239 (morph ( solution a b f)) [] | |
| 240 ≡⟨ identity ( solution a b f) ⟩ | |
| 241 ε b | |
| 242 ≡⟨ sym ( identity g ) ⟩ | |
| 243 (morph g) [] | |
| 244 ∎ | |
|
169
44bf6e78f891
builtin extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
168
diff
changeset
|
245 lemma-ext2 (x :: xs) = let open ≡-Reasoning in |
| 164 | 246 begin |
| 247 (morph ( solution a b f)) ( x :: xs ) | |
| 168 | 248 ≡⟨ homo ( solution a b f) {x :: []} {xs} ⟩ |
| 164 | 249 _∙_ b ((morph ( solution a b f)) ( x :: []) ) ((morph ( solution a b f)) xs ) |
| 254 | 250 ≡⟨ ≡-cong ( λ k → (_∙_ b ((morph ( solution a b f)) ( x :: []) ) k )) (lemma-ext2 xs ) ⟩ |
| 164 | 251 _∙_ b ((morph ( solution a b f)) ( x :: []) ) ((morph g) ( xs )) |
| 254 | 252 ≡⟨ ≡-cong ( λ k → ( _∙_ b ( k x ) ((morph g) ( xs )) )) ( |
| 164 | 253 begin |
| 254 | 254 ( λ 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
|
255 ≡⟨ extensionality {a} lemma-ext3 ⟩ |
| 254 | 256 ( λ x → (morph g) ( x :: [] ) ) |
| 164 | 257 ∎ |
| 258 ) ⟩ | |
| 259 _∙_ b ((morph g) ( x :: [] )) ((morph g) ( xs )) | |
| 168 | 260 ≡⟨ sym ( homo g ) ⟩ |
| 164 | 261 (morph g) ( x :: xs ) |
| 262 ∎ where | |
| 254 | 263 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
|
264 lemma-ext3 x = let open ≡-Reasoning in |
| 166 | 265 begin |
| 266 (morph ( solution a b f)) (x :: []) | |
| 267 ≡⟨ ( proj₂ ( IsMonoid.identity ( isMonoid b) )(f x) ) ⟩ | |
| 268 f x | |
| 254 | 269 ≡⟨ sym ( ≡-cong (λ f → f x ) eq ) ⟩ |
| 166 | 270 (morph g) ( x :: [] ) |
| 271 ∎ | |
| 272 | |
| 178 | 273 open NTrans |
| 274 -- fm-ε b = Φ | |
| 275 fm-ε : NTrans B B ( ( FunctorF A B FreeMonoidUniveralMapping) ○ U) identityFunctor | |
| 276 fm-ε = nat-ε A B {U} {Generator} {eta} FreeMonoidUniveralMapping | |
| 277 -- TMap fm-ε | |
|
157
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
278 |
|
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
279 open Adjunction |
|
167
c3863043c4a3
Free Monoid and Universal mapping problem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
166
diff
changeset
|
280 |
|
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
281 -- A = Sets {c} |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
282 -- B = Monoids |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
283 -- U underline funcotr |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
284 -- F generator = x :: [] |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
285 -- Eta x :: [] |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
286 -- Epsiron morph = Φ |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
287 |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
178
diff
changeset
|
288 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
|
289 |
|
c3863043c4a3
Free Monoid and Universal mapping problem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
166
diff
changeset
|
290 |
|
c3863043c4a3
Free Monoid and Universal mapping problem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
166
diff
changeset
|
291 |
|
c3863043c4a3
Free Monoid and Universal mapping problem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
166
diff
changeset
|
292 |