Mercurial > hg > Members > kono > Proof > category
annotate nat.agda @ 29:87cefecc5663
notation
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 13 Jul 2013 11:46:58 +0900 |
| parents | 5289c46d8eef |
| children | 98b8431a419b |
| 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 |
| 12 open Functor | |
| 13 | |
| 1 | 14 --T(g f) = T(g) T(f) |
| 15 | |
| 22 | 16 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 } |
| 17 → A [ ( FMap T (A [ g o f ] )) ≈ (A [ FMap T g o FMap T f ]) ] | |
| 18 Lemma1 = \t → IsFunctor.distr ( isFunctor t ) | |
| 0 | 19 |
| 20 -- F(f) | |
| 22 | 21 -- F(a) ---→ F(b) |
| 0 | 22 -- | | |
| 23 -- |t(a) |t(b) G(f)t(a) = t(b)F(f) | |
| 24 -- | | | |
| 25 -- v v | |
| 22 | 26 -- G(a) ---→ G(b) |
| 0 | 27 -- G(f) |
| 28 | |
| 7 | 29 record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′) |
| 0 | 30 ( F G : Functor D C ) |
| 7 | 31 (Trans : (A : Obj D) → Hom C (FObj F A) (FObj G A)) |
| 0 | 32 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where |
| 33 field | |
| 34 naturality : {a b : Obj D} {f : Hom D a b} | |
| 7 | 35 → C [ C [ ( FMap G f ) o ( Trans a ) ] ≈ C [ (Trans b ) o (FMap F f) ] ] |
| 0 | 36 -- uniqness : {d : Obj D} |
| 7 | 37 -- → C [ Trans d ≈ Trans d ] |
| 0 | 38 |
| 39 | |
| 7 | 40 record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) (F G : Functor domain codomain ) |
| 0 | 41 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where |
| 42 field | |
| 7 | 43 Trans : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A) |
| 44 isNTrans : IsNTrans domain codomain F G Trans | |
| 0 | 45 |
| 7 | 46 open NTrans |
| 1 | 47 Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A} |
| 22 | 48 → (μ : NTrans A A F G) → {a b : Obj A} { f : Hom A a b } |
| 49 → A [ A [ FMap G f o Trans μ a ] ≈ A [ Trans μ b o FMap F f ] ] | |
| 50 Lemma2 = \n → IsNTrans.naturality ( isNTrans n ) | |
| 0 | 51 |
| 52 open import Category.Cat | |
| 53 | |
| 22 | 54 -- η : 1_A → T |
| 55 -- μ : TT → T | |
| 0 | 56 -- μ(a)η(T(a)) = a |
| 57 -- μ(a)T(η(a)) = a | |
| 58 -- μ(a)(μ(T(a))) = μ(a)T(μ(a)) | |
| 59 | |
| 1 | 60 record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
| 61 ( T : Functor A A ) | |
| 7 | 62 ( η : NTrans A A identityFunctor T ) |
| 63 ( μ : NTrans A A (T ○ T) T) | |
| 1 | 64 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where |
| 65 field | |
| 22 | 66 assoc : {a : Obj A} → A [ A [ Trans μ a o Trans μ ( FObj T a ) ] ≈ A [ Trans μ a o FMap T (Trans μ a) ] ] |
| 67 unity1 : {a : Obj A} → A [ A [ Trans μ a o Trans η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] | |
| 68 unity2 : {a : Obj A} → A [ A [ Trans μ a o (FMap T (Trans η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] | |
| 0 | 69 |
| 7 | 70 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 | 71 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where |
| 7 | 72 eta : NTrans A A identityFunctor T |
| 6 | 73 eta = η |
| 7 | 74 mu : NTrans A A (T ○ T) T |
| 6 | 75 mu = μ |
| 1 | 76 field |
| 77 isMonad : IsMonad A T η μ | |
| 0 | 78 |
| 2 | 79 open Monad |
| 80 Lemma3 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} | |
| 81 { T : Functor A A } | |
| 7 | 82 { η : NTrans A A identityFunctor T } |
| 83 { μ : NTrans A A (T ○ T) T } | |
| 22 | 84 { a : Obj A } → |
| 2 | 85 ( M : Monad A T η μ ) |
| 22 | 86 → A [ A [ Trans μ a o Trans μ ( FObj T a ) ] ≈ A [ Trans μ a o FMap T (Trans μ a) ] ] |
| 87 Lemma3 = \m → IsMonad.assoc ( isMonad m ) | |
| 2 | 88 |
| 89 | |
| 90 Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b} | |
| 22 | 91 → A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ] |
| 92 Lemma4 = \a → IsCategory.identityL ( Category.isCategory a ) | |
| 0 | 93 |
| 3 | 94 Lemma5 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} |
| 95 { T : Functor A A } | |
| 7 | 96 { η : NTrans A A identityFunctor T } |
| 97 { μ : NTrans A A (T ○ T) T } | |
| 22 | 98 { a : Obj A } → |
| 3 | 99 ( M : Monad A T η μ ) |
| 22 | 100 → A [ A [ Trans μ a o Trans η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] |
| 101 Lemma5 = \m → IsMonad.unity1 ( isMonad m ) | |
| 3 | 102 |
| 103 Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} | |
| 104 { T : Functor A A } | |
| 7 | 105 { η : NTrans A A identityFunctor T } |
| 106 { μ : NTrans A A (T ○ T) T } | |
| 22 | 107 { a : Obj A } → |
| 3 | 108 ( M : Monad A T η μ ) |
| 22 | 109 → A [ A [ Trans μ a o (FMap T (Trans η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] |
| 110 Lemma6 = \m → IsMonad.unity2 ( isMonad m ) | |
| 3 | 111 |
| 112 -- T = M x A | |
| 0 | 113 -- nat of η |
| 114 -- g ○ f = μ(c) T(g) f | |
| 115 -- η(b) ○ f = f | |
| 116 -- f ○ η(a) = f | |
| 22 | 117 -- h ○ (g ○ f) = (h ○ g) ○ f |
| 0 | 118 |
| 4 | 119 record Kleisli { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) |
| 120 ( T : Functor A A ) | |
| 7 | 121 ( η : NTrans A A identityFunctor T ) |
| 122 ( μ : NTrans A A (T ○ T) T ) | |
| 4 | 123 ( M : Monad A T η μ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where |
| 5 | 124 monad : Monad A T η μ |
| 125 monad = M | |
| 22 | 126 -- g ○ f = μ(c) T(g) f |
| 127 join : { a b : Obj A } → ( c : Obj A ) → | |
| 128 ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c ) | |
| 7 | 129 join c g f = A [ Trans μ c o A [ FMap T g o f ] ] |
| 130 | |
| 10 | 131 |
| 7 | 132 |
| 18 | 133 module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where |
| 22 | 134 open import Relation.Binary.Core renaming ( Trans to Trasn1 ) |
| 7 | 135 |
| 29 | 136 _o_ : {a b c : Obj A } ( x : Hom A a b ) ( y : Hom A c a ) → Hom A c b |
| 137 x o y = A [ x o y ] | |
| 138 | |
| 139 _≈_ : {a b : Obj A } → Rel (Hom A a b) ℓ | |
| 140 x ≈ y = A [ x ≈ y ] | |
| 141 | |
| 142 infixr 9 _o_ | |
| 143 infix 4 _≈_ | |
| 144 | |
| 145 refl-hom : {a b : Obj A } { x : Hom A a b } → x ≈ x | |
| 18 | 146 refl-hom = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) |
| 8 | 147 |
| 29 | 148 trans-hom : {a b : Obj A } { x y z : Hom A a b } → |
| 149 x ≈ y → y ≈ z → x ≈ z | |
| 18 | 150 trans-hom b c = ( IsEquivalence.trans (IsCategory.isEquivalence ( Category.isCategory A ))) b c |
| 5 | 151 |
| 22 | 152 -- some short cuts |
| 153 | |
| 28 | 154 car : {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } → |
| 29 | 155 x ≈ y → ( x o f ) ≈ ( y o f ) |
| 28 | 156 car {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom ) eq |
| 22 | 157 |
| 28 | 158 cdr : {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } → |
| 29 | 159 x ≈ y → f o x ≈ f o y |
| 28 | 160 cdr {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom ) |
| 22 | 161 |
| 162 id : (a : Obj A ) → Hom A a a | |
| 163 id a = (Id {_} {_} {_} {A} a) | |
| 164 | |
| 29 | 165 idL : {a b : Obj A } { f : Hom A b a } → id a o f ≈ f |
| 22 | 166 idL = IsCategory.identityL (Category.isCategory A) |
| 167 | |
| 29 | 168 idR : {a b : Obj A } { f : Hom A a b } → f o id a ≈ f |
| 22 | 169 idR = IsCategory.identityR (Category.isCategory A) |
| 170 | |
| 29 | 171 sym : {a b : Obj A } { f g : Hom A a b } → f ≈ g → g ≈ f |
| 23 | 172 sym = IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A)) |
| 173 | |
| 22 | 174 assoc : {a b c d : Obj A } {f : Hom A c d} {g : Hom A b c} {h : Hom A a b} |
| 29 | 175 → f o ( g o h ) ≈ ( f o g ) o h |
| 22 | 176 assoc = IsCategory.associative (Category.isCategory A) |
| 177 | |
| 24 | 178 distr : (T : Functor A A) → {a b c : Obj A} {g : Hom A b c} { f : Hom A a b } |
| 29 | 179 → FMap T ( g o f ) ≈ FMap T g o FMap T f |
| 24 | 180 distr T = IsFunctor.distr ( isFunctor T ) |
| 22 | 181 |
| 182 nat : { c₁′ c₂′ ℓ′ : Level} (D : Category c₁′ c₂′ ℓ′) {a b : Obj D} {f : Hom D a b} {F G : Functor D A } | |
| 183 → (η : NTrans D A F G ) | |
| 29 | 184 → FMap G f o Trans η a ≈ Trans η b o FMap F f |
| 22 | 185 nat _ η = IsNTrans.naturality ( isNTrans η ) |
| 186 | |
| 18 | 187 infixr 2 _∎ |
| 188 infixr 2 _≈⟨_⟩_ | |
| 189 infix 1 begin_ | |
| 7 | 190 |
| 27 | 191 ------ If we have this, for example, as an axiom of a category, we can use ≡-Reasoning directly |
| 29 | 192 -- ≈-to-≡ : {a b : Obj A } { x y : Hom A a b } → A [ x ≈ y ] → x ≡ y |
| 27 | 193 -- ≈-to-≡ refl-hom = refl |
| 12 | 194 |
| 18 | 195 data _IsRelatedTo_ { a b : Obj A } ( x y : Hom A a b ) : |
| 196 Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where | |
| 29 | 197 relTo : (x≈y : x ≈ y ) → x IsRelatedTo y |
| 17 | 198 |
| 18 | 199 begin_ : { a b : Obj A } { x y : Hom A a b } → |
| 29 | 200 x IsRelatedTo y → x ≈ y |
| 18 | 201 begin relTo x≈y = x≈y |
| 17 | 202 |
| 18 | 203 _≈⟨_⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } → |
| 29 | 204 x ≈ y → y IsRelatedTo z → x IsRelatedTo z |
| 18 | 205 _ ≈⟨ x≈y ⟩ relTo y≈z = relTo (trans-hom x≈y y≈z) |
| 17 | 206 |
| 18 | 207 _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x |
| 208 _∎ _ = relTo refl-hom | |
| 17 | 209 |
| 22 | 210 lemma12 : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b c : Obj L } → |
| 211 ( x : Hom L c a ) → ( y : Hom L b c ) → L [ L [ x o y ] ≈ L [ x o y ] ] | |
| 18 | 212 lemma12 L x y = |
| 213 let open ≈-Reasoning ( L ) in | |
| 214 begin L [ x o y ] ∎ | |
| 11 | 215 |
| 22 | 216 Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → |
| 217 { a : Obj A } ( b : Obj A ) → | |
| 17 | 218 ( f : Hom A a b ) |
| 22 | 219 → A [ A [ (Id {_} {_} {_} {A} b) o f ] ≈ f ] |
| 18 | 220 Lemma61 c b g = -- IsCategory.identityL (Category.isCategory c) |
| 221 let open ≈-Reasoning (c) in | |
| 17 | 222 begin |
| 18 | 223 c [ Id {_} {_} {_} {c} b o g ] |
| 224 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ | |
| 17 | 225 g |
| 226 ∎ | |
| 11 | 227 |
| 4 | 228 open Kleisli |
| 22 | 229 -- η(b) ○ f = f |
| 230 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → | |
| 21 | 231 ( T : Functor A A ) |
| 232 ( η : NTrans A A identityFunctor T ) | |
| 7 | 233 { μ : NTrans A A (T ○ T) T } |
| 21 | 234 { a : Obj A } ( b : Obj A ) |
| 235 ( f : Hom A a ( FObj T b) ) | |
| 22 | 236 ( m : Monad A T η μ ) |
| 237 ( k : Kleisli A T η μ m) | |
| 238 → A [ join k b (Trans η b) f ≈ f ] | |
| 21 | 239 Lemma7 c T η b f m k = |
| 240 let open ≈-Reasoning (c) | |
| 241 μ = mu ( monad k ) | |
| 242 in | |
| 243 begin | |
| 244 join k b (Trans η b) f | |
| 245 ≈⟨ refl-hom ⟩ | |
| 246 c [ Trans μ b o c [ FMap T ((Trans η b)) o f ] ] | |
| 247 ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ | |
| 248 c [ c [ Trans μ b o FMap T ((Trans η b)) ] o f ] | |
| 28 | 249 ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad k )) ) ⟩ |
| 22 | 250 c [ id (FObj T b) o f ] |
| 21 | 251 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ |
| 252 f | |
| 253 ∎ | |
| 7 | 254 |
| 22 | 255 -- f ○ η(a) = f |
| 256 Lemma8 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) | |
| 257 ( T : Functor A A ) | |
| 258 ( η : NTrans A A identityFunctor T ) | |
| 7 | 259 { μ : NTrans A A (T ○ T) T } |
| 22 | 260 ( a : Obj A ) ( b : Obj A ) |
| 261 ( f : Hom A a ( FObj T b) ) | |
| 262 ( m : Monad A T η μ ) | |
| 263 ( k : Kleisli A T η μ m) | |
| 264 → A [ join k b f (Trans η a) ≈ f ] | |
| 265 Lemma8 c T η a b f m k = | |
| 266 begin | |
| 267 join k b f (Trans η a) | |
| 268 ≈⟨ refl-hom ⟩ | |
| 269 c [ Trans μ b o c [ FMap T f o (Trans η a) ] ] | |
| 28 | 270 ≈⟨ cdr ( IsNTrans.naturality ( isNTrans η )) ⟩ |
| 22 | 271 c [ Trans μ b o c [ (Trans η ( FObj T b)) o f ] ] |
| 272 ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ | |
| 273 c [ c [ Trans μ b o (Trans η ( FObj T b)) ] o f ] | |
| 28 | 274 ≈⟨ car ( IsMonad.unity1 ( isMonad ( monad k )) ) ⟩ |
| 22 | 275 c [ id (FObj T b) o f ] |
| 276 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ | |
| 277 f | |
| 278 ∎ where | |
| 279 open ≈-Reasoning (c) | |
| 280 μ = mu ( monad k ) | |
| 5 | 281 |
| 22 | 282 -- h ○ (g ○ f) = (h ○ g) ○ f |
| 23 | 283 Lemma9 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
| 284 ( T : Functor A A ) | |
| 285 ( η : NTrans A A identityFunctor T ) | |
| 286 ( μ : NTrans A A (T ○ T) T ) | |
| 287 ( a b c d : Obj A ) | |
| 288 ( f : Hom A a ( FObj T b) ) | |
| 289 ( g : Hom A b ( FObj T c) ) | |
| 290 ( h : Hom A c ( FObj T d) ) | |
| 291 ( m : Monad A T η μ ) | |
| 292 ( k : Kleisli A T η μ m) | |
| 22 | 293 → A [ join k d h (join k c g f) ≈ join k d ( join k d h g) f ] |
| 24 | 294 Lemma9 A T η μ a b c d f g h m k = |
| 295 begin | |
| 23 | 296 join k d h (join k c g f) |
| 28 | 297 ≈⟨ refl-hom ⟩ |
| 298 join k d h ( ( Trans μ c o ( FMap T g o f ) ) ) | |
| 299 ≈⟨ refl-hom ⟩ | |
| 300 ( Trans μ d o ( FMap T h o ( Trans μ c o ( FMap T g o f ) ) ) ) | |
| 301 ≈⟨ cdr ( cdr ( assoc )) ⟩ | |
| 302 ( Trans μ d o ( FMap T h o ( ( Trans μ c o FMap T g ) o f ) ) ) | |
| 303 ≈⟨ assoc ⟩ --- ( f o ( g o h ) ) = ( ( f o g ) o h ) | |
| 304 ( ( Trans μ d o FMap T h ) o ( (Trans μ c o FMap T g ) o f ) ) | |
| 25 | 305 ≈⟨ assoc ⟩ |
| 28 | 306 ( ( ( Trans μ d o FMap T h ) o (Trans μ c o FMap T g ) ) o f ) |
| 307 ≈⟨ car (sym assoc) ⟩ | |
| 308 ( ( Trans μ d o ( FMap T h o ( Trans μ c o FMap T g ) ) ) o f ) | |
| 309 ≈⟨ car ( cdr (assoc) ) ⟩ | |
| 310 ( ( Trans μ d o ( ( FMap T h o Trans μ c ) o FMap T g ) ) o f ) | |
| 311 ≈⟨ car assoc ⟩ | |
| 312 ( ( ( Trans μ d o ( FMap T h o Trans μ c ) ) o FMap T g ) o f ) | |
| 313 ≈⟨ car (car ( cdr ( begin | |
| 314 ( FMap T h o Trans μ c ) | |
|
26
ad62c87659ef
join association finish
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
25
diff
changeset
|
315 ≈⟨ nat A μ ⟩ |
| 28 | 316 ( Trans μ (FObj T d) o FMap T (FMap T h) ) |
| 25 | 317 ∎ |
| 318 ))) ⟩ | |
| 28 | 319 ( ( ( Trans μ d o ( Trans μ ( FObj T d) o FMap T ( FMap T h ) ) ) o FMap T g ) o f ) |
| 320 ≈⟨ car (sym assoc) ⟩ | |
| 321 ( ( Trans μ d o ( ( Trans μ ( FObj T d) o FMap T ( FMap T h ) ) o FMap T g ) ) o f ) | |
| 322 ≈⟨ car ( cdr (sym assoc) ) ⟩ | |
| 323 ( ( Trans μ d o ( Trans μ ( FObj T d) o ( FMap T ( FMap T h ) o FMap T g ) ) ) o f ) | |
| 324 ≈⟨ car ( cdr (cdr (sym (distr T )))) ⟩ | |
| 325 ( ( Trans μ d o ( Trans μ ( FObj T d) o FMap T ( ( FMap T h o g ) ) ) ) o f ) | |
| 326 ≈⟨ car assoc ⟩ | |
| 327 ( ( ( Trans μ d o Trans μ ( FObj T d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) | |
| 328 ≈⟨ car ( car ( | |
| 27 | 329 begin |
| 28 | 330 ( Trans μ d o Trans μ (FObj T d) ) |
| 27 | 331 ≈⟨ IsMonad.assoc ( isMonad m) ⟩ |
| 28 | 332 ( Trans μ d o FMap T (Trans μ d) ) |
| 27 | 333 ∎ |
| 334 )) ⟩ | |
| 28 | 335 ( ( ( Trans μ d o FMap T ( Trans μ d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) |
| 336 ≈⟨ car (sym assoc) ⟩ | |
| 337 ( ( Trans μ d o ( FMap T ( Trans μ d ) o FMap T ( ( FMap T h o g ) ) ) ) o f ) | |
| 24 | 338 ≈⟨ sym assoc ⟩ |
| 28 | 339 ( Trans μ d o ( ( FMap T ( Trans μ d ) o FMap T ( ( FMap T h o g ) ) ) o f ) ) |
| 340 ≈⟨ cdr ( car ( sym ( distr T ))) ⟩ | |
| 341 ( Trans μ d o ( FMap T ( ( ( Trans μ d ) o ( FMap T h o g ) ) ) o f ) ) | |
| 23 | 342 ≈⟨ refl-hom ⟩ |
| 28 | 343 join k d ( ( Trans μ d o ( FMap T h o g ) ) ) f |
| 23 | 344 ≈⟨ refl-hom ⟩ |
| 345 join k d ( join k d h g) f | |
| 24 | 346 ∎ where open ≈-Reasoning (A) |
| 3 | 347 |
| 348 | |
| 349 | |
| 350 -- Kleisli : | |
| 351 -- Kleisli = record { Hom = | |
| 352 -- ; Hom = _⟶_ | |
| 353 -- ; Id = IdProd | |
| 354 -- ; _o_ = _∘_ | |
| 355 -- ; _≈_ = _≈_ | |
| 356 -- ; isCategory = record { isEquivalence = record { refl = λ {φ} → ≈-refl {φ = φ} | |
| 357 -- ; sym = λ {φ ψ} → ≈-symm {φ = φ} {ψ} | |
| 358 -- ; trans = λ {φ ψ σ} → ≈-trans {φ = φ} {ψ} {σ} | |
| 359 -- } | |
| 360 -- ; identityL = identityL | |
| 361 -- ; identityR = identityR | |
| 362 -- ; o-resp-≈ = o-resp-≈ | |
| 363 -- ; associative = associative | |
| 364 -- } | |
| 365 -- } |