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