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