Mercurial > hg > Members > kono > Proof > category
annotate free-monoid.agda @ 162:18ab1be1ebb5
mapping done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 19 Aug 2013 12:34:08 +0900 |
| parents | ffeb33698173 |
| children | bc47179e3c9c |
| rev | line source |
|---|---|
| 155 | 1 -- {-# OPTIONS --universe-polymorphism #-} |
| 2 | |
| 162 | 3 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
| 4 | |
| 154 | 5 open import Category -- https://github.com/konn/category-agda |
| 6 open import Level | |
| 7 module free-monoid { c c₁ c₂ ℓ : Level } where | |
| 8 | |
| 9 open import Category.Sets | |
| 10 open import Category.Cat | |
| 11 open import HomReasoning | |
| 12 open import cat-utility | |
| 13 open import Relation.Binary.Core | |
| 14 open import Relation.Binary.PropositionalEquality | |
| 15 | |
| 162 | 16 -- from https://github.com/danr/Agda-projects/blob/master/Category-Theory/FreeMonoid.agda |
| 154 | 17 |
| 18 infixr 40 _::_ | |
| 156 | 19 data List (A : Set c ) : Set c where |
| 154 | 20 [] : List A |
| 21 _::_ : A -> List A -> List A | |
| 22 | |
| 23 | |
| 24 infixl 30 _++_ | |
| 156 | 25 _++_ : {A : Set c } -> List A -> List A -> List A |
| 154 | 26 [] ++ ys = ys |
| 27 (x :: xs) ++ ys = x :: (xs ++ ys) | |
| 28 | |
| 29 ≡-cong = Relation.Binary.PropositionalEquality.cong | |
| 30 | |
| 156 | 31 list-id-l : { A : Set c } -> { x : List A } -> [] ++ x ≡ x |
| 32 list-id-l {_} {_} = refl | |
| 33 list-id-r : { A : Set c } -> { x : List A } -> x ++ [] ≡ x | |
| 34 list-id-r {_} {[]} = refl | |
| 35 list-id-r {A} {x :: xs} = ≡-cong ( \y -> x :: y ) ( list-id-r {A} {xs} ) | |
| 36 list-assoc : {A : Set c} -> { xs ys zs : List A } -> | |
| 37 ( xs ++ ( ys ++ zs ) ) ≡ ( ( xs ++ ys ) ++ zs ) | |
| 38 list-assoc {_} {[]} {_} {_} = refl | |
| 39 list-assoc {A} {x :: xs} {ys} {zs} = ≡-cong ( \y -> x :: y ) | |
| 40 ( list-assoc {A} {xs} {ys} {zs} ) | |
| 41 list-o-resp-≈ : {A : Set c} -> {f g : List A } → {h i : List A } → | |
| 42 f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g) | |
| 43 list-o-resp-≈ {A} refl refl = refl | |
| 44 list-isEquivalence : {A : Set c} -> IsEquivalence {_} {_} {List A } _≡_ | |
| 45 list-isEquivalence {A} = -- this is the same function as A's equivalence but has different types | |
| 46 record { refl = refl | |
| 47 ; sym = sym | |
| 48 ; trans = trans | |
| 49 } | |
| 154 | 50 |
| 51 open import Algebra.FunctionProperties using (Op₁; Op₂) | |
| 156 | 52 open import Algebra.Structures |
| 53 open import Data.Product | |
| 154 | 54 |
| 55 | |
| 56 record ≡-Monoid : Set (suc c) where | |
| 57 infixl 7 _∙_ | |
| 58 field | |
| 59 Carrier : Set c | |
| 60 _∙_ : Op₂ Carrier | |
| 61 ε : Carrier | |
| 62 isMonoid : IsMonoid _≡_ _∙_ ε | |
| 63 | |
| 64 open ≡-Monoid | |
| 65 | |
| 66 record Monomorph ( a b : ≡-Monoid ) : Set (suc c) where | |
| 67 field | |
| 68 morph : Carrier a -> Carrier b | |
| 69 identity : morph (ε a) ≡ ε b | |
| 70 mdistr : ∀{x y} -> morph ( _∙_ a x y ) ≡ ( _∙_ b (morph x ) (morph y) ) | |
| 71 | |
| 72 open Monomorph | |
| 73 | |
| 155 | 74 _+_ : { a b c : ≡-Monoid } -> Monomorph b c -> Monomorph a b -> Monomorph a c |
| 75 _+_ {a} {b} {c} f g = record { | |
| 154 | 76 morph = \x -> morph f ( morph g x ) ; |
| 77 identity = identity1 ; | |
| 78 mdistr = mdistr1 | |
| 79 } where | |
| 80 identity1 : morph f ( morph g (ε a) ) ≡ ε c | |
| 81 -- morph f (ε b) = ε c , morph g (ε a) ) ≡ ε b | |
| 82 -- morph f morph g (ε a) ) ≡ morph f (ε b) = ε c | |
| 83 identity1 = trans ( ≡-cong (morph f ) ( identity g ) ) ( identity f ) | |
| 84 mdistr1 : ∀{x y} -> morph f ( morph g ( _∙_ a x y )) ≡ ( _∙_ c (morph f (morph g x )) (morph f (morph g y) ) ) | |
| 85 -- ∀{x y} -> morph f ( morph g ( _∙_ a x y )) ≡ morph f ( ( _∙_ c (morph g x )) (morph g y) ) | |
| 86 -- ∀{x y} -> morph f ( ( _∙_ c (morph g x )) (morph g y) ) ≡ ( _∙_ c (morph f (morph g x )) (morph f (morph g y) ) ) | |
| 87 mdistr1 = trans (≡-cong (morph f ) ( mdistr g) ) ( mdistr f ) | |
| 88 | |
| 155 | 89 M-id : { a : ≡-Monoid } -> Monomorph a a |
| 90 M-id = record { morph = \x -> x ; identity = refl ; mdistr = refl } | |
| 154 | 91 |
| 155 | 92 _==_ : { a b : ≡-Monoid } -> Monomorph a b -> Monomorph a b -> Set c |
| 93 _==_ f g = morph f ≡ morph g | |
| 94 | |
| 95 isMonoidCategory : IsCategory ≡-Monoid Monomorph _==_ _+_ (M-id) | |
| 96 isMonoidCategory = record { isEquivalence = isEquivalence1 | |
| 97 ; identityL = refl | |
| 98 ; identityR = refl | |
| 99 ; associative = refl | |
| 100 ; o-resp-≈ = \{a} {b} {c} {f} {g} {h} {i} -> o-resp-≈ {a} {b} {c} {f} {g} {h} {i} | |
| 101 } | |
| 102 where | |
| 103 o-resp-≈ : {a b c : ≡-Monoid } {f g : Monomorph a b } → {h i : Monomorph b c } → | |
| 104 f == g → h == i → (h + f) == (i + g) | |
| 105 o-resp-≈ {A} refl refl = refl | |
| 106 isEquivalence1 : { a b : ≡-Monoid } -> IsEquivalence {_} {_} {Monomorph a b} _==_ | |
| 107 isEquivalence1 = -- this is the same function as A's equivalence but has different types | |
| 108 record { refl = refl | |
| 109 ; sym = sym | |
| 110 ; trans = trans | |
| 111 } | |
| 112 MonoidCategory : Category _ _ _ | |
| 113 MonoidCategory = | |
| 114 record { Obj = ≡-Monoid | |
| 115 ; Hom = Monomorph | |
| 116 ; _o_ = _+_ | |
| 117 ; _≈_ = _==_ | |
| 118 ; Id = M-id | |
| 119 ; isCategory = isMonoidCategory | |
| 120 } | |
| 154 | 121 |
| 156 | 122 A = Sets {c} |
| 123 B = MonoidCategory | |
| 154 | 124 |
| 156 | 125 open Functor |
| 154 | 126 |
| 156 | 127 U : Functor B A |
| 128 U = record { | |
| 129 FObj = \m -> Carrier m ; | |
| 130 FMap = \f -> morph f ; | |
| 131 isFunctor = record { | |
| 132 ≈-cong = \x -> x | |
| 133 ; identity = refl | |
| 134 ; distr = refl | |
| 135 } | |
| 136 } | |
| 154 | 137 |
| 156 | 138 -- FObj |
| 159 | 139 list : (a : Set c) -> ≡-Monoid |
| 140 list a = record { | |
| 141 Carrier = List a | |
| 142 ; _∙_ = _++_ | |
| 143 ; ε = [] | |
| 144 ; isMonoid = record { | |
| 145 identity = ( ( \x -> list-id-l {a} ) , ( \x -> list-id-r {a} ) ) ; | |
| 146 isSemigroup = record { | |
| 147 assoc = \x -> \y -> \z -> sym ( list-assoc {a} {x} {y} {z} ) | |
| 148 ; isEquivalence = list-isEquivalence | |
| 149 ; ∙-cong = \x -> \y -> list-o-resp-≈ y x | |
| 150 } | |
| 151 } | |
| 152 } | |
| 153 | |
| 156 | 154 Generator : Obj A -> Obj B |
| 155 Generator s = list s | |
| 156 | |
|
157
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
157 -- solution |
|
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
158 |
| 159 | 159 open UniversalMapping |
| 158 | 160 |
| 161 | 161 Φ : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } → List a -> Carrier b |
| 162 Φ {a} {b} {f} [] = ε b | |
| 163 Φ {a} {b} {f} ( x :: xs ) = _∙_ b ( f x ) (Φ {a} {b} {f} xs ) | |
| 164 | |
| 165 solution : (a : Obj A ) (b : Obj B) ( f : Hom A a (FObj U b) ) → Hom B (Generator a ) b | |
| 166 solution a b f = record { | |
| 167 morph = \(l : List a) -> Φ l ; | |
| 168 identity = refl ; | |
| 162 | 169 mdistr = \{x y} -> mdistr1 x y |
| 161 | 170 } where |
| 162 | 171 _*_ : Carrier b -> Carrier b -> Carrier b |
| 172 _*_ f g = _∙_ b f g | |
| 173 mdistr1 : (x y : Carrier (Generator a)) → Φ ((Generator a ∙ x) y) ≡ (b ∙ Φ x) (Φ y) | |
| 174 mdistr1 [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ y)) | |
| 175 mdistr1 (x :: xs) y = let open ≡-Reasoning in | |
| 161 | 176 sym ( begin |
| 162 | 177 (Φ {a} {b} {f} (x :: xs)) * (Φ {a} {b} {f} y) |
| 161 | 178 ≡⟨⟩ |
| 162 | 179 ((f x) * (Φ {a} {b} {f} xs)) * (Φ {a} {b} {f} y) |
| 161 | 180 ≡⟨ ( IsMonoid.assoc ( isMonoid b )) _ _ _ ⟩ |
| 162 | 181 (f x) * ( (Φ {a} {b} {f} xs) * (Φ {a} {b} {f} y) ) |
| 182 ≡⟨ sym ( (IsMonoid.∙-cong (isMonoid b)) refl (mdistr1 xs y )) ⟩ | |
| 183 (f x) * ( Φ {a} {b} {f} ( xs ++ y ) ) | |
| 161 | 184 ≡⟨⟩ |
| 185 Φ {a} {b} {f} ( x :: ( xs ++ y ) ) | |
| 186 ≡⟨⟩ | |
| 187 Φ {a} {b} {f} ( (x :: xs) ++ y ) | |
| 188 ≡⟨⟩ | |
| 189 Φ {a} {b} {f} ((Generator a ∙ x :: xs) y) | |
| 190 ∎ ) | |
| 191 | |
| 162 | 192 eta : (a : Obj A) → Hom A a ( FObj U (Generator a) ) |
| 193 eta a = \( x : a ) -> x :: [] | |
| 194 | |
| 195 -- Functional Extensionarity Axiom (We cannot prove this in Agda / Coq, just assumming ) | |
| 196 postulate Extensionarity : { a b : Obj A } {f g : Hom A a b } → (∀ {x} → (f x ≡ g x)) → ( f ≡ g ) | |
| 197 | |
| 159 | 198 FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta |
| 162 | 199 FreeMonoidUniveralMapping = |
|
157
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
200 record { |
| 160 | 201 _* = \{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
|
202 isUniversalMapping = record { |
| 159 | 203 universalMapping = \{a b f} -> universalMapping {a} {b} {f} ; |
| 160 | 204 uniquness = \{a b f} -> uniquness {a} {b} {f} |
|
157
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
205 } |
| 159 | 206 } where |
| 160 | 207 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 | 208 universalMapping {a} {b} {f} = let open ≡-Reasoning in |
| 209 begin | |
| 160 | 210 FMap U ( solution a b f ) o eta a |
| 161 | 211 ≡⟨⟩ |
| 162 | 212 ( λ (x : a ) → Φ {a} {b} {f} (eta a x) ) |
| 213 ≡⟨⟩ | |
| 214 ( λ (x : a ) → Φ {a} {b} {f} ( x :: [] ) ) | |
| 215 ≡⟨⟩ | |
| 216 ( λ (x : a ) → _∙_ b ( f x ) (Φ {a} {b} {f} [] ) ) | |
| 217 ≡⟨⟩ | |
| 218 ( λ (x : a ) → _∙_ b ( f x ) ( ε b ) ) | |
| 219 ≡⟨ ≡-cong ( \ g -> ( ( λ (x : a ) → g x ) )) (Extensionarity lemma-ext1) ⟩ | |
| 220 ( λ (x : a ) → f x ) | |
| 221 ≡⟨⟩ | |
| 222 f | |
| 223 ∎ where | |
| 224 lemma-ext1 : ∀{ x : a } -> _∙_ b ( f x ) ( ε b ) ≡ f x | |
| 225 lemma-ext1 {x} = ( proj₂ ( IsMonoid.identity ( isMonoid b) ) ) (f x) | |
| 159 | 226 uniquness : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } → |
| 160 | 227 { g : Hom B (Generator a) b } → (FMap U g) o (eta a ) ≡ f → B [ solution a b f ≈ g ] |
| 159 | 228 uniquness = {!!} |
|
157
34a152235ddd
solution of universal mapping for free monoid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
229 |