Mercurial > hg > Members > kono > Proof > category
comparison stdalone-kleisli.agda @ 774:f3a493da92e8
add simple category version
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 13 Jun 2018 12:56:38 +0900 |
| parents | |
| children | 06a7831cf6ce |
comparison
equal
deleted
inserted
replaced
| 773:60942538dc41 | 774:f3a493da92e8 |
|---|---|
| 1 module stdalone-kleisli where | |
| 2 | |
| 3 open import Level | |
| 4 open import Relation.Binary | |
| 5 open import Relation.Binary.Core | |
| 6 | |
| 7 -- h g f | |
| 8 -- a ---→ b ---→ c ---→ d | |
| 9 -- | |
| 10 | |
| 11 record IsCategory {l : Level} ( Obj : Set (suc l) ) (Hom : Obj → Obj → Set l ) | |
| 12 ( _o_ : { a b c : Obj } → Hom b c → Hom a b → Hom a c ) | |
| 13 ( id : ( a : Obj ) → Hom a a ) | |
| 14 : Set (suc l) where | |
| 15 field | |
| 16 idL : { a b : Obj } { f : Hom a b } → ( id b o f ) ≡ f | |
| 17 idR : { a b : Obj } { f : Hom a b } → ( f o id a ) ≡ f | |
| 18 assoc : { a b c d : Obj } { f : Hom c d }{ g : Hom b c }{ h : Hom a b } → f o ( g o h ) ≡ ( f o g ) o h | |
| 19 | |
| 20 record Category {l : Level} : Set (suc (suc l)) where | |
| 21 field | |
| 22 Obj : Set (suc l) | |
| 23 Hom : Obj → Obj → Set l | |
| 24 _o_ : { a b c : Obj } → Hom b c → Hom a b → Hom a c | |
| 25 id : ( a : Obj ) → Hom a a | |
| 26 isCategory : IsCategory Obj Hom _o_ id | |
| 27 | |
| 28 Sets : Category | |
| 29 Sets = record { | |
| 30 Obj = Set | |
| 31 ; Hom = λ a b → a → b | |
| 32 ; _o_ = λ f g x → f ( g x ) | |
| 33 ; id = λ A x → x | |
| 34 ; isCategory = record { | |
| 35 idL = refl | |
| 36 ; idR = refl | |
| 37 ; assoc = refl | |
| 38 } | |
| 39 } | |
| 40 | |
| 41 | |
| 42 open Category | |
| 43 | |
| 44 _[_o_] : {l : Level} (C : Category {l} ) → {a b c : Obj C} → Hom C b c → Hom C a b → Hom C a c | |
| 45 C [ f o g ] = Category._o_ C f g | |
| 46 | |
| 47 -- | |
| 48 -- f g | |
| 49 -- a ----→ b -----→ c | |
| 50 -- | | | | |
| 51 -- T| T| T| | |
| 52 -- | | | | |
| 53 -- v v v | |
| 54 -- Ta ----→ Tb ----→ Tc | |
| 55 -- Tf Tg | |
| 56 | |
| 57 | |
| 58 record IsFunctor {l : Level} (C D : Category {l} ) | |
| 59 (FObj : Obj C → Obj D) | |
| 60 (FMap : {A B : Obj C} → Hom C A B → Hom D (FObj A) (FObj B)) | |
| 61 : Set (suc l ) where | |
| 62 field | |
| 63 identity : {A : Obj C} → FMap (id C A) ≡ id D (FObj A) | |
| 64 distr : {a b c : Obj C} {f : Hom C a b} {g : Hom C b c} | |
| 65 → FMap ( C [ g o f ]) ≡ (D [ FMap g o FMap f ] ) | |
| 66 | |
| 67 record Functor {l : Level} (domain codomain : Category {l} ) | |
| 68 : Set (suc l) where | |
| 69 field | |
| 70 FObj : Obj domain → Obj codomain | |
| 71 FMap : {A B : Obj domain} → Hom domain A B → Hom codomain (FObj A) (FObj B) | |
| 72 isFunctor : IsFunctor domain codomain FObj FMap | |
| 73 | |
| 74 open Functor | |
| 75 | |
| 76 idFunctor : {l : Level } { C : Category {l} } → Functor C C | |
| 77 idFunctor = record { | |
| 78 FObj = λ x → x | |
| 79 ; FMap = λ f → f | |
| 80 ; isFunctor = record { | |
| 81 identity = refl | |
| 82 ; distr = refl | |
| 83 } | |
| 84 } | |
| 85 | |
| 86 open import Relation.Binary.PropositionalEquality hiding ( [_] ) | |
| 87 | |
| 88 | |
| 89 _●_ : {l : Level} { A B C : Category {l} } → ( S : Functor B C ) ( T : Functor A B ) → Functor A C | |
| 90 _●_ {l} {A} {B} {C} S T = record { | |
| 91 FObj = λ x → FObj S ( FObj T x ) | |
| 92 ; FMap = λ f → FMap S ( FMap T f ) | |
| 93 ; isFunctor = record { | |
| 94 identity = λ {a} → identity a | |
| 95 ; distr = λ {a} {b} {c} {f} {g} → distr | |
| 96 } | |
| 97 } where | |
| 98 identity : (a : Obj A) → FMap S (FMap T (id A a)) ≡ id C (FObj S (FObj T a)) | |
| 99 identity a = let open ≡-Reasoning in begin | |
| 100 FMap S (FMap T (id A a)) | |
| 101 ≡⟨ cong ( λ z → FMap S z ) ( IsFunctor.identity (isFunctor T ) ) ⟩ | |
| 102 FMap S (id B (FObj T a) ) | |
| 103 ≡⟨ IsFunctor.identity (isFunctor S ) ⟩ | |
| 104 id C (FObj S (FObj T a)) | |
| 105 ∎ | |
| 106 distr : {a b c : Obj A} { f : Hom A a b } { g : Hom A b c } → FMap S (FMap T (A [ g o f ])) ≡ (C [ FMap S (FMap T g) o FMap S (FMap T f) ]) | |
| 107 distr {a} {b} {c} {f} {g} = let open ≡-Reasoning in begin | |
| 108 FMap S (FMap T (A [ g o f ])) | |
| 109 ≡⟨ cong ( λ z → FMap S z ) ( IsFunctor.distr (isFunctor T ) ) ⟩ | |
| 110 FMap S ( B [ FMap T g o FMap T f ] ) | |
| 111 ≡⟨ IsFunctor.distr (isFunctor S ) ⟩ | |
| 112 C [ FMap S (FMap T g) o FMap S (FMap T f) ] | |
| 113 ∎ | |
| 114 | |
| 115 | |
| 116 -- {A : Set c₁ } {B : Set c₂ } → { f g : A → B } → f x ≡ g x → f ≡ g | |
| 117 postulate extensionality : { c₁ c₂ : Level} → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ | |
| 118 | |
| 119 -- | |
| 120 -- t a | |
| 121 -- F a -----→ G a | |
| 122 -- | | | |
| 123 -- Ff | | Gf | |
| 124 -- v v | |
| 125 -- F b ------→ G b | |
| 126 -- t b | |
| 127 -- | |
| 128 | |
| 129 record IsNTrans { l : Level } (D C : Category {l} ) ( F G : Functor D C ) | |
| 130 (TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A)) | |
| 131 : Set (suc l) where | |
| 132 field | |
| 133 commute : {a b : Obj D} {f : Hom D a b} | |
| 134 → C [ ( FMap G f ) o ( TMap a ) ] ≡ C [ (TMap b ) o (FMap F f) ] | |
| 135 | |
| 136 record NTrans {l : Level} {domain codomain : Category {l} } (F G : Functor domain codomain ) | |
| 137 : Set (suc l) where | |
| 138 field | |
| 139 TMap : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A) | |
| 140 isNTrans : IsNTrans domain codomain F G TMap | |
| 141 | |
| 142 | |
| 143 | |
| 144 open NTrans | |
| 145 | |
| 146 -- | |
| 147 -- | |
| 148 -- η : 1 ------→ T | |
| 149 -- μ : TT -----→ T | |
| 150 -- | |
| 151 -- η μT | |
| 152 -- T -----→ TT TTT ------→ TT | |
| 153 -- | | | | | |
| 154 -- Tη | |μ Tμ | |Tμ | |
| 155 -- v | v v | |
| 156 -- TT -----→ T TT -------→ T | |
| 157 -- μ μT | |
| 158 | |
| 159 | |
| 160 record IsMonad {l : Level} { C : Category {l} } (T : Functor C C) ( η : NTrans idFunctor T ) ( μ : NTrans (T ● T) T ) | |
| 161 : Set (suc l) where | |
| 162 field | |
| 163 assoc : {a : Obj C} → C [ TMap μ a o TMap μ ( FObj T a ) ] ≡ C [ TMap μ a o FMap T (TMap μ a) ] | |
| 164 unity1 : {a : Obj C} → C [ TMap μ a o TMap η ( FObj T a ) ] ≡ id C (FObj T a) | |
| 165 unity2 : {a : Obj C} → C [ TMap μ a o (FMap T (TMap η a ))] ≡ id C (FObj T a) | |
| 166 | |
| 167 | |
| 168 record Monad {l : Level} { C : Category {l} } (T : Functor C C) : Set (suc l) where | |
| 169 field | |
| 170 η : NTrans idFunctor T | |
| 171 μ : NTrans (T ● T) T | |
| 172 isMonad : IsMonad T η μ | |
| 173 | |
| 174 record KleisliHom { c : Level} { A : Category {c} } { T : Functor A A } (a : Obj A) (b : Obj A) | |
| 175 : Set c where | |
| 176 field | |
| 177 KMap : Hom A a ( FObj T b ) | |
| 178 | |
| 179 open KleisliHom | |
| 180 | |
| 181 | |
| 182 left : {l : Level} (C : Category {l} ) {a b c : Obj C } {f f' : Hom C b c } {g : Hom C a b } → f ≡ f' → C [ f o g ] ≡ C [ f' o g ] | |
| 183 left {l} C {a} {b} {c} {f} {f'} {g} refl = cong ( λ z → C [ z o g ] ) refl | |
| 184 | |
| 185 right : {l : Level} (C : Category {l} ) {a b c : Obj C } {f : Hom C b c } {g g' : Hom C a b } → g ≡ g' → C [ f o g ] ≡ C [ f o g' ] | |
| 186 right {l} C {a} {b} {c} {f} {g} {g'} refl = cong ( λ z → C [ f o z ] ) refl | |
| 187 | |
| 188 Assoc : {l : Level} (C : Category {l} ) {a b c d : Obj C } {f : Hom C c d } {g : Hom C b c } { h : Hom C a b } | |
| 189 → C [ f o C [ g o h ] ] ≡ C [ C [ f o g ] o h ] | |
| 190 Assoc {l} C = IsCategory.assoc ( isCategory C ) | |
| 191 | |
| 192 | |
| 193 Kleisli : {l : Level} (C : Category {l} ) (T : Functor C C ) ( M : Monad T ) → Category {l} | |
| 194 Kleisli C T M = record { | |
| 195 Obj = Obj C | |
| 196 ; Hom = λ a b → KleisliHom {_} {C} {T} a b | |
| 197 ; _o_ = λ {a} {b} {c} f g → join {a} {b} {c} f g | |
| 198 ; id = λ a → record { KMap = TMap (Monad.η M) a } | |
| 199 ; isCategory = record { | |
| 200 idL = idL | |
| 201 ; idR = idR | |
| 202 ; assoc = assoc | |
| 203 } | |
| 204 } where | |
| 205 join : { a b c : Obj C } → KleisliHom b c → KleisliHom a b → KleisliHom a c | |
| 206 join {a} {b} {c} f g = record { KMap = ( C [ TMap (Monad.μ M) c o C [ FMap T ( KMap f ) o KMap g ] ] ) } | |
| 207 idL : {a b : Obj C} {f : KleisliHom a b} → join (record { KMap = TMap (Monad.η M) b }) f ≡ f | |
| 208 idL {a} {b} {f} = let open ≡-Reasoning in begin | |
| 209 record { KMap = C [ TMap (Monad.μ M) b o C [ FMap T (TMap (Monad.η M) b) o KMap f ] ] } | |
| 210 ≡⟨ cong ( λ z → record { KMap = z } ) ( begin | |
| 211 C [ TMap (Monad.μ M) b o C [ FMap T (TMap (Monad.η M) b) o KMap f ] ] | |
| 212 ≡⟨ IsCategory.assoc ( isCategory C ) ⟩ | |
| 213 C [ C [ TMap (Monad.μ M) b o FMap T (TMap (Monad.η M) b) ] o KMap f ] | |
| 214 ≡⟨ cong ( λ z → C [ z o KMap f ] ) ( IsMonad.unity2 (Monad.isMonad M ) ) ⟩ | |
| 215 C [ id C (FObj T b) o KMap f ] | |
| 216 ≡⟨ IsCategory.idL ( isCategory C ) ⟩ | |
| 217 KMap f | |
| 218 ∎ ) ⟩ | |
| 219 record { KMap = KMap f } | |
| 220 ∎ | |
| 221 idR : {a b : Obj C} {f : KleisliHom a b} → join f (record { KMap = TMap (Monad.η M) a }) ≡ f | |
| 222 idR {a} {b} {f} = let open ≡-Reasoning in begin | |
| 223 record { KMap = C [ TMap (Monad.μ M) b o C [ FMap T (KMap f) o TMap (Monad.η M) a ] ] } | |
| 224 ≡⟨ cong ( λ z → record { KMap = z } ) ( begin | |
| 225 C [ TMap (Monad.μ M) b o C [ FMap T (KMap f) o TMap (Monad.η M) a ] ] | |
| 226 ≡⟨ cong ( λ z → C [ TMap (Monad.μ M) b o z ] ) ( IsNTrans.commute (isNTrans (Monad.η M) )) ⟩ | |
| 227 C [ TMap (Monad.μ M) b o C [ TMap (Monad.η M) (FObj T b) o KMap f ] ] | |
| 228 ≡⟨ IsCategory.assoc ( isCategory C ) ⟩ | |
| 229 C [ C [ TMap (Monad.μ M) b o TMap (Monad.η M) (FObj T b) ] o KMap f ] | |
| 230 ≡⟨ cong ( λ z → C [ z o KMap f ] ) ( IsMonad.unity1 (Monad.isMonad M ) ) ⟩ | |
| 231 C [ id C (FObj T b) o KMap f ] | |
| 232 ≡⟨ IsCategory.idL ( isCategory C ) ⟩ | |
| 233 KMap f | |
| 234 ∎ ) ⟩ | |
| 235 record { KMap = KMap f } | |
| 236 ∎ | |
| 237 -- | |
| 238 -- TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ ( TMap (Monad.μ M) c ・ ( FMap T (KMap g) ・ KMap h ) ) ) ) | |
| 239 -- | |
| 240 -- h T g μ c | |
| 241 -- a ---→ T b -----------------→ T T c -------------------------→ T c | |
| 242 -- | | | | |
| 243 -- | | | | |
| 244 -- | | T T f NAT μ | T f | |
| 245 -- | | | | |
| 246 -- | v μ (T d) v | |
| 247 -- | distr T T T T d -------------------------→ T T d | |
| 248 -- | | | | |
| 249 -- | | | | |
| 250 -- | | T μ d Monad-assoc | μ d | |
| 251 -- | | | | |
| 252 -- | v v | |
| 253 -- +------------------→ T T d -------------------------→ T d | |
| 254 -- T (μ d・T f・g) μ d | |
| 255 -- | |
| 256 -- TMap (Monad.μ M) d ・ ( FMap T (( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ KMap g ) ) ) ・ KMap h ) ) | |
| 257 -- | |
| 258 _・_ : {a b c : Obj C } ( f : Hom C b c ) ( g : Hom C a b ) → Hom C a c | |
| 259 f ・ g = C [ f o g ] | |
| 260 assoc : {a b c d : Obj C} {f : KleisliHom c d} {g : KleisliHom b c} {h : KleisliHom a b} → join f (join g h) ≡ join (join f g) h | |
| 261 assoc {a} {b} {c} {d} {f} {g} {h} = let open ≡-Reasoning in begin | |
| 262 join f (join g h) | |
| 263 ≡⟨⟩ | |
| 264 record { KMap = TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ ( TMap (Monad.μ M) c ・ ( FMap T (KMap g) ・ KMap h ))) } | |
| 265 ≡⟨ cong ( λ z → record { KMap = z } ) ( begin | |
| 266 ( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ ( TMap (Monad.μ M) c ・ ( FMap T (KMap g) ・ KMap h ) ) ) ) | |
| 267 ≡⟨ right C ( right C (Assoc C)) ⟩ | |
| 268 ( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ ( ( TMap (Monad.μ M) c ・ FMap T (KMap g) ) ・ KMap h ) ) ) | |
| 269 ≡⟨ Assoc C ⟩ | |
| 270 ( ( TMap (Monad.μ M) d ・ FMap T (KMap f) ) ・ ( ( TMap (Monad.μ M) c ・ FMap T (KMap g) ) ・ KMap h ) ) | |
| 271 ≡⟨ Assoc C ⟩ | |
| 272 ( ( ( TMap (Monad.μ M) d ・ FMap T (KMap f) ) ・ ( TMap (Monad.μ M) c ・ FMap T (KMap g) ) ) ・ KMap h ) | |
| 273 ≡⟨ sym ( left C (Assoc C )) ⟩ | |
| 274 ( ( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ ( TMap (Monad.μ M) c ・ FMap T (KMap g) ) ) ) ・ KMap h ) | |
| 275 ≡⟨ left C ( right C (Assoc C)) ⟩ | |
| 276 ( ( TMap (Monad.μ M) d ・ ( ( FMap T (KMap f) ・ TMap (Monad.μ M) c ) ・ FMap T (KMap g) ) ) ・ KMap h ) | |
| 277 ≡⟨ left C (Assoc C)⟩ | |
| 278 ( ( ( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ TMap (Monad.μ M) c ) ) ・ FMap T (KMap g) ) ・ KMap h ) | |
| 279 ≡⟨ left C ( left C ( right C ( IsNTrans.commute (isNTrans (Monad.μ M) ) ) )) ⟩ | |
| 280 ( ( ( TMap (Monad.μ M) d ・ ( TMap (Monad.μ M) (FObj T d) ・ FMap (T ● T) (KMap f) ) ) ・ FMap T (KMap g) ) ・ KMap h ) | |
| 281 ≡⟨ sym ( left C (Assoc C)) ⟩ | |
| 282 ( ( TMap (Monad.μ M) d ・ ( ( TMap (Monad.μ M) (FObj T d) ・ FMap (T ● T) (KMap f) ) ・ FMap T (KMap g) ) ) ・ KMap h ) | |
| 283 ≡⟨ sym ( left C ( right C (Assoc C))) ⟩ | |
| 284 ( ( TMap (Monad.μ M) d ・ ( TMap (Monad.μ M) (FObj T d) ・ ( FMap (T ● T) (KMap f) ・ FMap T (KMap g) ) ) ) ・ KMap h ) | |
| 285 ≡⟨ sym ( left C ( right C (right C (IsFunctor.distr (isFunctor T ) ) ) )) ⟩ | |
| 286 ( ( TMap (Monad.μ M) d ・ ( TMap (Monad.μ M) (FObj T d) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ) ・ KMap h ) | |
| 287 ≡⟨ left C (Assoc C) ⟩ | |
| 288 ( ( ( TMap (Monad.μ M) d ・ TMap (Monad.μ M) (FObj T d) ) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ・ KMap h ) | |
| 289 ≡⟨ left C (left C ( IsMonad.assoc (Monad.isMonad M ) ) ) ⟩ | |
| 290 ( ( ( TMap (Monad.μ M) d ・ FMap T (TMap (Monad.μ M) d) ) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ・ KMap h ) | |
| 291 ≡⟨ sym ( left C (Assoc C)) ⟩ | |
| 292 ( ( TMap (Monad.μ M) d ・ ( FMap T (TMap (Monad.μ M) d) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ) ・ KMap h ) | |
| 293 ≡⟨ sym (Assoc C) ⟩ | |
| 294 ( TMap (Monad.μ M) d ・ ( ( FMap T (TMap (Monad.μ M) d) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ・ KMap h ) ) | |
| 295 ≡⟨ sym (right C ( left C (IsFunctor.distr (isFunctor T )))) ⟩ | |
| 296 ( TMap (Monad.μ M) d ・ ( FMap T (( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ KMap g ) ) ) ・ KMap h ) ) | |
| 297 ∎ ) ⟩ | |
| 298 record { KMap = ( TMap (Monad.μ M) d ・ ( FMap T (( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ KMap g ) ) ) ・ KMap h ) ) } | |
| 299 ≡⟨⟩ | |
| 300 join (join f g) h | |
| 301 ∎ | |
| 302 | |
| 303 -- | |
| 304 -- U : Kleisli Sets | |
| 305 -- F : Sets Kleisli | |
| 306 -- | |
| 307 -- Hom Klei a b ←---→ Hom Sets a (U●F b ) | |
| 308 -- | |
| 309 -- Hom Klei (F a) (F b) ←---→ Hom Sets a (U●F b ) | |
| 310 -- | |
| 311 -- Hom Klei (F a) b ←---→ Hom Sets a U(b) Hom Klei (F a) b ←---→ Hom Sets a U(b) | |
| 312 -- | | | | | |
| 313 -- Ff| f| |f |Uf | |
| 314 -- | | | | | |
| 315 -- ↓ ↓ ↓ ↓ | |
| 316 -- Hom Klei (F (f a)) b ←---→ Hom Sets (f a) U(b) Hom Klei (F a) (f b) ←---→ Hom Sets a U(f b) | |
| 317 -- | |
| 318 -- | |
| 319 | |
| 320 record UnityOfOppsite ( Kleisli : Category ) ( U : Functor Kleisli Sets ) ( F : Functor Sets Kleisli ) : Set (suc zero) where | |
| 321 field | |
| 322 hom-right : {a : Obj Sets} { b : Obj Kleisli } → Hom Sets a ( FObj U b ) → Hom Kleisli (FObj F a) b | |
| 323 hom-left : {a : Obj Sets} { b : Obj Kleisli } → Hom Kleisli (FObj F a) b → Hom Sets a ( FObj U b ) | |
| 324 hom-right-injective : {a : Obj Sets} { b : Obj Kleisli } → {f : Hom Sets a (FObj U b) } → hom-left ( hom-right f ) ≡ f | |
| 325 hom-left-injective : {a : Obj Sets} { b : Obj Kleisli } → {f : Hom Kleisli (FObj F a) b } → hom-right ( hom-left f ) ≡ f | |
| 326 --- naturality of Φ | |
| 327 hom-left-commute1 : {a : Obj Sets} {b b' : Obj Kleisli } → | |
| 328 { f : Hom Kleisli (FObj F a) b } → { k : Hom Kleisli b b' } → | |
| 329 hom-left ( Kleisli [ k o f ] ) ≡ Sets [ FMap U k o hom-left f ] | |
| 330 hom-left-commute2 : {a a' : Obj Sets} {b : Obj Kleisli } → | |
| 331 { f : Hom Kleisli (FObj F a) b } → { h : Hom Sets a' a } → | |
| 332 hom-left ( Kleisli [ f o FMap F h ] ) ≡ Sets [ hom-left f o h ] | |
| 333 hom-right-commute1 : {a : Obj Sets} {b b' : Obj Kleisli } → | |
| 334 { g : Hom Sets a (FObj U b)} → { k : Hom Kleisli b b' } → | |
| 335 Kleisli [ k o hom-right g ] ≡ hom-right ( Sets [ FMap U k o g ] ) | |
| 336 hom-right-commute1 {a} {b} {b'} {g} {k} = let open ≡-Reasoning in begin | |
| 337 Kleisli [ k o hom-right g ] | |
| 338 ≡⟨ sym hom-left-injective ⟩ | |
| 339 hom-right ( hom-left ( Kleisli [ k o hom-right g ] ) ) | |
| 340 ≡⟨ cong ( λ z → hom-right z ) hom-left-commute1 ⟩ | |
| 341 hom-right (Sets [ FMap U k o hom-left (hom-right g) ]) | |
| 342 ≡⟨ cong ( λ z → hom-right ( Sets [ FMap U k o z ] )) hom-right-injective ⟩ | |
| 343 hom-right ( Sets [ FMap U k o g ] ) | |
| 344 ∎ | |
| 345 hom-right-commute2 : {a a' : Obj Sets} {b : Obj Kleisli } → | |
| 346 { g : Hom Sets a (FObj U b) } → { h : Hom Sets a' a } → | |
| 347 Kleisli [ hom-right g o FMap F h ] ≡ hom-right ( Sets [ g o h ] ) | |
| 348 hom-right-commute2 {a} {a'} {b} {g} {h} = let open ≡-Reasoning in begin | |
| 349 Kleisli [ hom-right g o FMap F h ] | |
| 350 ≡⟨ sym hom-left-injective ⟩ | |
| 351 hom-right (hom-left (Kleisli [ hom-right g o FMap F h ])) | |
| 352 ≡⟨ cong ( λ z → hom-right z ) hom-left-commute2 ⟩ | |
| 353 hom-right (Sets [ hom-left (hom-right g) o h ]) | |
| 354 ≡⟨ cong ( λ z → hom-right ( Sets [ z o h ] )) hom-right-injective ⟩ | |
| 355 hom-right (Sets [ g o h ]) | |
| 356 ∎ | |
| 357 | |
| 358 | |
| 359 | |
| 360 | |
| 361 _・_ : {a b c : Obj Sets } ( f : Hom Sets b c ) ( g : Hom Sets a b ) → Hom Sets a c | |
| 362 f ・ g = Sets [ f o g ] | |
| 363 | |
| 364 U : ( T : Functor Sets Sets ) → { m : Monad T } → Functor (Kleisli Sets T m) Sets | |
| 365 U T {m} = record { | |
| 366 FObj = FObj T | |
| 367 ; FMap = λ {a} {b} f x → TMap ( μ m ) b ( FMap T ( KMap f ) x ) | |
| 368 ; isFunctor = record { identity = IsMonad.unity2 (isMonad m) ; distr = distr } | |
| 369 } where | |
| 370 open Monad | |
| 371 distr : {a b c : Obj (Kleisli Sets T m)} {f : Hom (Kleisli Sets T m) a b} {g : Hom (Kleisli Sets T m) b c} → | |
| 372 (λ x → TMap (μ m) c (FMap T (KMap (Kleisli Sets T m [ g o f ])) x)) | |
| 373 ≡ (Sets [ (λ x → TMap (μ m) c (FMap T (KMap g) x)) o (λ x → TMap (μ m) b (FMap T (KMap f) x)) ]) | |
| 374 distr {a} {b} {c} {f} {g} = let open ≡-Reasoning in begin | |
| 375 Sets [ TMap (μ m) c o FMap T (KMap (Kleisli Sets T m [ g o f ])) ] | |
| 376 ≡⟨⟩ | |
| 377 Sets [ TMap (μ m) c o FMap T ( Sets [ TMap (μ m) c o Sets [ FMap T ( KMap g ) o KMap f ] ] ) ] | |
| 378 ≡⟨ right Sets {_} {_} {_} {TMap (μ m) c} {_} {_} ( IsFunctor.distr (Functor.isFunctor T) ) ⟩ | |
| 379 Sets [ TMap (μ m) c o Sets [ FMap T ( TMap (μ m) c) o FMap T ( Sets [ FMap T (KMap g) o KMap f ] ) ] ] | |
| 380 ≡⟨ sym ( left Sets (IsMonad.assoc (isMonad m ))) ⟩ | |
| 381 Sets [ Sets [ TMap (μ m) c o TMap (μ m) (FObj T c) ] o (FMap T (Sets [ FMap T (KMap g) o KMap f ])) ] | |
| 382 ≡⟨ right Sets {_} {_} {_} {TMap (μ m) c} ( right Sets {_} {_} {_} {TMap (μ m) (FObj T c)} ( IsFunctor.distr (Functor.isFunctor T) ) ) ⟩ | |
| 383 Sets [ Sets [ TMap (μ m) c o TMap (μ m) (FObj T c) ] o Sets [ FMap T ( FMap T (KMap g)) o FMap T ( KMap f ) ] ] | |
| 384 ≡⟨ sym ( right Sets {_} {_} {_} {TMap (μ m) c} ( left Sets (IsNTrans.commute ( NTrans.isNTrans (μ m))))) ⟩ | |
| 385 Sets [ Sets [ TMap (μ m) c o FMap T (KMap g) ] o Sets [ TMap (μ m) b o FMap T (KMap f) ] ] | |
| 386 ∎ | |
| 387 | |
| 388 | |
| 389 F : ( T : Functor Sets Sets ) → {m : Monad T} → Functor Sets ( Kleisli Sets T m) | |
| 390 F T {m} = record { | |
| 391 FObj = λ a → a ; FMap = λ {a} {b} f → record { KMap = λ x → TMap (η m) b (f x) } | |
| 392 ; isFunctor = record { identity = refl ; distr = distr } | |
| 393 } where | |
| 394 open Monad | |
| 395 distr : {a b c : Obj Sets} {f : Hom Sets a b} {g : Hom Sets b c} → record { KMap = λ x → TMap (η m) c ((Sets [ g o f ]) x) } ≡ | |
| 396 Kleisli Sets T m [ record { KMap = λ x → TMap (η m) c (g x) } o record { KMap = λ x → TMap (η m) b (f x) } ] | |
| 397 distr {a} {b} {c} {f} {g} = let open ≡-Reasoning in ( cong ( λ z → record { KMap = z } ) ( begin | |
| 398 Sets [ TMap (η m) c o Sets [ g o f ] ] | |
| 399 ≡⟨ left Sets {_} {_} {_} {Sets [ TMap (η m) c o g ] } ( sym ( IsNTrans.commute ( NTrans.isNTrans (η m) ) )) ⟩ | |
| 400 Sets [ Sets [ FMap T g o TMap (η m) b ] o f ] | |
| 401 ≡⟨ sym ( IsCategory.idL ( Category.isCategory Sets )) ⟩ | |
| 402 Sets [ ( λ x → x ) o Sets [ Sets [ FMap T g o TMap (η m) b ] o f ] ] | |
| 403 ≡⟨ sym ( left Sets (IsMonad.unity2 (isMonad m ))) ⟩ | |
| 404 Sets [ Sets [ TMap (μ m) c o FMap T (TMap (η m) c) ] o Sets [ FMap T g o Sets [ TMap (η m) b o f ] ] ] | |
| 405 ≡⟨ sym ( right Sets {_} {_} {_} {TMap (μ m) c} {_} ( left Sets {_} {_} {_} { FMap T (Sets [ TMap (η m) c o g ] )} ( IsFunctor.distr (Functor.isFunctor T) ))) ⟩ | |
| 406 Sets [ TMap (μ m) c o ( Sets [ FMap T (Sets [ TMap (η m) c o g ] ) o Sets [ TMap (η m) b o f ] ] ) ] | |
| 407 ∎ )) | |
| 408 | |
| 409 -- | |
| 410 -- Hom Sets a (FObj U b) = Hom Sets a (T b) | |
| 411 -- Hom Kleisli (FObj F a) b = Hom Sets a (T b) | |
| 412 -- | |
| 413 | |
| 414 lemma→ : ( T : Functor Sets Sets ) → (m : Monad T ) → UnityOfOppsite (Kleisli Sets T m) (U T {m} ) (F T {m}) | |
| 415 lemma→ T m = | |
| 416 let open Monad in | |
| 417 record { | |
| 418 hom-right = λ {a} {b} f → record { KMap = f } | |
| 419 ; hom-left = λ {a} {b} f x → TMap (μ m) b ( TMap ( η m ) (FObj T b) ( (KMap f) x ) ) | |
| 420 ; hom-right-injective = hom-right-injective | |
| 421 ; hom-left-injective = hom-left-injective | |
| 422 ; hom-left-commute1 = hom-left-commute1 | |
| 423 ; hom-left-commute2 = hom-left-commute2 | |
| 424 } where | |
| 425 open Monad | |
| 426 hom-right-injective : {a : Obj Sets} {b : Obj (Kleisli Sets T m)} | |
| 427 {f : Hom Sets a (FObj (U T {m}) b)} → (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (f x))) ≡ f | |
| 428 hom-right-injective {a} {b} {f} = let open ≡-Reasoning in begin | |
| 429 Sets [ TMap (μ m) b o Sets [ TMap (η m) (FObj T b) o f ] ] | |
| 430 ≡⟨ left Sets ( IsMonad.unity1 ( isMonad m ) ) ⟩ | |
| 431 Sets [ id Sets (FObj (U T {m}) b) o f ] | |
| 432 ≡⟨ IsCategory.idL ( isCategory Sets ) ⟩ | |
| 433 f | |
| 434 ∎ | |
| 435 hom-left-injective : {a : Obj Sets} {b : Obj (Kleisli Sets T m)} {f : Hom (Kleisli Sets T m) (FObj (F T {m}) a) b} | |
| 436 → record { KMap = λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap f x)) } ≡ f | |
| 437 hom-left-injective {a} {b} {f} = let open ≡-Reasoning in cong ( λ z → record { KMap = z } ) ( begin | |
| 438 Sets [ TMap (μ m) b o Sets [ TMap (η m) (FObj T b) o KMap f ] ] | |
| 439 ≡⟨ left Sets ( IsMonad.unity1 ( isMonad m ) ) ⟩ | |
| 440 KMap f | |
| 441 ∎ ) | |
| 442 hom-left-commute1 : {a : Obj Sets} {b b' : Obj (Kleisli Sets T m)} {f : Hom (Kleisli Sets T m) (FObj (F T {m}) a) b} {k : Hom (Kleisli Sets T m) b b'} → | |
| 443 (λ x → TMap (μ m) b' (TMap (η m) (FObj T b') (KMap (Kleisli Sets T m [ k o f ]) x))) | |
| 444 ≡ (Sets [ FMap (U T {m}) k o (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap f x))) ]) | |
| 445 hom-left-commute1 {a} {b} {b'} {f} {k} = let open ≡-Reasoning in begin | |
| 446 Sets [ TMap (μ m) b' o Sets [ TMap (η m) (FObj T b') o KMap (Kleisli Sets T m [ k o f ] ) ] ] | |
| 447 ≡⟨⟩ | |
| 448 TMap (μ m) b' ・ ( TMap (η m) (FObj T b') ・ ( TMap (μ m) b' ・ ( FMap T (KMap k) ・ KMap f ))) | |
| 449 ≡⟨ left Sets ( IsMonad.unity1 ( isMonad m )) ⟩ | |
| 450 TMap (μ m) b' ・ ( FMap T (KMap k) ・ KMap f ) | |
| 451 ≡⟨ right Sets {_} {_} {_} {TMap ( μ m ) b' ・ FMap T ( KMap k )} ( left Sets ( sym ( IsMonad.unity1 ( isMonad m ) ) ) ) ⟩ | |
| 452 ( TMap ( μ m ) b' ・ FMap T ( KMap k ) ) ・ ( TMap (μ m) b ・ ( TMap (η m) (FObj T b) ・ KMap f ) ) | |
| 453 ≡⟨⟩ | |
| 454 Sets [ FMap (U T {m}) k o Sets [ TMap (μ m) b o Sets [ TMap (η m) (FObj T b) o KMap f ] ] ] | |
| 455 ∎ | |
| 456 hom-left-commute2 : {a a' : Obj Sets} {b : Obj (Kleisli Sets T m)} {f : Hom (Kleisli Sets T m) (FObj (F T {m}) a) b} {h : Hom Sets a' a} → | |
| 457 (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap (Kleisli Sets T m [ f o FMap (F T {m}) h ]) x))) | |
| 458 ≡ (Sets [ (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap f x))) o h ]) | |
| 459 hom-left-commute2 {a} {a'} {b} {f} {h} = let open ≡-Reasoning in begin | |
| 460 TMap (μ m) b ・ (TMap (η m) (FObj T b) ・ (KMap (Kleisli Sets T m [ f o FMap (F T {m}) h ]))) | |
| 461 ≡⟨⟩ | |
| 462 TMap (μ m) b ・ (TMap (η m) (FObj T b) ・ ( (TMap (μ m) b ・ FMap T (KMap f) ) ・ ( TMap (η m) a ・ h ))) | |
| 463 ≡⟨ left Sets (IsMonad.unity1 ( isMonad m )) ⟩ | |
| 464 (TMap (μ m) b ・ FMap T (KMap f) ) ・ ( TMap (η m) a ・ h ) | |
| 465 ≡⟨ right Sets {_} {_} {_} {TMap (μ m) b} ( left Sets ( IsNTrans.commute ( isNTrans (η m) ))) ⟩ | |
| 466 TMap (μ m) b ・ (( TMap (η m) (FObj T b)・ KMap f ) ・ h ) | |
| 467 ∎ | |
| 468 | |
| 469 | |
| 470 | |
| 471 lemma← : ( U F : Functor Sets Sets ) → UnityOfOppsite Sets U F → Monad ( U ● F ) | |
| 472 lemma← U F uo = record { | |
| 473 η = η | |
| 474 ; μ = μ | |
| 475 ; isMonad = record { | |
| 476 unity1 = unity1 | |
| 477 ; unity2 = unity2 | |
| 478 ; assoc = assoc | |
| 479 } | |
| 480 } where | |
| 481 open UnityOfOppsite | |
| 482 T = U ● F | |
| 483 η-comm : {a b : Obj Sets} {f : Hom Sets a b} → Sets [ FMap (U ● F) f o (λ x → hom-left uo (λ x₁ → x₁) x) ] | |
| 484 ≡ Sets [ (λ x → hom-left uo (λ x₁ → x₁) x) o FMap (idFunctor {_} {Sets} ) f ] | |
| 485 η-comm {a} {b} {f} = let open ≡-Reasoning in begin | |
| 486 FMap (U ● F) f ・ (hom-left uo (λ x₁ → x₁) ) | |
| 487 ≡⟨ sym (hom-left-commute1 uo) ⟩ | |
| 488 hom-left uo ( FMap F f ・ (λ x₁ → x₁) ) | |
| 489 ≡⟨ hom-left-commute2 uo ⟩ | |
| 490 hom-left uo (λ x₁ → x₁) ・ FMap ( idFunctor {_} {Sets} ) f | |
| 491 ∎ | |
| 492 η : NTrans (idFunctor {_} {Sets}) T | |
| 493 η = record { TMap = λ a x → (hom-left uo) (λ x → x ) x ; isNTrans = record { commute = η-comm } } | |
| 494 μ-comm : {a b : Obj Sets} {f : Hom Sets a b} → (Sets [ FMap T f o (λ x → FMap U (hom-right uo (λ x₁ → x₁)) x) ]) | |
| 495 ≡ (Sets [ (λ x → FMap U (hom-right uo (λ x₁ → x₁)) x) o FMap (T ● T) f ]) | |
| 496 μ-comm {a} {b} {f} = let open ≡-Reasoning in begin | |
| 497 FMap T f ・ FMap U (hom-right uo (λ x₁ → x₁)) | |
| 498 ≡⟨⟩ | |
| 499 FMap U (FMap F f ) ・ FMap U (hom-right uo (λ x₁ → x₁)) | |
| 500 ≡⟨ sym ( IsFunctor.distr ( Functor.isFunctor U)) ⟩ | |
| 501 FMap U (FMap F f ・ hom-right uo (λ x₁ → x₁)) | |
| 502 ≡⟨ cong ( λ z → FMap U z ) (hom-right-commute1 uo) ⟩ | |
| 503 FMap U ( hom-right uo (FMap U (FMap F f) ・ (λ x₁ → x₁) ) ) | |
| 504 ≡⟨ sym ( cong ( λ z → FMap U z ) (hom-right-commute2 uo)) ⟩ | |
| 505 FMap U ((hom-right uo (λ x₁ → x₁)) ・ (FMap F (FMap U (FMap F f )))) | |
| 506 ≡⟨ IsFunctor.distr ( Functor.isFunctor U) ⟩ | |
| 507 FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap U (FMap F (FMap U (FMap F f ))) | |
| 508 ≡⟨⟩ | |
| 509 FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap (T ● T) f | |
| 510 ∎ | |
| 511 μ : NTrans (T ● T) T | |
| 512 μ = record { TMap = λ a x → FMap U ( hom-right uo (λ x → x)) x ; isNTrans = record { commute = μ-comm } } | |
| 513 unity1 : {a : Obj Sets} → (Sets [ TMap μ a o TMap η (FObj (U ● F) a) ]) ≡ id Sets (FObj (U ● F) a) | |
| 514 unity1 {a} = let open ≡-Reasoning in begin | |
| 515 TMap μ a ・ TMap η (FObj (U ● F) a) | |
| 516 ≡⟨⟩ | |
| 517 FMap U (hom-right uo (λ x₁ → x₁)) ・ hom-left uo (λ x₁ → x₁) | |
| 518 ≡⟨ sym (hom-left-commute1 uo ) ⟩ | |
| 519 hom-left uo ( hom-right uo (λ x₁ → x₁) ・ (λ x₁ → x₁) ) | |
| 520 ≡⟨ hom-right-injective uo ⟩ | |
| 521 id Sets (FObj (U ● F) a) | |
| 522 ∎ | |
| 523 unity2 : {a : Obj Sets} → (Sets [ TMap μ a o FMap (U ● F) (TMap η a) ]) ≡ id Sets (FObj (U ● F) a) | |
| 524 unity2 {a} = let open ≡-Reasoning in begin | |
| 525 TMap μ a ・ FMap (U ● F) (TMap η a) | |
| 526 ≡⟨⟩ | |
| 527 FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap U (FMap F (hom-left uo (λ x₁ → x₁))) | |
| 528 ≡⟨ sym ( IsFunctor.distr (isFunctor U)) ⟩ | |
| 529 FMap U (hom-right uo (λ x₁ → x₁) ・ FMap F (hom-left uo (λ x₁ → x₁))) | |
| 530 ≡⟨ cong ( λ z → FMap U z ) (hom-right-commute2 uo) ⟩ | |
| 531 FMap U (hom-right uo ((λ x₁ → x₁) ・ hom-left uo (λ x₁ → x₁) )) | |
| 532 ≡⟨ cong ( λ z → FMap U z ) (hom-left-injective uo) ⟩ | |
| 533 FMap U ( id Sets (FObj F a) ) | |
| 534 ≡⟨ IsFunctor.identity (isFunctor U) ⟩ | |
| 535 id Sets (FObj (U ● F) a) | |
| 536 ∎ | |
| 537 assoc : {a : Obj Sets} → (Sets [ TMap μ a o TMap μ (FObj (U ● F) a) ]) ≡ (Sets [ TMap μ a o FMap (U ● F) (TMap μ a) ]) | |
| 538 assoc {a} = let open ≡-Reasoning in begin | |
| 539 TMap μ a ・ TMap μ (FObj (U ● F) a) | |
| 540 ≡⟨⟩ | |
| 541 FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap U (hom-right uo (λ x₁ → x₁)) | |
| 542 ≡⟨ sym ( IsFunctor.distr (isFunctor U )) ⟩ | |
| 543 FMap U (hom-right uo (λ x₁ → x₁) ・ hom-right uo (λ x₁ → x₁)) | |
| 544 ≡⟨ cong ( λ z → FMap U z ) ( hom-right-commute1 uo ) ⟩ | |
| 545 FMap U (hom-right uo ((λ x₁ → x₁) ・ FMap U (hom-right uo (λ x₁ → x₁))) ) | |
| 546 ≡⟨ sym ( cong ( λ z → FMap U z ) ( hom-right-commute2 uo ) ) ⟩ | |
| 547 FMap U (hom-right uo (λ x₁ → x₁) ・ FMap F (FMap U (hom-right uo (λ x₁ → x₁)))) | |
| 548 ≡⟨ IsFunctor.distr (isFunctor U ) ⟩ | |
| 549 FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap U (FMap F (FMap U (hom-right uo (λ x₁ → x₁)))) | |
| 550 ≡⟨⟩ | |
| 551 TMap μ a ・ FMap (U ● F) (TMap μ a) | |
| 552 ∎ | |
| 553 | |
| 554 | |
| 555 | |
| 556 | |
| 557 | |
| 558 |