Mercurial > hg > Members > kono > Proof > category
annotate free-monoid.agda @ 185:173d078ee443
Yoneda join
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 28 Aug 2013 21:51:59 +0900 |
| parents | 6626a7cd9129 |
| children | 58ee98bbb333 |
| 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 |
| 23 _::_ : A -> List A -> List A | |
| 24 | |
| 25 | |
| 26 infixl 30 _++_ | |
| 156 | 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 | |
| 156 | 33 list-id-l : { A : Set c } -> { x : List A } -> [] ++ x ≡ x |
| 34 list-id-l {_} {_} = refl | |
| 35 list-id-r : { A : Set c } -> { x : List A } -> x ++ [] ≡ x | |
| 36 list-id-r {_} {[]} = refl | |
| 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 } -> | |
| 39 ( xs ++ ( ys ++ zs ) ) ≡ ( ( xs ++ ys ) ++ zs ) | |
| 40 list-assoc {_} {[]} {_} {_} = refl | |
| 41 list-assoc {A} {x :: xs} {ys} {zs} = ≡-cong ( \y -> x :: y ) | |
| 42 ( list-assoc {A} {xs} {ys} {zs} ) | |
| 43 list-o-resp-≈ : {A : Set c} -> {f g : List A } → {h i : List A } → | |
| 44 f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g) | |
| 45 list-o-resp-≈ {A} refl refl = refl | |
| 46 list-isEquivalence : {A : Set c} -> IsEquivalence {_} {_} {List A } _≡_ | |
| 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 | |
| 70 morph : Carrier a -> Carrier b | |
| 71 identity : morph (ε a) ≡ ε b | |
| 168 | 72 homo : ∀{x y} -> morph ( _∙_ a x y ) ≡ ( _∙_ b (morph x ) (morph y) ) |
| 154 | 73 |
| 74 open Monomorph | |
| 75 | |
| 155 | 76 _+_ : { a b c : ≡-Monoid } -> Monomorph b c -> Monomorph a b -> Monomorph a c |
| 77 _+_ {a} {b} {c} f g = record { | |
| 154 | 78 morph = \x -> morph f ( morph g x ) ; |
| 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 ) | |
| 168 | 86 homo1 : ∀{x y} -> morph f ( morph g ( _∙_ a x y )) ≡ ( _∙_ c (morph f (morph g x )) (morph f (morph g y) ) ) |
| 154 | 87 -- ∀{x y} -> morph f ( morph g ( _∙_ a x y )) ≡ morph f ( ( _∙_ c (morph g x )) (morph g y) ) |
| 168 | 88 -- ∀{x y} -> morph f ( ( _∙_ c (morph g x )) (morph g y) ) |
| 89 -- ≡ ( _∙_ c (morph f (morph g x )) (morph f (morph g y) ) ) | |
| 90 homo1 = trans (≡-cong (morph f ) ( homo g) ) ( homo f ) | |
| 154 | 91 |
| 155 | 92 M-id : { a : ≡-Monoid } -> Monomorph a a |
| 168 | 93 M-id = record { morph = \x -> x ; identity = refl ; homo = refl } |
| 154 | 94 |
| 155 | 95 _==_ : { a b : ≡-Monoid } -> Monomorph a b -> Monomorph a b -> Set c |
| 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 | |
| 103 ; o-resp-≈ = \{a} {b} {c} {f} {g} {h} {i} -> o-resp-≈ {a} {b} {c} {f} {g} {h} {i} | |
| 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 | |
| 109 isEquivalence1 : { a b : ≡-Monoid } -> IsEquivalence {_} {_} {Monomorph a b} _==_ | |
| 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 { | |
| 132 FObj = \m -> Carrier m ; | |
| 133 FMap = \f -> morph f ; | |
| 134 isFunctor = record { | |
| 135 ≈-cong = \x -> x | |
| 136 ; identity = refl | |
| 137 ; distr = refl | |
| 138 } | |
| 139 } | |
| 154 | 140 |
| 156 | 141 -- FObj |
| 159 | 142 list : (a : Set c) -> ≡-Monoid |
| 143 list a = record { | |
| 144 Carrier = List a | |
| 145 ; _∙_ = _++_ | |
| 146 ; ε = [] | |
| 147 ; isMonoid = record { | |
| 148 identity = ( ( \x -> list-id-l {a} ) , ( \x -> list-id-r {a} ) ) ; | |
| 149 isSemigroup = record { | |
| 150 assoc = \x -> \y -> \z -> sym ( list-assoc {a} {x} {y} {z} ) | |
| 151 ; isEquivalence = list-isEquivalence | |
| 152 ; ∙-cong = \x -> \y -> list-o-resp-≈ y x | |
| 153 } | |
| 154 } | |
| 155 } | |
| 156 | |
| 156 | 157 Generator : Obj A -> Obj B |
| 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 |
| 161 | 164 Φ : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } → List a -> Carrier b |
| 165 Φ {a} {b} {f} [] = ε b | |
| 166 Φ {a} {b} {f} ( x :: xs ) = _∙_ b ( f x ) (Φ {a} {b} {f} xs ) | |
| 167 | |
| 168 solution : (a : Obj A ) (b : Obj B) ( f : Hom A a (FObj U b) ) → Hom B (Generator a ) b | |
| 169 solution a b f = record { | |
| 170 morph = \(l : List a) -> Φ l ; | |
| 171 identity = refl ; | |
| 168 | 172 homo = \{x y} -> homo1 x y |
| 161 | 173 } where |
| 162 | 174 _*_ : Carrier b -> Carrier b -> Carrier b |
| 175 _*_ f g = _∙_ b f g | |
| 168 | 176 homo1 : (x y : Carrier (Generator a)) → Φ ((Generator a ∙ x) y) ≡ (b ∙ Φ x) (Φ y) |
| 177 homo1 [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ y)) | |
| 178 homo1 (x :: xs) y = let open ≡-Reasoning in | |
| 161 | 179 sym ( begin |
| 162 | 180 (Φ {a} {b} {f} (x :: xs)) * (Φ {a} {b} {f} y) |
| 161 | 181 ≡⟨⟩ |
| 162 | 182 ((f x) * (Φ {a} {b} {f} xs)) * (Φ {a} {b} {f} y) |
| 161 | 183 ≡⟨ ( IsMonoid.assoc ( isMonoid b )) _ _ _ ⟩ |
| 162 | 184 (f x) * ( (Φ {a} {b} {f} xs) * (Φ {a} {b} {f} y) ) |
| 168 | 185 ≡⟨ sym ( (IsMonoid.∙-cong (isMonoid b)) refl (homo1 xs y )) ⟩ |
| 162 | 186 (f x) * ( Φ {a} {b} {f} ( xs ++ y ) ) |
| 161 | 187 ≡⟨⟩ |
| 188 Φ {a} {b} {f} ( x :: ( xs ++ y ) ) | |
| 189 ≡⟨⟩ | |
| 190 Φ {a} {b} {f} ( (x :: xs) ++ y ) | |
| 191 ≡⟨⟩ | |
| 192 Φ {a} {b} {f} ((Generator a ∙ x :: xs) y) | |
| 193 ∎ ) | |
| 194 | |
| 162 | 195 eta : (a : Obj A) → Hom A a ( FObj U (Generator a) ) |
| 196 eta a = \( x : a ) -> x :: [] | |
| 197 | |
| 168 | 198 -- 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
|
199 -- 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
|
200 postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c |
| 162 | 201 |
| 159 | 202 FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta |
| 162 | 203 FreeMonoidUniveralMapping = |
|
157
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
204 record { |
| 160 | 205 _* = \{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
|
206 isUniversalMapping = record { |
| 159 | 207 universalMapping = \{a b f} -> universalMapping {a} {b} {f} ; |
|
167
c3863043c4a3
Free Monoid and Universal mapping problem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
166
diff
changeset
|
208 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
|
209 } |
| 159 | 210 } where |
| 160 | 211 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 | 212 universalMapping {a} {b} {f} = let open ≡-Reasoning in |
| 213 begin | |
| 160 | 214 FMap U ( solution a b f ) o eta a |
| 161 | 215 ≡⟨⟩ |
| 162 | 216 ( λ (x : a ) → Φ {a} {b} {f} (eta a x) ) |
| 217 ≡⟨⟩ | |
| 218 ( λ (x : a ) → Φ {a} {b} {f} ( x :: [] ) ) | |
| 219 ≡⟨⟩ | |
| 220 ( λ (x : a ) → _∙_ b ( f x ) (Φ {a} {b} {f} [] ) ) | |
| 221 ≡⟨⟩ | |
| 222 ( λ (x : a ) → _∙_ b ( f x ) ( ε b ) ) | |
|
170
721cf9d9f5e3
use functional extensionality in library
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
169
diff
changeset
|
223 ≡⟨ ≡-cong ( \ g -> ( ( λ (x : a ) → g x ) )) (extensionality {a} lemma-ext1) ⟩ |
| 162 | 224 ( λ (x : a ) → f x ) |
| 225 ≡⟨⟩ | |
| 226 f | |
| 227 ∎ where | |
|
169
44bf6e78f891
builtin extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
168
diff
changeset
|
228 lemma-ext1 : ∀( x : a ) -> _∙_ b ( f x ) ( ε b ) ≡ f x |
|
44bf6e78f891
builtin extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
168
diff
changeset
|
229 lemma-ext1 x = ( proj₂ ( IsMonoid.identity ( isMonoid b) ) ) (f x) |
| 159 | 230 uniquness : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } → |
| 160 | 231 { 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
|
232 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
|
233 extensionality lemma-ext2 where |
|
169
44bf6e78f891
builtin extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
168
diff
changeset
|
234 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
|
235 -- (morph ( solution a b f)) [] ≡ (morph g) [] ) |
|
169
44bf6e78f891
builtin extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
168
diff
changeset
|
236 lemma-ext2 [] = let open ≡-Reasoning in |
| 164 | 237 begin |
| 238 (morph ( solution a b f)) [] | |
| 239 ≡⟨ identity ( solution a b f) ⟩ | |
| 240 ε b | |
| 241 ≡⟨ sym ( identity g ) ⟩ | |
| 242 (morph g) [] | |
| 243 ∎ | |
|
169
44bf6e78f891
builtin extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
168
diff
changeset
|
244 lemma-ext2 (x :: xs) = let open ≡-Reasoning in |
| 164 | 245 begin |
| 246 (morph ( solution a b f)) ( x :: xs ) | |
| 168 | 247 ≡⟨ homo ( solution a b f) {x :: []} {xs} ⟩ |
| 164 | 248 _∙_ b ((morph ( solution a b f)) ( x :: []) ) ((morph ( solution a b f)) xs ) |
|
169
44bf6e78f891
builtin extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
168
diff
changeset
|
249 ≡⟨ ≡-cong ( \ k -> (_∙_ b ((morph ( solution a b f)) ( x :: []) ) k )) (lemma-ext2 xs ) ⟩ |
| 164 | 250 _∙_ b ((morph ( solution a b f)) ( x :: []) ) ((morph g) ( xs )) |
| 251 ≡⟨ ≡-cong ( \k -> ( _∙_ b ( k x ) ((morph g) ( xs )) )) ( | |
| 252 begin | |
| 253 ( \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
|
254 ≡⟨ extensionality {a} lemma-ext3 ⟩ |
| 164 | 255 ( \x -> (morph g) ( x :: [] ) ) |
| 256 ∎ | |
| 257 ) ⟩ | |
| 258 _∙_ b ((morph g) ( x :: [] )) ((morph g) ( xs )) | |
| 168 | 259 ≡⟨ sym ( homo g ) ⟩ |
| 164 | 260 (morph g) ( x :: xs ) |
| 261 ∎ where | |
|
169
44bf6e78f891
builtin extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
168
diff
changeset
|
262 lemma-ext3 : ∀( x : a ) -> (morph ( solution a b f)) (x :: []) ≡ (morph g) ( x :: [] ) |
|
44bf6e78f891
builtin extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
168
diff
changeset
|
263 lemma-ext3 x = let open ≡-Reasoning in |
| 166 | 264 begin |
| 265 (morph ( solution a b f)) (x :: []) | |
| 266 ≡⟨ ( proj₂ ( IsMonoid.identity ( isMonoid b) )(f x) ) ⟩ | |
| 267 f x | |
| 268 ≡⟨ sym ( ≡-cong (\f -> f x ) eq ) ⟩ | |
| 269 (morph g) ( x :: [] ) | |
| 270 ∎ | |
| 271 | |
| 178 | 272 open NTrans |
| 273 -- fm-ε b = Φ | |
| 274 fm-ε : NTrans B B ( ( FunctorF A B FreeMonoidUniveralMapping) ○ U) identityFunctor | |
| 275 fm-ε = nat-ε A B {U} {Generator} {eta} FreeMonoidUniveralMapping | |
| 276 -- TMap fm-ε | |
|
157
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
277 |
|
167
c3863043c4a3
Free Monoid and Universal mapping problem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
166
diff
changeset
|
278 adjoint = UMAdjunction A B U Generator eta FreeMonoidUniveralMapping |
|
c3863043c4a3
Free Monoid and Universal mapping problem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
166
diff
changeset
|
279 |
|
c3863043c4a3
Free Monoid and Universal mapping problem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
166
diff
changeset
|
280 |
|
c3863043c4a3
Free Monoid and Universal mapping problem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
166
diff
changeset
|
281 |
|
c3863043c4a3
Free Monoid and Universal mapping problem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
166
diff
changeset
|
282 |
|
c3863043c4a3
Free Monoid and Universal mapping problem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
166
diff
changeset
|
283 |