Mercurial > hg > Members > kono > Proof > category
annotate monoid-monad.agda @ 781:340708e8d54f
fix for 2.5.4.2
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 08 Mar 2019 17:46:59 +0900 |
parents | 60942538dc41 |
children | bded2347efa4 |
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 |
781 | 18 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym ) |
19 | |
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
|
20 |
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 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
|
22 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
|
23 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
|
24 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
|
25 _∙_ : Op₂ Carrier |
301 | 26 ε : Carrier -- id in Monoid |
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
|
27 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
|
28 |
151 | 29 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
|
30 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
|
31 |
149 | 32 A = Sets {c} |
138 | 33 |
139 | 34 -- T : A → (M x A) |
134 | 35 |
149 | 36 T : Functor A A |
138 | 37 T = record { |
151 | 38 FObj = λ a → (Carrier M) × a |
149 | 39 ; FMap = λ f → map ( λ x → x ) f |
138 | 40 ; isFunctor = record { |
41 identity = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets )) | |
42 ; distr = (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets ))) | |
43 ; ≈-cong = cong1 | |
44 } | |
45 } where | |
139 | 46 cong1 : {ℓ′ : Level} → {a b : Set ℓ′} { f g : Hom (Sets {ℓ′}) a b} → |
151 | 47 Sets [ f ≈ g ] → Sets [ map (λ (x : Carrier M) → x) f ≈ map (λ (x : Carrier M) → x) g ] |
138 | 48 cong1 _≡_.refl = _≡_.refl |
129 | 49 |
144 | 50 open Functor |
51 | |
149 | 52 Lemma-MM1 : {a b : Obj A} {f : Hom A a b} → |
151 | 53 A [ A [ FMap T f o (λ x → ε M , x) ] ≈ |
54 A [ (λ x → ε M , x) o f ] ] | |
149 | 55 Lemma-MM1 {a} {b} {f} = let open ≈-Reasoning A renaming ( _o_ to _*_ ) in |
139 | 56 begin |
151 | 57 FMap T f o (λ x → ε M , x) |
139 | 58 ≈⟨⟩ |
151 | 59 (λ x → ε M , x) o f |
139 | 60 ∎ |
61 | |
150 | 62 -- η : a → (ε,a) |
149 | 63 η : NTrans A A identityFunctor T |
139 | 64 η = record { |
151 | 65 TMap = λ a → λ(x : a) → ( ε M , x ) ; |
139 | 66 isNTrans = record { |
149 | 67 commute = Lemma-MM1 |
139 | 68 } |
69 } | |
70 | |
150 | 71 -- μ : (m,(m',a)) → (m*m,a) |
139 | 72 |
151 | 73 muMap : (a : Obj A ) → FObj T ( FObj T a ) → Σ (Carrier M) (λ x → a ) |
74 muMap a ( m , ( m' , x ) ) = ( _∙_ M m m' , x ) | |
139 | 75 |
149 | 76 Lemma-MM2 : {a b : Obj A} {f : Hom A a b} → |
77 A [ A [ FMap T f o (λ x → muMap a x) ] ≈ | |
78 A [ (λ x → muMap b x) o FMap (T ○ T) f ] ] | |
79 Lemma-MM2 {a} {b} {f} = let open ≈-Reasoning A renaming ( _o_ to _*_ ) in | |
139 | 80 begin |
81 FMap T f o (λ x → muMap a x) | |
82 ≈⟨⟩ | |
83 (λ x → muMap b x) o FMap (T ○ T) f | |
84 ∎ | |
85 | |
149 | 86 μ : NTrans A A ( T ○ T ) T |
139 | 87 μ = record { |
149 | 88 TMap = λ a → λ x → muMap a x ; |
139 | 89 isNTrans = record { |
149 | 90 commute = λ{a} {b} {f} → Lemma-MM2 {a} {b} {f} |
139 | 91 } |
92 } | |
141 | 93 |
94 open NTrans | |
95 | |
144 | 96 Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b} {x : Σ A B } → (((proj₁ x) , proj₂ x ) ≡ x ) |
142 | 97 Lemma-MM33 = _≡_.refl |
98 | |
169
44bf6e78f891
builtin extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
168
diff
changeset
|
99 Lemma-MM34 : ∀( x : Carrier M ) → ( (M ∙ ε M) x ≡ x ) |
44bf6e78f891
builtin extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
168
diff
changeset
|
100 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
|
101 |
169
44bf6e78f891
builtin extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
168
diff
changeset
|
102 Lemma-MM35 : ∀( x : Carrier M ) → ((M ∙ x) (ε M)) ≡ x |
44bf6e78f891
builtin extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
168
diff
changeset
|
103 Lemma-MM35 x = ( proj₂ ( IsMonoid.identity ( isMonoid M )) ) x |
141 | 104 |
170
721cf9d9f5e3
use functional extensionality in library
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
169
diff
changeset
|
105 Lemma-MM36 : ∀( x y z : Carrier M ) → ((M ∙ (M ∙ x) y) z) ≡ (_∙_ M x (_∙_ M y z ) ) |
721cf9d9f5e3
use functional extensionality in library
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
169
diff
changeset
|
106 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
|
107 |
168 | 108 -- 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
|
109 import Relation.Binary.PropositionalEquality |
170
721cf9d9f5e3
use functional extensionality in library
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
169
diff
changeset
|
110 -- postulate extensionality : { a b : Obj A } {f g : Hom A a b } → Relation.Binary.PropositionalEquality.Extensionality c c |
721cf9d9f5e3
use functional extensionality in library
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
169
diff
changeset
|
111 postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c |
144 | 112 |
170
721cf9d9f5e3
use functional extensionality in library
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
169
diff
changeset
|
113 -- Multi Arguments Functional Extensionality |
721cf9d9f5e3
use functional extensionality in library
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
169
diff
changeset
|
114 extensionality30 : {f g : Carrier M → Carrier M → Carrier M → Carrier M } → |
721cf9d9f5e3
use functional extensionality in library
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
169
diff
changeset
|
115 (∀ x y z → f x y z ≡ g x y z ) → ( f ≡ g ) |
300 | 116 extensionality30 eq = extensionality ( λ x → extensionality ( λ y → extensionality (eq x y) ) ) |
144 | 117 |
151 | 118 Lemma-MM9 : ( λ(x : Carrier M) → ( M ∙ ε M ) x ) ≡ ( λ(x : Carrier M) → x ) |
170
721cf9d9f5e3
use functional extensionality in library
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
169
diff
changeset
|
119 Lemma-MM9 = extensionality Lemma-MM34 |
144 | 120 |
151 | 121 Lemma-MM10 : ( λ x → ((M ∙ x) (ε M))) ≡ ( λ x → x ) |
170
721cf9d9f5e3
use functional extensionality in library
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
169
diff
changeset
|
122 Lemma-MM10 = extensionality 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
|
123 |
151 | 124 Lemma-MM11 : (λ x y z → ((M ∙ (M ∙ x) y) z)) ≡ (λ x y z → ( _∙_ M x (_∙_ M y z ) )) |
170
721cf9d9f5e3
use functional extensionality in library
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
169
diff
changeset
|
125 Lemma-MM11 = extensionality30 Lemma-MM36 |
145 | 126 |
773 | 127 MonoidMonad : Monad A |
141 | 128 MonoidMonad = record { |
773 | 129 T = T |
130 ; η = η | |
131 ; μ = μ | |
132 ; isMonad = record { | |
148
6e80e1aaa8b9
no yellow on monoid monad
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
147
diff
changeset
|
133 unity1 = Lemma-MM3 ; |
141 | 134 unity2 = Lemma-MM4 ; |
148
6e80e1aaa8b9
no yellow on monoid monad
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
147
diff
changeset
|
135 assoc = Lemma-MM5 |
141 | 136 } |
137 } where | |
147 | 138 Lemma-MM3 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] |
149 | 139 Lemma-MM3 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in |
141 | 140 begin |
141 TMap μ a o TMap η ( FObj T a ) | |
142 ≈⟨⟩ | |
151 | 143 ( λ x → ((M ∙ ε M) (proj₁ x) , proj₂ x )) |
149 | 144 ≈⟨ cong ( λ f → ( λ x → ( ( f (proj₁ x) ) , proj₂ x ))) ( Lemma-MM9 ) ⟩ |
147 | 145 ( λ (x : FObj T a) → (proj₁ x) , proj₂ x ) |
144 | 146 ≈⟨⟩ |
141 | 147 ( λ x → x ) |
148 ≈⟨⟩ | |
149 Id {_} {_} {_} {A} (FObj T a) | |
150 ∎ | |
151 Lemma-MM4 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] | |
149 | 152 Lemma-MM4 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in |
144 | 153 begin |
154 TMap μ a o (FMap T (TMap η a )) | |
155 ≈⟨⟩ | |
151 | 156 ( λ x → (M ∙ proj₁ x) (ε M) , proj₂ x ) |
149 | 157 ≈⟨ cong ( λ f → ( λ x → ( f (proj₁ x) ) , proj₂ x )) ( Lemma-MM10 ) ⟩ |
144 | 158 ( λ x → (proj₁ x) , proj₂ x ) |
159 ≈⟨⟩ | |
160 ( λ x → x ) | |
161 ≈⟨⟩ | |
162 Id {_} {_} {_} {A} (FObj T a) | |
163 ∎ | |
141 | 164 Lemma-MM5 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] |
149 | 165 Lemma-MM5 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in |
144 | 166 begin |
167 TMap μ a o TMap μ ( FObj T a ) | |
168 ≈⟨⟩ | |
151 | 169 ( λ x → (M ∙ (M ∙ proj₁ x) (proj₁ (proj₂ x))) (proj₁ (proj₂ (proj₂ x))) , proj₂ (proj₂ (proj₂ x))) |
149 | 170 ≈⟨ 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
|
171 (( 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
|
172 )) Lemma-MM11 ⟩ |
151 | 173 ( λ x → (M ∙ proj₁ x) ((M ∙ proj₁ (proj₂ x)) (proj₁ (proj₂ (proj₂ x)))) , proj₂ (proj₂ (proj₂ x))) |
144 | 174 ≈⟨⟩ |
175 TMap μ a o FMap T (TMap μ a) | |
176 ∎ | |
141 | 177 |
178 | |
300 | 179 F : (m : Carrier M) → { a b : Obj A } → ( f : a → b ) → Hom A a ( FObj T b ) |
180 F m {a} {b} f = λ (x : a ) → ( m , ( f x) ) | |
141 | 181 |
151 | 182 postulate m m' : Carrier M |
183 postulate a b c' : Obj A | |
300 | 184 postulate f : b → c' |
185 postulate g : a → b | |
151 | 186 |
153 | 187 Lemma-MM12 = Monad.join MonoidMonad (F m f) (F m' g) |
151 | 188 |
773 | 189 open import kleisli {_} {_} {_} {A} {T} {η} {μ} {Monad.isMonad MonoidMonad} |
151 | 190 |
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
170
diff
changeset
|
191 -- nat-ε TMap = λ a₁ → record { KMap = λ x → x } |
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
170
diff
changeset
|
192 -- nat-η TMap = λ a₁ → _,_ (ε, M) |
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
170
diff
changeset
|
193 -- U_T Functor Kleisli A |
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
170
diff
changeset
|
194 -- U_T FObj = λ B → Σ (Carrier M) (λ x → B) FMap = λ {a₁} {b₁} f₁ x → ( proj₁ x ∙ (proj₁ (KMap f₁ (proj₂ x))) , proj₂ (KMap f₁ (proj₂ x)) |
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
170
diff
changeset
|
195 -- F_T Functor A Kleisli |
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
170
diff
changeset
|
196 -- F_T FObj = λ a₁ → a₁ FMap = λ {a₁} {b₁} f₁ → record { KMap = λ x → ε M , f₁ x } |