Mercurial > hg > Members > kono > Proof > category
changeset 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 | 60942538dc41 |
| children | 06a7831cf6ce |
| files | stdalone-kleisli.agda |
| diffstat | 1 files changed, 558 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/stdalone-kleisli.agda Wed Jun 13 12:56:38 2018 +0900 @@ -0,0 +1,558 @@ +module stdalone-kleisli where + +open import Level +open import Relation.Binary +open import Relation.Binary.Core + +-- h g f +-- a ---→ b ---→ c ---→ d +-- + +record IsCategory {l : Level} ( Obj : Set (suc l) ) (Hom : Obj → Obj → Set l ) + ( _o_ : { a b c : Obj } → Hom b c → Hom a b → Hom a c ) + ( id : ( a : Obj ) → Hom a a ) + : Set (suc l) where + field + idL : { a b : Obj } { f : Hom a b } → ( id b o f ) ≡ f + idR : { a b : Obj } { f : Hom a b } → ( f o id a ) ≡ f + 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 + +record Category {l : Level} : Set (suc (suc l)) where + field + Obj : Set (suc l) + Hom : Obj → Obj → Set l + _o_ : { a b c : Obj } → Hom b c → Hom a b → Hom a c + id : ( a : Obj ) → Hom a a + isCategory : IsCategory Obj Hom _o_ id + +Sets : Category +Sets = record { + Obj = Set + ; Hom = λ a b → a → b + ; _o_ = λ f g x → f ( g x ) + ; id = λ A x → x + ; isCategory = record { + idL = refl + ; idR = refl + ; assoc = refl + } + } + + +open Category + +_[_o_] : {l : Level} (C : Category {l} ) → {a b c : Obj C} → Hom C b c → Hom C a b → Hom C a c +C [ f o g ] = Category._o_ C f g + +-- +-- f g +-- a ----→ b -----→ c +-- | | | +-- T| T| T| +-- | | | +-- v v v +-- Ta ----→ Tb ----→ Tc +-- Tf Tg + + +record IsFunctor {l : Level} (C D : Category {l} ) + (FObj : Obj C → Obj D) + (FMap : {A B : Obj C} → Hom C A B → Hom D (FObj A) (FObj B)) + : Set (suc l ) where + field + identity : {A : Obj C} → FMap (id C A) ≡ id D (FObj A) + distr : {a b c : Obj C} {f : Hom C a b} {g : Hom C b c} + → FMap ( C [ g o f ]) ≡ (D [ FMap g o FMap f ] ) + +record Functor {l : Level} (domain codomain : Category {l} ) + : Set (suc l) where + field + FObj : Obj domain → Obj codomain + FMap : {A B : Obj domain} → Hom domain A B → Hom codomain (FObj A) (FObj B) + isFunctor : IsFunctor domain codomain FObj FMap + +open Functor + +idFunctor : {l : Level } { C : Category {l} } → Functor C C +idFunctor = record { + FObj = λ x → x + ; FMap = λ f → f + ; isFunctor = record { + identity = refl + ; distr = refl + } + } + +open import Relation.Binary.PropositionalEquality hiding ( [_] ) + + +_●_ : {l : Level} { A B C : Category {l} } → ( S : Functor B C ) ( T : Functor A B ) → Functor A C +_●_ {l} {A} {B} {C} S T = record { + FObj = λ x → FObj S ( FObj T x ) + ; FMap = λ f → FMap S ( FMap T f ) + ; isFunctor = record { + identity = λ {a} → identity a + ; distr = λ {a} {b} {c} {f} {g} → distr + } + } where + identity : (a : Obj A) → FMap S (FMap T (id A a)) ≡ id C (FObj S (FObj T a)) + identity a = let open ≡-Reasoning in begin + FMap S (FMap T (id A a)) + ≡⟨ cong ( λ z → FMap S z ) ( IsFunctor.identity (isFunctor T ) ) ⟩ + FMap S (id B (FObj T a) ) + ≡⟨ IsFunctor.identity (isFunctor S ) ⟩ + id C (FObj S (FObj T a)) + ∎ + 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) ]) + distr {a} {b} {c} {f} {g} = let open ≡-Reasoning in begin + FMap S (FMap T (A [ g o f ])) + ≡⟨ cong ( λ z → FMap S z ) ( IsFunctor.distr (isFunctor T ) ) ⟩ + FMap S ( B [ FMap T g o FMap T f ] ) + ≡⟨ IsFunctor.distr (isFunctor S ) ⟩ + C [ FMap S (FMap T g) o FMap S (FMap T f) ] + ∎ + + +-- {A : Set c₁ } {B : Set c₂ } → { f g : A → B } → f x ≡ g x → f ≡ g +postulate extensionality : { c₁ c₂ : Level} → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ + +-- +-- t a +-- F a -----→ G a +-- | | +-- Ff | | Gf +-- v v +-- F b ------→ G b +-- t b +-- + +record IsNTrans { l : Level } (D C : Category {l} ) ( F G : Functor D C ) + (TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A)) + : Set (suc l) where + field + commute : {a b : Obj D} {f : Hom D a b} + → C [ ( FMap G f ) o ( TMap a ) ] ≡ C [ (TMap b ) o (FMap F f) ] + +record NTrans {l : Level} {domain codomain : Category {l} } (F G : Functor domain codomain ) + : Set (suc l) where + field + TMap : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A) + isNTrans : IsNTrans domain codomain F G TMap + + + +open NTrans + +-- +-- +-- η : 1 ------→ T +-- μ : TT -----→ T +-- +-- η μT +-- T -----→ TT TTT ------→ TT +-- | | | | +-- Tη | |μ Tμ | |Tμ +-- v | v v +-- TT -----→ T TT -------→ T +-- μ μT + + +record IsMonad {l : Level} { C : Category {l} } (T : Functor C C) ( η : NTrans idFunctor T ) ( μ : NTrans (T ● T) T ) + : Set (suc l) where + field + assoc : {a : Obj C} → C [ TMap μ a o TMap μ ( FObj T a ) ] ≡ C [ TMap μ a o FMap T (TMap μ a) ] + unity1 : {a : Obj C} → C [ TMap μ a o TMap η ( FObj T a ) ] ≡ id C (FObj T a) + unity2 : {a : Obj C} → C [ TMap μ a o (FMap T (TMap η a ))] ≡ id C (FObj T a) + + +record Monad {l : Level} { C : Category {l} } (T : Functor C C) : Set (suc l) where + field + η : NTrans idFunctor T + μ : NTrans (T ● T) T + isMonad : IsMonad T η μ + +record KleisliHom { c : Level} { A : Category {c} } { T : Functor A A } (a : Obj A) (b : Obj A) + : Set c where + field + KMap : Hom A a ( FObj T b ) + +open KleisliHom + + +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 ] +left {l} C {a} {b} {c} {f} {f'} {g} refl = cong ( λ z → C [ z o g ] ) refl + +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' ] +right {l} C {a} {b} {c} {f} {g} {g'} refl = cong ( λ z → C [ f o z ] ) refl + +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 } + → C [ f o C [ g o h ] ] ≡ C [ C [ f o g ] o h ] +Assoc {l} C = IsCategory.assoc ( isCategory C ) + + +Kleisli : {l : Level} (C : Category {l} ) (T : Functor C C ) ( M : Monad T ) → Category {l} +Kleisli C T M = record { + Obj = Obj C + ; Hom = λ a b → KleisliHom {_} {C} {T} a b + ; _o_ = λ {a} {b} {c} f g → join {a} {b} {c} f g + ; id = λ a → record { KMap = TMap (Monad.η M) a } + ; isCategory = record { + idL = idL + ; idR = idR + ; assoc = assoc + } + } where + join : { a b c : Obj C } → KleisliHom b c → KleisliHom a b → KleisliHom a c + join {a} {b} {c} f g = record { KMap = ( C [ TMap (Monad.μ M) c o C [ FMap T ( KMap f ) o KMap g ] ] ) } + idL : {a b : Obj C} {f : KleisliHom a b} → join (record { KMap = TMap (Monad.η M) b }) f ≡ f + idL {a} {b} {f} = let open ≡-Reasoning in begin + record { KMap = C [ TMap (Monad.μ M) b o C [ FMap T (TMap (Monad.η M) b) o KMap f ] ] } + ≡⟨ cong ( λ z → record { KMap = z } ) ( begin + C [ TMap (Monad.μ M) b o C [ FMap T (TMap (Monad.η M) b) o KMap f ] ] + ≡⟨ IsCategory.assoc ( isCategory C ) ⟩ + C [ C [ TMap (Monad.μ M) b o FMap T (TMap (Monad.η M) b) ] o KMap f ] + ≡⟨ cong ( λ z → C [ z o KMap f ] ) ( IsMonad.unity2 (Monad.isMonad M ) ) ⟩ + C [ id C (FObj T b) o KMap f ] + ≡⟨ IsCategory.idL ( isCategory C ) ⟩ + KMap f + ∎ ) ⟩ + record { KMap = KMap f } + ∎ + idR : {a b : Obj C} {f : KleisliHom a b} → join f (record { KMap = TMap (Monad.η M) a }) ≡ f + idR {a} {b} {f} = let open ≡-Reasoning in begin + record { KMap = C [ TMap (Monad.μ M) b o C [ FMap T (KMap f) o TMap (Monad.η M) a ] ] } + ≡⟨ cong ( λ z → record { KMap = z } ) ( begin + C [ TMap (Monad.μ M) b o C [ FMap T (KMap f) o TMap (Monad.η M) a ] ] + ≡⟨ cong ( λ z → C [ TMap (Monad.μ M) b o z ] ) ( IsNTrans.commute (isNTrans (Monad.η M) )) ⟩ + C [ TMap (Monad.μ M) b o C [ TMap (Monad.η M) (FObj T b) o KMap f ] ] + ≡⟨ IsCategory.assoc ( isCategory C ) ⟩ + C [ C [ TMap (Monad.μ M) b o TMap (Monad.η M) (FObj T b) ] o KMap f ] + ≡⟨ cong ( λ z → C [ z o KMap f ] ) ( IsMonad.unity1 (Monad.isMonad M ) ) ⟩ + C [ id C (FObj T b) o KMap f ] + ≡⟨ IsCategory.idL ( isCategory C ) ⟩ + KMap f + ∎ ) ⟩ + record { KMap = KMap f } + ∎ + -- + -- TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ ( TMap (Monad.μ M) c ・ ( FMap T (KMap g) ・ KMap h ) ) ) ) + -- + -- h T g μ c + -- a ---→ T b -----------------→ T T c -------------------------→ T c + -- | | | + -- | | | + -- | | T T f NAT μ | T f + -- | | | + -- | v μ (T d) v + -- | distr T T T T d -------------------------→ T T d + -- | | | + -- | | | + -- | | T μ d Monad-assoc | μ d + -- | | | + -- | v v + -- +------------------→ T T d -------------------------→ T d + -- T (μ d・T f・g) μ d + -- + -- TMap (Monad.μ M) d ・ ( FMap T (( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ KMap g ) ) ) ・ KMap h ) ) + -- + _・_ : {a b c : Obj C } ( f : Hom C b c ) ( g : Hom C a b ) → Hom C a c + f ・ g = C [ f o g ] + 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 + assoc {a} {b} {c} {d} {f} {g} {h} = let open ≡-Reasoning in begin + join f (join g h) + ≡⟨⟩ + record { KMap = TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ ( TMap (Monad.μ M) c ・ ( FMap T (KMap g) ・ KMap h ))) } + ≡⟨ cong ( λ z → record { KMap = z } ) ( begin + ( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ ( TMap (Monad.μ M) c ・ ( FMap T (KMap g) ・ KMap h ) ) ) ) + ≡⟨ right C ( right C (Assoc C)) ⟩ + ( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ ( ( TMap (Monad.μ M) c ・ FMap T (KMap g) ) ・ KMap h ) ) ) + ≡⟨ Assoc C ⟩ + ( ( TMap (Monad.μ M) d ・ FMap T (KMap f) ) ・ ( ( TMap (Monad.μ M) c ・ FMap T (KMap g) ) ・ KMap h ) ) + ≡⟨ Assoc C ⟩ + ( ( ( TMap (Monad.μ M) d ・ FMap T (KMap f) ) ・ ( TMap (Monad.μ M) c ・ FMap T (KMap g) ) ) ・ KMap h ) + ≡⟨ sym ( left C (Assoc C )) ⟩ + ( ( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ ( TMap (Monad.μ M) c ・ FMap T (KMap g) ) ) ) ・ KMap h ) + ≡⟨ left C ( right C (Assoc C)) ⟩ + ( ( TMap (Monad.μ M) d ・ ( ( FMap T (KMap f) ・ TMap (Monad.μ M) c ) ・ FMap T (KMap g) ) ) ・ KMap h ) + ≡⟨ left C (Assoc C)⟩ + ( ( ( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ TMap (Monad.μ M) c ) ) ・ FMap T (KMap g) ) ・ KMap h ) + ≡⟨ left C ( left C ( right C ( IsNTrans.commute (isNTrans (Monad.μ M) ) ) )) ⟩ + ( ( ( TMap (Monad.μ M) d ・ ( TMap (Monad.μ M) (FObj T d) ・ FMap (T ● T) (KMap f) ) ) ・ FMap T (KMap g) ) ・ KMap h ) + ≡⟨ sym ( left C (Assoc C)) ⟩ + ( ( TMap (Monad.μ M) d ・ ( ( TMap (Monad.μ M) (FObj T d) ・ FMap (T ● T) (KMap f) ) ・ FMap T (KMap g) ) ) ・ KMap h ) + ≡⟨ sym ( left C ( right C (Assoc C))) ⟩ + ( ( TMap (Monad.μ M) d ・ ( TMap (Monad.μ M) (FObj T d) ・ ( FMap (T ● T) (KMap f) ・ FMap T (KMap g) ) ) ) ・ KMap h ) + ≡⟨ sym ( left C ( right C (right C (IsFunctor.distr (isFunctor T ) ) ) )) ⟩ + ( ( TMap (Monad.μ M) d ・ ( TMap (Monad.μ M) (FObj T d) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ) ・ KMap h ) + ≡⟨ left C (Assoc C) ⟩ + ( ( ( TMap (Monad.μ M) d ・ TMap (Monad.μ M) (FObj T d) ) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ・ KMap h ) + ≡⟨ left C (left C ( IsMonad.assoc (Monad.isMonad M ) ) ) ⟩ + ( ( ( TMap (Monad.μ M) d ・ FMap T (TMap (Monad.μ M) d) ) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ・ KMap h ) + ≡⟨ sym ( left C (Assoc C)) ⟩ + ( ( TMap (Monad.μ M) d ・ ( FMap T (TMap (Monad.μ M) d) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ) ・ KMap h ) + ≡⟨ sym (Assoc C) ⟩ + ( TMap (Monad.μ M) d ・ ( ( FMap T (TMap (Monad.μ M) d) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ・ KMap h ) ) + ≡⟨ sym (right C ( left C (IsFunctor.distr (isFunctor T )))) ⟩ + ( TMap (Monad.μ M) d ・ ( FMap T (( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ KMap g ) ) ) ・ KMap h ) ) + ∎ ) ⟩ + record { KMap = ( TMap (Monad.μ M) d ・ ( FMap T (( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ KMap g ) ) ) ・ KMap h ) ) } + ≡⟨⟩ + join (join f g) h + ∎ + +-- +-- U : Kleisli Sets +-- F : Sets Kleisli +-- +-- Hom Klei a b ←---→ Hom Sets a (U●F b ) +-- +-- Hom Klei (F a) (F b) ←---→ Hom Sets a (U●F b ) +-- +-- Hom Klei (F a) b ←---→ Hom Sets a U(b) Hom Klei (F a) b ←---→ Hom Sets a U(b) +-- | | | | +-- Ff| f| |f |Uf +-- | | | | +-- ↓ ↓ ↓ ↓ +-- Hom Klei (F (f a)) b ←---→ Hom Sets (f a) U(b) Hom Klei (F a) (f b) ←---→ Hom Sets a U(f b) +-- +-- + +record UnityOfOppsite ( Kleisli : Category ) ( U : Functor Kleisli Sets ) ( F : Functor Sets Kleisli ) : Set (suc zero) where + field + hom-right : {a : Obj Sets} { b : Obj Kleisli } → Hom Sets a ( FObj U b ) → Hom Kleisli (FObj F a) b + hom-left : {a : Obj Sets} { b : Obj Kleisli } → Hom Kleisli (FObj F a) b → Hom Sets a ( FObj U b ) + hom-right-injective : {a : Obj Sets} { b : Obj Kleisli } → {f : Hom Sets a (FObj U b) } → hom-left ( hom-right f ) ≡ f + hom-left-injective : {a : Obj Sets} { b : Obj Kleisli } → {f : Hom Kleisli (FObj F a) b } → hom-right ( hom-left f ) ≡ f + --- naturality of Φ + hom-left-commute1 : {a : Obj Sets} {b b' : Obj Kleisli } → + { f : Hom Kleisli (FObj F a) b } → { k : Hom Kleisli b b' } → + hom-left ( Kleisli [ k o f ] ) ≡ Sets [ FMap U k o hom-left f ] + hom-left-commute2 : {a a' : Obj Sets} {b : Obj Kleisli } → + { f : Hom Kleisli (FObj F a) b } → { h : Hom Sets a' a } → + hom-left ( Kleisli [ f o FMap F h ] ) ≡ Sets [ hom-left f o h ] + hom-right-commute1 : {a : Obj Sets} {b b' : Obj Kleisli } → + { g : Hom Sets a (FObj U b)} → { k : Hom Kleisli b b' } → + Kleisli [ k o hom-right g ] ≡ hom-right ( Sets [ FMap U k o g ] ) + hom-right-commute1 {a} {b} {b'} {g} {k} = let open ≡-Reasoning in begin + Kleisli [ k o hom-right g ] + ≡⟨ sym hom-left-injective ⟩ + hom-right ( hom-left ( Kleisli [ k o hom-right g ] ) ) + ≡⟨ cong ( λ z → hom-right z ) hom-left-commute1 ⟩ + hom-right (Sets [ FMap U k o hom-left (hom-right g) ]) + ≡⟨ cong ( λ z → hom-right ( Sets [ FMap U k o z ] )) hom-right-injective ⟩ + hom-right ( Sets [ FMap U k o g ] ) + ∎ + hom-right-commute2 : {a a' : Obj Sets} {b : Obj Kleisli } → + { g : Hom Sets a (FObj U b) } → { h : Hom Sets a' a } → + Kleisli [ hom-right g o FMap F h ] ≡ hom-right ( Sets [ g o h ] ) + hom-right-commute2 {a} {a'} {b} {g} {h} = let open ≡-Reasoning in begin + Kleisli [ hom-right g o FMap F h ] + ≡⟨ sym hom-left-injective ⟩ + hom-right (hom-left (Kleisli [ hom-right g o FMap F h ])) + ≡⟨ cong ( λ z → hom-right z ) hom-left-commute2 ⟩ + hom-right (Sets [ hom-left (hom-right g) o h ]) + ≡⟨ cong ( λ z → hom-right ( Sets [ z o h ] )) hom-right-injective ⟩ + hom-right (Sets [ g o h ]) + ∎ + + + + +_・_ : {a b c : Obj Sets } ( f : Hom Sets b c ) ( g : Hom Sets a b ) → Hom Sets a c +f ・ g = Sets [ f o g ] + +U : ( T : Functor Sets Sets ) → { m : Monad T } → Functor (Kleisli Sets T m) Sets +U T {m} = record { + FObj = FObj T + ; FMap = λ {a} {b} f x → TMap ( μ m ) b ( FMap T ( KMap f ) x ) + ; isFunctor = record { identity = IsMonad.unity2 (isMonad m) ; distr = distr } + } where + open Monad + 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} → + (λ x → TMap (μ m) c (FMap T (KMap (Kleisli Sets T m [ g o f ])) x)) + ≡ (Sets [ (λ x → TMap (μ m) c (FMap T (KMap g) x)) o (λ x → TMap (μ m) b (FMap T (KMap f) x)) ]) + distr {a} {b} {c} {f} {g} = let open ≡-Reasoning in begin + Sets [ TMap (μ m) c o FMap T (KMap (Kleisli Sets T m [ g o f ])) ] + ≡⟨⟩ + Sets [ TMap (μ m) c o FMap T ( Sets [ TMap (μ m) c o Sets [ FMap T ( KMap g ) o KMap f ] ] ) ] + ≡⟨ right Sets {_} {_} {_} {TMap (μ m) c} {_} {_} ( IsFunctor.distr (Functor.isFunctor T) ) ⟩ + Sets [ TMap (μ m) c o Sets [ FMap T ( TMap (μ m) c) o FMap T ( Sets [ FMap T (KMap g) o KMap f ] ) ] ] + ≡⟨ sym ( left Sets (IsMonad.assoc (isMonad m ))) ⟩ + Sets [ Sets [ TMap (μ m) c o TMap (μ m) (FObj T c) ] o (FMap T (Sets [ FMap T (KMap g) o KMap f ])) ] + ≡⟨ right Sets {_} {_} {_} {TMap (μ m) c} ( right Sets {_} {_} {_} {TMap (μ m) (FObj T c)} ( IsFunctor.distr (Functor.isFunctor T) ) ) ⟩ + Sets [ Sets [ TMap (μ m) c o TMap (μ m) (FObj T c) ] o Sets [ FMap T ( FMap T (KMap g)) o FMap T ( KMap f ) ] ] + ≡⟨ sym ( right Sets {_} {_} {_} {TMap (μ m) c} ( left Sets (IsNTrans.commute ( NTrans.isNTrans (μ m))))) ⟩ + Sets [ Sets [ TMap (μ m) c o FMap T (KMap g) ] o Sets [ TMap (μ m) b o FMap T (KMap f) ] ] + ∎ + + +F : ( T : Functor Sets Sets ) → {m : Monad T} → Functor Sets ( Kleisli Sets T m) +F T {m} = record { + FObj = λ a → a ; FMap = λ {a} {b} f → record { KMap = λ x → TMap (η m) b (f x) } + ; isFunctor = record { identity = refl ; distr = distr } + } where + open Monad + 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) } ≡ + Kleisli Sets T m [ record { KMap = λ x → TMap (η m) c (g x) } o record { KMap = λ x → TMap (η m) b (f x) } ] + distr {a} {b} {c} {f} {g} = let open ≡-Reasoning in ( cong ( λ z → record { KMap = z } ) ( begin + Sets [ TMap (η m) c o Sets [ g o f ] ] + ≡⟨ left Sets {_} {_} {_} {Sets [ TMap (η m) c o g ] } ( sym ( IsNTrans.commute ( NTrans.isNTrans (η m) ) )) ⟩ + Sets [ Sets [ FMap T g o TMap (η m) b ] o f ] + ≡⟨ sym ( IsCategory.idL ( Category.isCategory Sets )) ⟩ + Sets [ ( λ x → x ) o Sets [ Sets [ FMap T g o TMap (η m) b ] o f ] ] + ≡⟨ sym ( left Sets (IsMonad.unity2 (isMonad m ))) ⟩ + Sets [ Sets [ TMap (μ m) c o FMap T (TMap (η m) c) ] o Sets [ FMap T g o Sets [ TMap (η m) b o f ] ] ] + ≡⟨ sym ( right Sets {_} {_} {_} {TMap (μ m) c} {_} ( left Sets {_} {_} {_} { FMap T (Sets [ TMap (η m) c o g ] )} ( IsFunctor.distr (Functor.isFunctor T) ))) ⟩ + Sets [ TMap (μ m) c o ( Sets [ FMap T (Sets [ TMap (η m) c o g ] ) o Sets [ TMap (η m) b o f ] ] ) ] + ∎ )) + +-- +-- Hom Sets a (FObj U b) = Hom Sets a (T b) +-- Hom Kleisli (FObj F a) b = Hom Sets a (T b) +-- + +lemma→ : ( T : Functor Sets Sets ) → (m : Monad T ) → UnityOfOppsite (Kleisli Sets T m) (U T {m} ) (F T {m}) +lemma→ T m = + let open Monad in + record { + hom-right = λ {a} {b} f → record { KMap = f } + ; hom-left = λ {a} {b} f x → TMap (μ m) b ( TMap ( η m ) (FObj T b) ( (KMap f) x ) ) + ; hom-right-injective = hom-right-injective + ; hom-left-injective = hom-left-injective + ; hom-left-commute1 = hom-left-commute1 + ; hom-left-commute2 = hom-left-commute2 + } where + open Monad + hom-right-injective : {a : Obj Sets} {b : Obj (Kleisli Sets T m)} + {f : Hom Sets a (FObj (U T {m}) b)} → (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (f x))) ≡ f + hom-right-injective {a} {b} {f} = let open ≡-Reasoning in begin + Sets [ TMap (μ m) b o Sets [ TMap (η m) (FObj T b) o f ] ] + ≡⟨ left Sets ( IsMonad.unity1 ( isMonad m ) ) ⟩ + Sets [ id Sets (FObj (U T {m}) b) o f ] + ≡⟨ IsCategory.idL ( isCategory Sets ) ⟩ + f + ∎ + hom-left-injective : {a : Obj Sets} {b : Obj (Kleisli Sets T m)} {f : Hom (Kleisli Sets T m) (FObj (F T {m}) a) b} + → record { KMap = λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap f x)) } ≡ f + hom-left-injective {a} {b} {f} = let open ≡-Reasoning in cong ( λ z → record { KMap = z } ) ( begin + Sets [ TMap (μ m) b o Sets [ TMap (η m) (FObj T b) o KMap f ] ] + ≡⟨ left Sets ( IsMonad.unity1 ( isMonad m ) ) ⟩ + KMap f + ∎ ) + 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'} → + (λ x → TMap (μ m) b' (TMap (η m) (FObj T b') (KMap (Kleisli Sets T m [ k o f ]) x))) + ≡ (Sets [ FMap (U T {m}) k o (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap f x))) ]) + hom-left-commute1 {a} {b} {b'} {f} {k} = let open ≡-Reasoning in begin + Sets [ TMap (μ m) b' o Sets [ TMap (η m) (FObj T b') o KMap (Kleisli Sets T m [ k o f ] ) ] ] + ≡⟨⟩ + TMap (μ m) b' ・ ( TMap (η m) (FObj T b') ・ ( TMap (μ m) b' ・ ( FMap T (KMap k) ・ KMap f ))) + ≡⟨ left Sets ( IsMonad.unity1 ( isMonad m )) ⟩ + TMap (μ m) b' ・ ( FMap T (KMap k) ・ KMap f ) + ≡⟨ right Sets {_} {_} {_} {TMap ( μ m ) b' ・ FMap T ( KMap k )} ( left Sets ( sym ( IsMonad.unity1 ( isMonad m ) ) ) ) ⟩ + ( TMap ( μ m ) b' ・ FMap T ( KMap k ) ) ・ ( TMap (μ m) b ・ ( TMap (η m) (FObj T b) ・ KMap f ) ) + ≡⟨⟩ + Sets [ FMap (U T {m}) k o Sets [ TMap (μ m) b o Sets [ TMap (η m) (FObj T b) o KMap f ] ] ] + ∎ + 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} → + (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap (Kleisli Sets T m [ f o FMap (F T {m}) h ]) x))) + ≡ (Sets [ (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap f x))) o h ]) + hom-left-commute2 {a} {a'} {b} {f} {h} = let open ≡-Reasoning in begin + TMap (μ m) b ・ (TMap (η m) (FObj T b) ・ (KMap (Kleisli Sets T m [ f o FMap (F T {m}) h ]))) + ≡⟨⟩ + TMap (μ m) b ・ (TMap (η m) (FObj T b) ・ ( (TMap (μ m) b ・ FMap T (KMap f) ) ・ ( TMap (η m) a ・ h ))) + ≡⟨ left Sets (IsMonad.unity1 ( isMonad m )) ⟩ + (TMap (μ m) b ・ FMap T (KMap f) ) ・ ( TMap (η m) a ・ h ) + ≡⟨ right Sets {_} {_} {_} {TMap (μ m) b} ( left Sets ( IsNTrans.commute ( isNTrans (η m) ))) ⟩ + TMap (μ m) b ・ (( TMap (η m) (FObj T b)・ KMap f ) ・ h ) + ∎ + + + +lemma← : ( U F : Functor Sets Sets ) → UnityOfOppsite Sets U F → Monad ( U ● F ) +lemma← U F uo = record { + η = η + ; μ = μ + ; isMonad = record { + unity1 = unity1 + ; unity2 = unity2 + ; assoc = assoc + } + } where + open UnityOfOppsite + T = U ● F + η-comm : {a b : Obj Sets} {f : Hom Sets a b} → Sets [ FMap (U ● F) f o (λ x → hom-left uo (λ x₁ → x₁) x) ] + ≡ Sets [ (λ x → hom-left uo (λ x₁ → x₁) x) o FMap (idFunctor {_} {Sets} ) f ] + η-comm {a} {b} {f} = let open ≡-Reasoning in begin + FMap (U ● F) f ・ (hom-left uo (λ x₁ → x₁) ) + ≡⟨ sym (hom-left-commute1 uo) ⟩ + hom-left uo ( FMap F f ・ (λ x₁ → x₁) ) + ≡⟨ hom-left-commute2 uo ⟩ + hom-left uo (λ x₁ → x₁) ・ FMap ( idFunctor {_} {Sets} ) f + ∎ + η : NTrans (idFunctor {_} {Sets}) T + η = record { TMap = λ a x → (hom-left uo) (λ x → x ) x ; isNTrans = record { commute = η-comm } } + μ-comm : {a b : Obj Sets} {f : Hom Sets a b} → (Sets [ FMap T f o (λ x → FMap U (hom-right uo (λ x₁ → x₁)) x) ]) + ≡ (Sets [ (λ x → FMap U (hom-right uo (λ x₁ → x₁)) x) o FMap (T ● T) f ]) + μ-comm {a} {b} {f} = let open ≡-Reasoning in begin + FMap T f ・ FMap U (hom-right uo (λ x₁ → x₁)) + ≡⟨⟩ + FMap U (FMap F f ) ・ FMap U (hom-right uo (λ x₁ → x₁)) + ≡⟨ sym ( IsFunctor.distr ( Functor.isFunctor U)) ⟩ + FMap U (FMap F f ・ hom-right uo (λ x₁ → x₁)) + ≡⟨ cong ( λ z → FMap U z ) (hom-right-commute1 uo) ⟩ + FMap U ( hom-right uo (FMap U (FMap F f) ・ (λ x₁ → x₁) ) ) + ≡⟨ sym ( cong ( λ z → FMap U z ) (hom-right-commute2 uo)) ⟩ + FMap U ((hom-right uo (λ x₁ → x₁)) ・ (FMap F (FMap U (FMap F f )))) + ≡⟨ IsFunctor.distr ( Functor.isFunctor U) ⟩ + FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap U (FMap F (FMap U (FMap F f ))) + ≡⟨⟩ + FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap (T ● T) f + ∎ + μ : NTrans (T ● T) T + μ = record { TMap = λ a x → FMap U ( hom-right uo (λ x → x)) x ; isNTrans = record { commute = μ-comm } } + unity1 : {a : Obj Sets} → (Sets [ TMap μ a o TMap η (FObj (U ● F) a) ]) ≡ id Sets (FObj (U ● F) a) + unity1 {a} = let open ≡-Reasoning in begin + TMap μ a ・ TMap η (FObj (U ● F) a) + ≡⟨⟩ + FMap U (hom-right uo (λ x₁ → x₁)) ・ hom-left uo (λ x₁ → x₁) + ≡⟨ sym (hom-left-commute1 uo ) ⟩ + hom-left uo ( hom-right uo (λ x₁ → x₁) ・ (λ x₁ → x₁) ) + ≡⟨ hom-right-injective uo ⟩ + id Sets (FObj (U ● F) a) + ∎ + unity2 : {a : Obj Sets} → (Sets [ TMap μ a o FMap (U ● F) (TMap η a) ]) ≡ id Sets (FObj (U ● F) a) + unity2 {a} = let open ≡-Reasoning in begin + TMap μ a ・ FMap (U ● F) (TMap η a) + ≡⟨⟩ + FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap U (FMap F (hom-left uo (λ x₁ → x₁))) + ≡⟨ sym ( IsFunctor.distr (isFunctor U)) ⟩ + FMap U (hom-right uo (λ x₁ → x₁) ・ FMap F (hom-left uo (λ x₁ → x₁))) + ≡⟨ cong ( λ z → FMap U z ) (hom-right-commute2 uo) ⟩ + FMap U (hom-right uo ((λ x₁ → x₁) ・ hom-left uo (λ x₁ → x₁) )) + ≡⟨ cong ( λ z → FMap U z ) (hom-left-injective uo) ⟩ + FMap U ( id Sets (FObj F a) ) + ≡⟨ IsFunctor.identity (isFunctor U) ⟩ + id Sets (FObj (U ● F) a) + ∎ + assoc : {a : Obj Sets} → (Sets [ TMap μ a o TMap μ (FObj (U ● F) a) ]) ≡ (Sets [ TMap μ a o FMap (U ● F) (TMap μ a) ]) + assoc {a} = let open ≡-Reasoning in begin + TMap μ a ・ TMap μ (FObj (U ● F) a) + ≡⟨⟩ + FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap U (hom-right uo (λ x₁ → x₁)) + ≡⟨ sym ( IsFunctor.distr (isFunctor U )) ⟩ + FMap U (hom-right uo (λ x₁ → x₁) ・ hom-right uo (λ x₁ → x₁)) + ≡⟨ cong ( λ z → FMap U z ) ( hom-right-commute1 uo ) ⟩ + FMap U (hom-right uo ((λ x₁ → x₁) ・ FMap U (hom-right uo (λ x₁ → x₁))) ) + ≡⟨ sym ( cong ( λ z → FMap U z ) ( hom-right-commute2 uo ) ) ⟩ + FMap U (hom-right uo (λ x₁ → x₁) ・ FMap F (FMap U (hom-right uo (λ x₁ → x₁)))) + ≡⟨ IsFunctor.distr (isFunctor U ) ⟩ + FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap U (FMap F (FMap U (hom-right uo (λ x₁ → x₁)))) + ≡⟨⟩ + TMap μ a ・ FMap (U ● F) (TMap μ a) + ∎ + + + + + +