Mercurial > hg > Members > kono > Proof > category
annotate monoid-monad.agda @ 149:2f68a9e0167b
clean up
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 15 Aug 2013 12:04:50 +0900 |
parents | 6e80e1aaa8b9 |
children | 5dc6f3f43507 |
rev | line source |
---|---|
129 | 1 open import Category -- https://github.com/konn/category-agda |
130 | 2 open import Algebra |
129 | 3 open import Level |
149 | 4 open import Category.Sets |
5 module monoid-monad {c : Level} where | |
130 | 6 |
142 | 7 open import Algebra.Structures |
129 | 8 open import HomReasoning |
9 open import cat-utility | |
10 open import Category.Cat | |
138 | 11 open import Data.Product |
12 open import Relation.Binary.Core | |
13 open import Relation.Binary | |
131 | 14 |
146
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
15 -- open Monoid |
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
16 open import Algebra.FunctionProperties using (Op₁; Op₂) |
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
17 |
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
18 |
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
19 record ≡-Monoid c : Set (suc c) where |
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
20 infixl 7 _∙_ |
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
21 field |
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
22 Carrier : Set c |
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
23 _∙_ : Op₂ Carrier |
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
24 ε : Carrier |
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
25 isMonoid : IsMonoid _≡_ _∙_ ε |
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
26 open IsMonoid isMonoid public |
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
27 |
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
28 postulate Mono : ≡-Monoid c |
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
29 open ≡-Monoid |
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
30 |
149 | 31 A = Sets {c} |
138 | 32 |
139 | 33 -- T : A → (M x A) |
134 | 34 |
149 | 35 T : Functor A A |
138 | 36 T = record { |
149 | 37 FObj = λ a → (Carrier Mono) × a |
38 ; FMap = λ f → map ( λ x → x ) f | |
138 | 39 ; isFunctor = record { |
40 identity = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets )) | |
41 ; distr = (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets ))) | |
42 ; ≈-cong = cong1 | |
43 } | |
44 } where | |
139 | 45 cong1 : {ℓ′ : Level} → {a b : Set ℓ′} { f g : Hom (Sets {ℓ′}) a b} → |
146
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
46 Sets [ f ≈ g ] → Sets [ map (λ (x : Carrier Mono) → x) f ≈ map (λ (x : Carrier Mono) → x) g ] |
138 | 47 cong1 _≡_.refl = _≡_.refl |
129 | 48 |
144 | 49 open Functor |
50 | |
149 | 51 Lemma-MM1 : {a b : Obj A} {f : Hom A a b} → |
52 A [ A [ FMap T f o (λ x → ε Mono , x) ] ≈ | |
53 A [ (λ x → ε Mono , x) o f ] ] | |
54 Lemma-MM1 {a} {b} {f} = let open ≈-Reasoning A renaming ( _o_ to _*_ ) in | |
139 | 55 begin |
144 | 56 FMap T f o (λ x → ε Mono , x) |
139 | 57 ≈⟨⟩ |
58 (λ x → ε Mono , x) o f | |
59 ∎ | |
60 | |
61 -- a → (ε,a) | |
149 | 62 η : NTrans A A identityFunctor T |
139 | 63 η = record { |
149 | 64 TMap = λ a → λ(x : a) → ( ε Mono , x ) ; |
139 | 65 isNTrans = record { |
149 | 66 commute = Lemma-MM1 |
139 | 67 } |
68 } | |
69 | |
70 -- (m,(m',a)) → (m*m,a) | |
71 | |
149 | 72 muMap : (a : Obj A ) → FObj T ( FObj T a ) → Σ (Carrier Mono) (λ x → a ) |
139 | 73 muMap a ( m , ( m' , x ) ) = ( _∙_ Mono m m' , x ) |
74 | |
149 | 75 Lemma-MM2 : {a b : Obj A} {f : Hom A a b} → |
76 A [ A [ FMap T f o (λ x → muMap a x) ] ≈ | |
77 A [ (λ x → muMap b x) o FMap (T ○ T) f ] ] | |
78 Lemma-MM2 {a} {b} {f} = let open ≈-Reasoning A renaming ( _o_ to _*_ ) in | |
139 | 79 begin |
80 FMap T f o (λ x → muMap a x) | |
81 ≈⟨⟩ | |
82 (λ x → muMap b x) o FMap (T ○ T) f | |
83 ∎ | |
84 | |
149 | 85 μ : NTrans A A ( T ○ T ) T |
139 | 86 μ = record { |
149 | 87 TMap = λ a → λ x → muMap a x ; |
139 | 88 isNTrans = record { |
149 | 89 commute = λ{a} {b} {f} → Lemma-MM2 {a} {b} {f} |
139 | 90 } |
91 } | |
141 | 92 |
93 open NTrans | |
94 | |
144 | 95 Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b} {x : Σ A B } → (((proj₁ x) , proj₂ x ) ≡ x ) |
142 | 96 Lemma-MM33 = _≡_.refl |
97 | |
149 | 98 Lemma-MM34 : ∀{ x : Carrier Mono } → ( (Mono ∙ ε Mono) x ≡ x ) |
147 | 99 Lemma-MM34 {x} = (( proj₁ ( IsMonoid.identity ( isMonoid Mono )) ) x ) |
146
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
100 |
149 | 101 Lemma-MM35 : ∀{ x : Carrier Mono } → ((Mono ∙ x) (ε Mono)) ≡ x |
146
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
102 Lemma-MM35 {x} = ( proj₂ ( IsMonoid.identity ( isMonoid Mono )) ) x |
141 | 103 |
149 | 104 Lemma-MM36 : ∀{ x y z : Carrier Mono } → ((Mono ∙ (Mono ∙ x) y) z) ≡ (_∙_ Mono x (_∙_ Mono y z ) ) |
146
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
105 Lemma-MM36 {x} {y} {z} = ( IsMonoid.assoc ( isMonoid Mono )) x y z |
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
106 |
149 | 107 -- Functional Extensionarity (We cannot prove this in Agda / Coq, just assumming ) |
108 postulate Extensionarity : {f g : Carrier Mono → Carrier Mono } → (∀ {x} → (f x ≡ g x)) → ( f ≡ g ) | |
144 | 109 |
149 | 110 postulate Extensionarity3 : {f g : Carrier Mono → Carrier Mono → Carrier Mono → Carrier Mono } → |
111 (∀{x y z} → f x y z ≡ g x y z ) → ( f ≡ g ) | |
144 | 112 |
149 | 113 Lemma-MM9 : ( λ(x : Carrier Mono) → ( Mono ∙ ε Mono ) x ) ≡ ( λ(x : Carrier Mono) → x ) |
114 Lemma-MM9 = Extensionarity Lemma-MM34 | |
144 | 115 |
149 | 116 Lemma-MM10 : ( λ x → ((Mono ∙ x) (ε Mono))) ≡ ( λ x → x ) |
117 Lemma-MM10 = Extensionarity Lemma-MM35 | |
146
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
118 |
149 | 119 Lemma-MM11 : (λ x y z → ((Mono ∙ (Mono ∙ x) y) z)) ≡ (λ x y z → ( _∙_ Mono x (_∙_ Mono y z ) )) |
120 Lemma-MM11 = Extensionarity3 Lemma-MM36 | |
145 | 121 |
149 | 122 MonoidMonad : Monad A T η μ |
141 | 123 MonoidMonad = record { |
124 isMonad = record { | |
148
6e80e1aaa8b9
no yellow on monoid monad
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
147
diff
changeset
|
125 unity1 = Lemma-MM3 ; |
141 | 126 unity2 = Lemma-MM4 ; |
148
6e80e1aaa8b9
no yellow on monoid monad
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
147
diff
changeset
|
127 assoc = Lemma-MM5 |
141 | 128 } |
129 } where | |
147 | 130 Lemma-MM3 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] |
149 | 131 Lemma-MM3 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in |
141 | 132 begin |
133 TMap μ a o TMap η ( FObj T a ) | |
134 ≈⟨⟩ | |
135 ( λ x → ((Mono ∙ ε Mono) (proj₁ x) , proj₂ x )) | |
149 | 136 ≈⟨ cong ( λ f → ( λ x → ( ( f (proj₁ x) ) , proj₂ x ))) ( Lemma-MM9 ) ⟩ |
147 | 137 ( λ (x : FObj T a) → (proj₁ x) , proj₂ x ) |
144 | 138 ≈⟨⟩ |
141 | 139 ( λ x → x ) |
140 ≈⟨⟩ | |
141 Id {_} {_} {_} {A} (FObj T a) | |
142 ∎ | |
143 Lemma-MM4 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] | |
149 | 144 Lemma-MM4 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in |
144 | 145 begin |
146 TMap μ a o (FMap T (TMap η a )) | |
147 ≈⟨⟩ | |
148 ( λ x → (Mono ∙ proj₁ x) (ε Mono) , proj₂ x ) | |
149 | 149 ≈⟨ cong ( λ f → ( λ x → ( f (proj₁ x) ) , proj₂ x )) ( Lemma-MM10 ) ⟩ |
144 | 150 ( λ x → (proj₁ x) , proj₂ x ) |
151 ≈⟨⟩ | |
152 ( λ x → x ) | |
153 ≈⟨⟩ | |
154 Id {_} {_} {_} {A} (FObj T a) | |
155 ∎ | |
141 | 156 Lemma-MM5 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] |
149 | 157 Lemma-MM5 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in |
144 | 158 begin |
159 TMap μ a o TMap μ ( FObj T a ) | |
160 ≈⟨⟩ | |
161 ( λ x → (Mono ∙ (Mono ∙ proj₁ x) (proj₁ (proj₂ x))) (proj₁ (proj₂ (proj₂ x))) , proj₂ (proj₂ (proj₂ x))) | |
149 | 162 ≈⟨ cong ( λ f → ( λ x → |
146
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
163 (( f ( proj₁ x ) ((proj₁ (proj₂ x))) ((proj₁ (proj₂ (proj₂ x))) )) , proj₂ (proj₂ (proj₂ x)) ) |
945f26ed12d5
assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
145
diff
changeset
|
164 )) Lemma-MM11 ⟩ |
144 | 165 ( λ x → (Mono ∙ proj₁ x) ((Mono ∙ proj₁ (proj₂ x)) (proj₁ (proj₂ (proj₂ x)))) , proj₂ (proj₂ (proj₂ x))) |
166 ≈⟨⟩ | |
167 TMap μ a o FMap T (TMap μ a) | |
168 ∎ | |
141 | 169 |
170 | |
171 |