Mercurial > hg > Members > kono > Proof > category
annotate nat.agda @ 49:d2b5be1143bf
naturality of ε
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 23 Jul 2013 10:13:09 +0900 |
| parents | 17b8bafebad7 |
| children | 83ff8d48fdca |
| rev | line source |
|---|---|
| 0 | 1 module nat where |
| 2 | |
| 3 -- Monad | |
| 4 -- Category A | |
| 5 -- A = Category | |
| 22 | 6 -- Functor T : A → A |
| 0 | 7 --T(a) = t(a) |
| 8 --T(f) = tf(f) | |
| 9 | |
| 2 | 10 open import Category -- https://github.com/konn/category-agda |
| 0 | 11 open import Level |
| 31 | 12 open import Category.HomReasoning |
| 0 | 13 |
| 1 | 14 --T(g f) = T(g) T(f) |
| 15 | |
| 31 | 16 open Functor |
| 22 | 17 Lemma1 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} (T : Functor A A) → {a b c : Obj A} {g : Hom A b c} { f : Hom A a b } |
| 18 → A [ ( FMap T (A [ g o f ] )) ≈ (A [ FMap T g o FMap T f ]) ] | |
| 19 Lemma1 = \t → IsFunctor.distr ( isFunctor t ) | |
| 0 | 20 |
| 21 | |
| 7 | 22 open NTrans |
| 1 | 23 Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A} |
| 22 | 24 → (μ : NTrans A A F G) → {a b : Obj A} { f : Hom A a b } |
| 30 | 25 → A [ A [ FMap G f o TMap μ a ] ≈ A [ TMap μ b o FMap F f ] ] |
| 22 | 26 Lemma2 = \n → IsNTrans.naturality ( isNTrans n ) |
| 0 | 27 |
| 28 open import Category.Cat | |
| 29 | |
| 22 | 30 -- η : 1_A → T |
| 31 -- μ : TT → T | |
| 0 | 32 -- μ(a)η(T(a)) = a |
| 33 -- μ(a)T(η(a)) = a | |
| 34 -- μ(a)(μ(T(a))) = μ(a)T(μ(a)) | |
| 35 | |
| 1 | 36 record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
| 37 ( T : Functor A A ) | |
| 7 | 38 ( η : NTrans A A identityFunctor T ) |
| 39 ( μ : NTrans A A (T ○ T) T) | |
| 1 | 40 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where |
| 41 field | |
| 30 | 42 assoc : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] |
| 43 unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] | |
| 44 unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] | |
| 0 | 45 |
| 7 | 46 record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T) |
| 1 | 47 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where |
| 7 | 48 eta : NTrans A A identityFunctor T |
| 6 | 49 eta = η |
| 7 | 50 mu : NTrans A A (T ○ T) T |
| 6 | 51 mu = μ |
| 1 | 52 field |
| 53 isMonad : IsMonad A T η μ | |
| 0 | 54 |
| 2 | 55 open Monad |
| 56 Lemma3 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} | |
| 57 { T : Functor A A } | |
| 7 | 58 { η : NTrans A A identityFunctor T } |
| 59 { μ : NTrans A A (T ○ T) T } | |
| 22 | 60 { a : Obj A } → |
| 2 | 61 ( M : Monad A T η μ ) |
| 30 | 62 → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] |
| 22 | 63 Lemma3 = \m → IsMonad.assoc ( isMonad m ) |
| 2 | 64 |
| 65 | |
| 66 Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b} | |
| 22 | 67 → A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ] |
| 68 Lemma4 = \a → IsCategory.identityL ( Category.isCategory a ) | |
| 0 | 69 |
| 3 | 70 Lemma5 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} |
| 71 { T : Functor A A } | |
| 7 | 72 { η : NTrans A A identityFunctor T } |
| 73 { μ : NTrans A A (T ○ T) T } | |
| 22 | 74 { a : Obj A } → |
| 3 | 75 ( M : Monad A T η μ ) |
| 30 | 76 → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] |
| 22 | 77 Lemma5 = \m → IsMonad.unity1 ( isMonad m ) |
| 3 | 78 |
| 79 Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} | |
| 80 { T : Functor A A } | |
| 7 | 81 { η : NTrans A A identityFunctor T } |
| 82 { μ : NTrans A A (T ○ T) T } | |
| 22 | 83 { a : Obj A } → |
| 3 | 84 ( M : Monad A T η μ ) |
| 30 | 85 → A [ A [ TMap μ a o (FMap T (TMap η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] |
| 22 | 86 Lemma6 = \m → IsMonad.unity2 ( isMonad m ) |
| 3 | 87 |
| 88 -- T = M x A | |
| 0 | 89 -- nat of η |
| 90 -- g ○ f = μ(c) T(g) f | |
| 91 -- η(b) ○ f = f | |
| 92 -- f ○ η(a) = f | |
| 22 | 93 -- h ○ (g ○ f) = (h ○ g) ○ f |
| 0 | 94 |
| 4 | 95 record Kleisli { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) |
| 96 ( T : Functor A A ) | |
| 7 | 97 ( η : NTrans A A identityFunctor T ) |
| 98 ( μ : NTrans A A (T ○ T) T ) | |
| 4 | 99 ( M : Monad A T η μ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where |
| 5 | 100 monad : Monad A T η μ |
| 101 monad = M | |
| 22 | 102 -- g ○ f = μ(c) T(g) f |
| 103 join : { a b : Obj A } → ( c : Obj A ) → | |
| 104 ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c ) | |
| 30 | 105 join c g f = A [ TMap μ c o A [ FMap T g o f ] ] |
| 7 | 106 |
| 22 | 107 lemma12 : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b c : Obj L } → |
| 108 ( x : Hom L c a ) → ( y : Hom L b c ) → L [ L [ x o y ] ≈ L [ x o y ] ] | |
| 18 | 109 lemma12 L x y = |
| 110 let open ≈-Reasoning ( L ) in | |
| 111 begin L [ x o y ] ∎ | |
| 11 | 112 |
| 113 | |
| 4 | 114 open Kleisli |
| 22 | 115 -- η(b) ○ f = f |
| 116 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → | |
| 21 | 117 ( T : Functor A A ) |
| 118 ( η : NTrans A A identityFunctor T ) | |
| 7 | 119 { μ : NTrans A A (T ○ T) T } |
| 21 | 120 { a : Obj A } ( b : Obj A ) |
| 121 ( f : Hom A a ( FObj T b) ) | |
| 22 | 122 ( m : Monad A T η μ ) |
| 123 ( k : Kleisli A T η μ m) | |
| 30 | 124 → A [ join k b (TMap η b) f ≈ f ] |
| 21 | 125 Lemma7 c T η b f m k = |
| 126 let open ≈-Reasoning (c) | |
| 127 μ = mu ( monad k ) | |
| 128 in | |
| 129 begin | |
| 30 | 130 join k b (TMap η b) f |
| 21 | 131 ≈⟨ refl-hom ⟩ |
| 30 | 132 c [ TMap μ b o c [ FMap T ((TMap η b)) o f ] ] |
| 21 | 133 ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ |
| 30 | 134 c [ c [ TMap μ b o FMap T ((TMap η b)) ] o f ] |
| 28 | 135 ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad k )) ) ⟩ |
| 22 | 136 c [ id (FObj T b) o f ] |
| 21 | 137 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ |
| 138 f | |
| 139 ∎ | |
| 7 | 140 |
| 22 | 141 -- f ○ η(a) = f |
| 142 Lemma8 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) | |
| 143 ( T : Functor A A ) | |
| 144 ( η : NTrans A A identityFunctor T ) | |
| 7 | 145 { μ : NTrans A A (T ○ T) T } |
| 22 | 146 ( a : Obj A ) ( b : Obj A ) |
| 147 ( f : Hom A a ( FObj T b) ) | |
| 148 ( m : Monad A T η μ ) | |
| 149 ( k : Kleisli A T η μ m) | |
| 30 | 150 → A [ join k b f (TMap η a) ≈ f ] |
| 22 | 151 Lemma8 c T η a b f m k = |
| 152 begin | |
| 30 | 153 join k b f (TMap η a) |
| 22 | 154 ≈⟨ refl-hom ⟩ |
| 30 | 155 c [ TMap μ b o c [ FMap T f o (TMap η a) ] ] |
| 28 | 156 ≈⟨ cdr ( IsNTrans.naturality ( isNTrans η )) ⟩ |
| 30 | 157 c [ TMap μ b o c [ (TMap η ( FObj T b)) o f ] ] |
| 22 | 158 ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ |
| 30 | 159 c [ c [ TMap μ b o (TMap η ( FObj T b)) ] o f ] |
| 28 | 160 ≈⟨ car ( IsMonad.unity1 ( isMonad ( monad k )) ) ⟩ |
| 22 | 161 c [ id (FObj T b) o f ] |
| 162 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ | |
| 163 f | |
| 164 ∎ where | |
| 165 open ≈-Reasoning (c) | |
| 166 μ = mu ( monad k ) | |
| 5 | 167 |
| 22 | 168 -- h ○ (g ○ f) = (h ○ g) ○ f |
| 23 | 169 Lemma9 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
| 170 ( T : Functor A A ) | |
| 171 ( η : NTrans A A identityFunctor T ) | |
| 172 ( μ : NTrans A A (T ○ T) T ) | |
| 173 ( a b c d : Obj A ) | |
| 174 ( f : Hom A a ( FObj T b) ) | |
| 175 ( g : Hom A b ( FObj T c) ) | |
| 176 ( h : Hom A c ( FObj T d) ) | |
| 177 ( m : Monad A T η μ ) | |
| 178 ( k : Kleisli A T η μ m) | |
| 22 | 179 → A [ join k d h (join k c g f) ≈ join k d ( join k d h g) f ] |
| 24 | 180 Lemma9 A T η μ a b c d f g h m k = |
| 181 begin | |
| 23 | 182 join k d h (join k c g f) |
| 30 | 183 ≈⟨⟩ |
| 184 join k d h ( ( TMap μ c o ( FMap T g o f ) ) ) | |
| 28 | 185 ≈⟨ refl-hom ⟩ |
| 30 | 186 ( TMap μ d o ( FMap T h o ( TMap μ c o ( FMap T g o f ) ) ) ) |
| 28 | 187 ≈⟨ cdr ( cdr ( assoc )) ⟩ |
| 30 | 188 ( TMap μ d o ( FMap T h o ( ( TMap μ c o FMap T g ) o f ) ) ) |
| 28 | 189 ≈⟨ assoc ⟩ --- ( f o ( g o h ) ) = ( ( f o g ) o h ) |
| 30 | 190 ( ( TMap μ d o FMap T h ) o ( (TMap μ c o FMap T g ) o f ) ) |
| 25 | 191 ≈⟨ assoc ⟩ |
| 30 | 192 ( ( ( TMap μ d o FMap T h ) o (TMap μ c o FMap T g ) ) o f ) |
| 28 | 193 ≈⟨ car (sym assoc) ⟩ |
| 30 | 194 ( ( TMap μ d o ( FMap T h o ( TMap μ c o FMap T g ) ) ) o f ) |
| 28 | 195 ≈⟨ car ( cdr (assoc) ) ⟩ |
| 30 | 196 ( ( TMap μ d o ( ( FMap T h o TMap μ c ) o FMap T g ) ) o f ) |
| 28 | 197 ≈⟨ car assoc ⟩ |
| 30 | 198 ( ( ( TMap μ d o ( FMap T h o TMap μ c ) ) o FMap T g ) o f ) |
| 28 | 199 ≈⟨ car (car ( cdr ( begin |
| 30 | 200 ( FMap T h o TMap μ c ) |
|
26
ad62c87659ef
join association finish
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
25
diff
changeset
|
201 ≈⟨ nat A μ ⟩ |
| 30 | 202 ( TMap μ (FObj T d) o FMap T (FMap T h) ) |
| 25 | 203 ∎ |
| 204 ))) ⟩ | |
| 30 | 205 ( ( ( TMap μ d o ( TMap μ ( FObj T d) o FMap T ( FMap T h ) ) ) o FMap T g ) o f ) |
| 28 | 206 ≈⟨ car (sym assoc) ⟩ |
| 30 | 207 ( ( TMap μ d o ( ( TMap μ ( FObj T d) o FMap T ( FMap T h ) ) o FMap T g ) ) o f ) |
| 28 | 208 ≈⟨ car ( cdr (sym assoc) ) ⟩ |
| 30 | 209 ( ( TMap μ d o ( TMap μ ( FObj T d) o ( FMap T ( FMap T h ) o FMap T g ) ) ) o f ) |
| 28 | 210 ≈⟨ car ( cdr (cdr (sym (distr T )))) ⟩ |
| 30 | 211 ( ( TMap μ d o ( TMap μ ( FObj T d) o FMap T ( ( FMap T h o g ) ) ) ) o f ) |
| 28 | 212 ≈⟨ car assoc ⟩ |
| 30 | 213 ( ( ( TMap μ d o TMap μ ( FObj T d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) |
| 28 | 214 ≈⟨ car ( car ( |
| 27 | 215 begin |
| 30 | 216 ( TMap μ d o TMap μ (FObj T d) ) |
| 27 | 217 ≈⟨ IsMonad.assoc ( isMonad m) ⟩ |
| 30 | 218 ( TMap μ d o FMap T (TMap μ d) ) |
| 27 | 219 ∎ |
| 220 )) ⟩ | |
| 30 | 221 ( ( ( TMap μ d o FMap T ( TMap μ d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) |
| 28 | 222 ≈⟨ car (sym assoc) ⟩ |
| 30 | 223 ( ( TMap μ d o ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) ) o f ) |
| 24 | 224 ≈⟨ sym assoc ⟩ |
| 30 | 225 ( TMap μ d o ( ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) o f ) ) |
| 28 | 226 ≈⟨ cdr ( car ( sym ( distr T ))) ⟩ |
| 30 | 227 ( TMap μ d o ( FMap T ( ( ( TMap μ d ) o ( FMap T h o g ) ) ) o f ) ) |
| 23 | 228 ≈⟨ refl-hom ⟩ |
| 30 | 229 join k d ( ( TMap μ d o ( FMap T h o g ) ) ) f |
| 23 | 230 ≈⟨ refl-hom ⟩ |
| 231 join k d ( join k d h g) f | |
| 24 | 232 ∎ where open ≈-Reasoning (A) |
| 3 | 233 |
| 234 | |
| 235 | |
| 236 -- Kleisli : | |
| 237 -- Kleisli = record { Hom = | |
| 238 -- ; Hom = _⟶_ | |
| 239 -- ; Id = IdProd | |
| 240 -- ; _o_ = _∘_ | |
| 241 -- ; _≈_ = _≈_ | |
| 242 -- ; isCategory = record { isEquivalence = record { refl = λ {φ} → ≈-refl {φ = φ} | |
| 243 -- ; sym = λ {φ ψ} → ≈-symm {φ = φ} {ψ} | |
| 244 -- ; trans = λ {φ ψ σ} → ≈-trans {φ = φ} {ψ} {σ} | |
| 245 -- } | |
| 246 -- ; identityL = identityL | |
| 247 -- ; identityR = identityR | |
| 248 -- ; o-resp-≈ = o-resp-≈ | |
| 249 -- ; associative = associative | |
| 250 -- } | |
| 251 -- } |