Mercurial > hg > Members > kono > Proof > category
annotate monoid-monad.agda @ 151:3bd5109c83f3
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 17 Aug 2013 20:59:31 +0900 |
| parents | 5dc6f3f43507 |
| children | 3249aaddc405 |
| 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 |
| 151 | 27 postulate M : ≡-Monoid c |
|
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
|
28 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
|
29 |
| 149 | 30 A = Sets {c} |
| 138 | 31 |
| 139 | 32 -- T : A → (M x A) |
| 134 | 33 |
| 149 | 34 T : Functor A A |
| 138 | 35 T = record { |
| 151 | 36 FObj = λ a → (Carrier M) × a |
| 149 | 37 ; FMap = λ f → map ( λ x → x ) f |
| 138 | 38 ; isFunctor = record { |
| 39 identity = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets )) | |
| 40 ; distr = (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets ))) | |
| 41 ; ≈-cong = cong1 | |
| 42 } | |
| 43 } where | |
| 139 | 44 cong1 : {ℓ′ : Level} → {a b : Set ℓ′} { f g : Hom (Sets {ℓ′}) a b} → |
| 151 | 45 Sets [ f ≈ g ] → Sets [ map (λ (x : Carrier M) → x) f ≈ map (λ (x : Carrier M) → x) g ] |
| 138 | 46 cong1 _≡_.refl = _≡_.refl |
| 129 | 47 |
| 144 | 48 open Functor |
| 49 | |
| 149 | 50 Lemma-MM1 : {a b : Obj A} {f : Hom A a b} → |
| 151 | 51 A [ A [ FMap T f o (λ x → ε M , x) ] ≈ |
| 52 A [ (λ x → ε M , x) o f ] ] | |
| 149 | 53 Lemma-MM1 {a} {b} {f} = let open ≈-Reasoning A renaming ( _o_ to _*_ ) in |
| 139 | 54 begin |
| 151 | 55 FMap T f o (λ x → ε M , x) |
| 139 | 56 ≈⟨⟩ |
| 151 | 57 (λ x → ε M , x) o f |
| 139 | 58 ∎ |
| 59 | |
| 150 | 60 -- η : a → (ε,a) |
| 149 | 61 η : NTrans A A identityFunctor T |
| 139 | 62 η = record { |
| 151 | 63 TMap = λ a → λ(x : a) → ( ε M , x ) ; |
| 139 | 64 isNTrans = record { |
| 149 | 65 commute = Lemma-MM1 |
| 139 | 66 } |
| 67 } | |
| 68 | |
| 150 | 69 -- μ : (m,(m',a)) → (m*m,a) |
| 139 | 70 |
| 151 | 71 muMap : (a : Obj A ) → FObj T ( FObj T a ) → Σ (Carrier M) (λ x → a ) |
| 72 muMap a ( m , ( m' , x ) ) = ( _∙_ M m m' , x ) | |
| 139 | 73 |
| 149 | 74 Lemma-MM2 : {a b : Obj A} {f : Hom A a b} → |
| 75 A [ A [ FMap T f o (λ x → muMap a x) ] ≈ | |
| 76 A [ (λ x → muMap b x) o FMap (T ○ T) f ] ] | |
| 77 Lemma-MM2 {a} {b} {f} = let open ≈-Reasoning A renaming ( _o_ to _*_ ) in | |
| 139 | 78 begin |
| 79 FMap T f o (λ x → muMap a x) | |
| 80 ≈⟨⟩ | |
| 81 (λ x → muMap b x) o FMap (T ○ T) f | |
| 82 ∎ | |
| 83 | |
| 149 | 84 μ : NTrans A A ( T ○ T ) T |
| 139 | 85 μ = record { |
| 149 | 86 TMap = λ a → λ x → muMap a x ; |
| 139 | 87 isNTrans = record { |
| 149 | 88 commute = λ{a} {b} {f} → Lemma-MM2 {a} {b} {f} |
| 139 | 89 } |
| 90 } | |
| 141 | 91 |
| 92 open NTrans | |
| 93 | |
| 144 | 94 Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b} {x : Σ A B } → (((proj₁ x) , proj₂ x ) ≡ x ) |
| 142 | 95 Lemma-MM33 = _≡_.refl |
| 96 | |
| 151 | 97 Lemma-MM34 : ∀{ x : Carrier M } → ( (M ∙ ε M) x ≡ x ) |
| 98 Lemma-MM34 {x} = (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) 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
|
99 |
| 151 | 100 Lemma-MM35 : ∀{ x : Carrier M } → ((M ∙ x) (ε M)) ≡ x |
| 101 Lemma-MM35 {x} = ( proj₂ ( IsMonoid.identity ( isMonoid M )) ) x | |
| 141 | 102 |
| 151 | 103 Lemma-MM36 : ∀{ x y z : Carrier M } → ((M ∙ (M ∙ x) y) z) ≡ (_∙_ M x (_∙_ M y z ) ) |
| 104 Lemma-MM36 {x} {y} {z} = ( IsMonoid.assoc ( isMonoid M )) x 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 |
| 150 | 106 -- Functional Extensionarity Axiom (We cannot prove this in Agda / Coq, just assumming ) |
| 151 | 107 postulate Extensionarity : {f g : Carrier M → Carrier M } → (∀ {x} → (f x ≡ g x)) → ( f ≡ g ) |
| 144 | 108 |
| 151 | 109 postulate Extensionarity3 : {f g : Carrier M → Carrier M → Carrier M → Carrier M } → |
| 149 | 110 (∀{x y z} → f x y z ≡ g x y z ) → ( f ≡ g ) |
| 144 | 111 |
| 151 | 112 Lemma-MM9 : ( λ(x : Carrier M) → ( M ∙ ε M ) x ) ≡ ( λ(x : Carrier M) → x ) |
| 149 | 113 Lemma-MM9 = Extensionarity Lemma-MM34 |
| 144 | 114 |
| 151 | 115 Lemma-MM10 : ( λ x → ((M ∙ x) (ε M))) ≡ ( λ x → x ) |
| 149 | 116 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
|
117 |
| 151 | 118 Lemma-MM11 : (λ x y z → ((M ∙ (M ∙ x) y) z)) ≡ (λ x y z → ( _∙_ M x (_∙_ M y z ) )) |
| 149 | 119 Lemma-MM11 = Extensionarity3 Lemma-MM36 |
| 145 | 120 |
| 149 | 121 MonoidMonad : Monad A T η μ |
| 141 | 122 MonoidMonad = record { |
| 123 isMonad = record { | |
|
148
6e80e1aaa8b9
no yellow on monoid monad
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
147
diff
changeset
|
124 unity1 = Lemma-MM3 ; |
| 141 | 125 unity2 = Lemma-MM4 ; |
|
148
6e80e1aaa8b9
no yellow on monoid monad
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
147
diff
changeset
|
126 assoc = Lemma-MM5 |
| 141 | 127 } |
| 128 } where | |
| 147 | 129 Lemma-MM3 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] |
| 149 | 130 Lemma-MM3 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in |
| 141 | 131 begin |
| 132 TMap μ a o TMap η ( FObj T a ) | |
| 133 ≈⟨⟩ | |
| 151 | 134 ( λ x → ((M ∙ ε M) (proj₁ x) , proj₂ x )) |
| 149 | 135 ≈⟨ cong ( λ f → ( λ x → ( ( f (proj₁ x) ) , proj₂ x ))) ( Lemma-MM9 ) ⟩ |
| 147 | 136 ( λ (x : FObj T a) → (proj₁ x) , proj₂ x ) |
| 144 | 137 ≈⟨⟩ |
| 141 | 138 ( λ x → x ) |
| 139 ≈⟨⟩ | |
| 140 Id {_} {_} {_} {A} (FObj T a) | |
| 141 ∎ | |
| 142 Lemma-MM4 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] | |
| 149 | 143 Lemma-MM4 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in |
| 144 | 144 begin |
| 145 TMap μ a o (FMap T (TMap η a )) | |
| 146 ≈⟨⟩ | |
| 151 | 147 ( λ x → (M ∙ proj₁ x) (ε M) , proj₂ x ) |
| 149 | 148 ≈⟨ cong ( λ f → ( λ x → ( f (proj₁ x) ) , proj₂ x )) ( Lemma-MM10 ) ⟩ |
| 144 | 149 ( λ x → (proj₁ x) , proj₂ x ) |
| 150 ≈⟨⟩ | |
| 151 ( λ x → x ) | |
| 152 ≈⟨⟩ | |
| 153 Id {_} {_} {_} {A} (FObj T a) | |
| 154 ∎ | |
| 141 | 155 Lemma-MM5 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] |
| 149 | 156 Lemma-MM5 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in |
| 144 | 157 begin |
| 158 TMap μ a o TMap μ ( FObj T a ) | |
| 159 ≈⟨⟩ | |
| 151 | 160 ( λ x → (M ∙ (M ∙ proj₁ x) (proj₁ (proj₂ x))) (proj₁ (proj₂ (proj₂ x))) , proj₂ (proj₂ (proj₂ x))) |
| 149 | 161 ≈⟨ 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
|
162 (( 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
|
163 )) Lemma-MM11 ⟩ |
| 151 | 164 ( λ x → (M ∙ proj₁ x) ((M ∙ proj₁ (proj₂ x)) (proj₁ (proj₂ (proj₂ x)))) , proj₂ (proj₂ (proj₂ x))) |
| 144 | 165 ≈⟨⟩ |
| 166 TMap μ a o FMap T (TMap μ a) | |
| 167 ∎ | |
| 141 | 168 |
| 169 | |
| 151 | 170 F : (m : Carrier M) -> { a b : Obj A } -> ( f : a -> b ) -> Hom A a ( FObj T b ) |
| 171 F m {a} {b} f = \(x : a ) -> ( m , ( f x) ) | |
| 141 | 172 |
| 151 | 173 postulate m m' : Carrier M |
| 174 postulate a b c' : Obj A | |
| 175 postulate f : b -> c' | |
| 176 postulate g : a -> b | |
| 177 | |
| 178 LemmaMM12 = Monad.join MonoidMonad (F m f) (F m' g) | |
| 179 | |
| 180 open import kleisli {_} {_} {_} {A} {T} {η} {μ} {MonoidMonad} | |
| 181 | |
| 182 |