Kleisli Category の Comparison Functor
Menu MenuKleisli Category の Comparison Functor
examples/comparison-functor.agdai Monad の Resolution (UR,FR,εR) があると、その Adjoint Functor は、Kleisli Category の U_T, F_T と Comparison Functor K_T を通して関連します。ここでも問題になるのは、T と UR ○ FR が同じものなのに型が違うということです。
T=UF : T ≃ (UR ○ FR)があるのだから変換できるだろうと思うし、実際、
KtoT : (a b : Obj A) -> (RHom a b) -> {g h : Hom A (FObj ( U_K ○ F_K ) b) (FObj T b) } -> ([ A ] g ~ h) -> Hom A a (FObj T b) KtoT _ _ f {g} {h} (Category.Cat.refl eq) = A [ g o (KMap f) ] KTMap : {a b : Obj A} -> (f : RHom a b) -> Hom A a (FObj T b) KTMap {a} {b} f = KtoT a b f {_} {_} (( ≃-sym (T=UF RK)) (id1 A b))とかで変換しようと思えばできなくはないようです。 T ≃ (UR ○ FR) を [ A ] g ~ h で受けて、左辺と右辺を取り出すというような方法です。なのですが、どうしてもうまく行かず。「よくわからないがとにかく等しい」というのを扱うのは難しい。
でも、Adjoint があるので、それから Monad を構成すると、それは、(UR ○ FR) に対して定義された Monad になります。Resolution なのだから、それは元の Monad と同じはず。T と μ が等しい以上の意味はないわけですけど。この方針だと型は合います。
KTMap のような変換を使うのと証明の形自体は変わりません。 Comparison Functor の証明
まず、module のparameterとして、いろいろなものを定義します。
module comparison-functor { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } { η : NTrans A A identityFunctor T } { μ : NTrans A A (T ○ T) T } { M' : Monad A T η μ } {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' ) { U_K : Functor B A } { F_K : Functor A B } { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) } { ε_K : NTrans B B ( F_K ○ U_K ) identityFunctor } { μ_K' : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) } ( AdjK : Adjunction A B U_K F_K η_K ε_K ) ( RK : MResolution A B T U_K F_K {η_K} {ε_K} {μ_K'} AdjK ) where open import adj-monad T_K = U_K ○ F_K μ_K : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) μ_K = UεF A B U_K F_K ε_K M : Monad A (U_K ○ F_K ) η_K μ_K M = Adj2Monad A B {U_K} {F_K} {η_K} {ε_K} AdjK open import kleisli {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } { η_K } { μ_K } { M }μ_K は UεF として作り、Adjunction AdjK から Monad M を作ります。その Monad に対して Kleisli Category を作ってやります。これで Resolution、Monad、Kleisli Category と道具立てはそろいました。
Functor K_T は、対象は F_K(a) で、射は ε(F_K b) o F_K(f) です。f は Hom A a b です。
open Functor open NTrans open KleisliHom open Adjunction open MResolution kfmap : {a b : Obj A} (f : KHom a b) -> Hom B (FObj F_K a) (FObj F_K b) kfmap {_} {b} f = B [ TMap ε_K (FObj F_K b) o FMap F_K (KMap f) ] K_T : Functor KleisliCategory B K_T = record { FObj = FObj F_K ; FMap = kfmap ; isFunctor = record { ≈-cong = ≈-cong ; identity = identity ; distr = distr1 } } where identity : {a : Obj A} → B [ kfmap (K-id {a}) ≈ id1 B (FObj F_K a) ] identity {a} = let open ≈-Reasoning (B) in begin kfmap (K-id {a}) ≈⟨⟩ TMap ε_K (FObj F_K a) o FMap F_K (KMap (K-id {a})) ≈⟨⟩ TMap ε_K (FObj F_K a) o FMap F_K (TMap η_K a) ≈⟨ IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩ id1 B (FObj F_K a) ∎ ≈-cong : {a b : Obj A} -> {f g : KHom a b} → A [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ] ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in begin kfmap f ≈⟨⟩ TMap ε_K (FObj F_K b) o FMap F_K (KMap f) ≈⟨ cdr ( fcong F_K f≈g) ⟩ TMap ε_K (FObj F_K b) o FMap F_K (KMap g) ≈⟨⟩ kfmap g ∎identity と ≈-cong は簡単に証明できます。分配則は元の圏が Kleisli 圏なので厄介です。* が join です。
distr1 : {a b c : Obj A} {f : KHom a b} {g : KHom b c} → B [ kfmap (g * f) ≈ (B [ kfmap g o kfmap f ] )] distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (B) in begin kfmap (g * f) ≈⟨⟩ TMap ε_K (FObj F_K c) o FMap F_K (KMap (g * f)) ≈⟨⟩ TMap ε_K (FObj F_K c) o FMap F_K (A [ TMap μ_K c o A [ FMap ( U_K ○ F_K ) (KMap g) o KMap f ] ] ) ≈⟨ cdr ( distr F_K ) ⟩ TMap ε_K (FObj F_K c) o ( FMap F_K (TMap μ_K c) o ( FMap F_K (A [ FMap ( U_K ○ F_K ) (KMap g) o KMap f ]))) ≈⟨ cdr (cdr ( distr F_K )) ⟩ TMap ε_K (FObj F_K c) o ( FMap F_K (TMap μ_K c) o (( FMap F_K (FMap ( U_K ○ F_K ) (KMap g))) o (FMap F_K (KMap f)))) ≈⟨ cdr assoc ⟩ TMap ε_K (FObj F_K c) o ((( FMap F_K (TMap μ_K c) o ( FMap F_K (FMap (U_K ○ F_K) (KMap g))))) o (FMap F_K (KMap f))) ≈⟨⟩ TMap ε_K (FObj F_K c) o (( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) )) o ( FMap F_K (FMap (U_K ○ F_K) (KMap g)))) o (FMap F_K (KMap f))) ≈⟨ sym (cdr assoc) ⟩ TMap ε_K (FObj F_K c) o (( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) ))) o (( FMap F_K (FMap (U_K ○ F_K) (KMap g))) o (FMap F_K (KMap f)))) ≈⟨ assoc ⟩ (TMap ε_K (FObj F_K c) o ( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) )))) o (( FMap F_K (FMap (U_K ○ F_K) (KMap g))) o (FMap F_K (KMap f))) ≈⟨ car (sym (nat ε_K)) ⟩ (TMap ε_K (FObj F_K c) o ( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)))) o (( FMap F_K (FMap (U_K ○ F_K) (KMap g))) o (FMap F_K (KMap f))) ≈⟨ sym assoc ⟩ TMap ε_K (FObj F_K c) o (( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c))) o ((( FMap F_K (FMap (U_K ○ F_K) (KMap g)))) o (FMap F_K (KMap f)))) ≈⟨ cdr assoc ⟩ TMap ε_K (FObj F_K c) o ((( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c))) o (( FMap F_K (FMap (U_K ○ F_K) (KMap g))))) o (FMap F_K (KMap f))) ≈⟨ cdr ( car ( begin TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)) o ((FMap F_K (FMap (U_K ○ F_K) (KMap g)))) ≈⟨⟩ TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)) o (FMap (F_K ○ U_K) (FMap F_K (KMap g))) ≈⟨ sym (nat ε_K) ⟩ ( FMap F_K (KMap g)) o (TMap ε_K (FObj F_K b)) ∎ )) ⟩ TMap ε_K (FObj F_K c) o ((( FMap F_K (KMap g)) o (TMap ε_K (FObj F_K b))) o FMap F_K (KMap f)) ≈⟨ cdr (sym assoc) ⟩ TMap ε_K (FObj F_K c) o (( FMap F_K (KMap g)) o (TMap ε_K (FObj F_K b) o FMap F_K (KMap f))) ≈⟨ assoc ⟩ (TMap ε_K (FObj F_K c) o FMap F_K (KMap g)) o (TMap ε_K (FObj F_K b) o FMap F_K (KMap f)) ≈⟨⟩ kfmap g o kfmap f ∎わお。でも、こちらで使われているのは自然変換の可換性だけです。
これで Functor はできたので、あとは性質を見ていくだけです。
Lemma-K1 : {a b : Obj A} ( f : Hom A a b ) -> B [ FMap K_T ( FMap F_T f) ≈ FMap F_K f ] Lemma-K1 {a} {b} f = let open ≈-Reasoning (B) in begin FMap K_T ( FMap F_T f) ≈⟨⟩ TMap ε_K (FObj F_K b) o FMap F_K (KMap( FMap F_T f)) ≈⟨⟩ TMap ε_K (FObj F_K b) o FMap F_K (A [ TMap η_K b o f ]) ≈⟨ cdr ( distr F_K) ⟩ TMap ε_K (FObj F_K b) o (FMap F_K (TMap η_K b) o FMap F_K f ) ≈⟨ assoc ⟩ (TMap ε_K (FObj F_K b) o FMap F_K (TMap η_K b)) o FMap F_K f ≈⟨ car ( IsAdjunction.adjoint2 (isAdjunction AdjK)) ⟩ id1 B (FObj F_K b) o FMap F_K f ≈⟨ idL ⟩ FMap F_K f ∎ Lemma-K2 : {a b : Obj A} ( f : KHom a b ) -> A [ FMap U_K ( FMap K_T f) ≈ FMap U_T f ] Lemma-K2 {a} {b} f = let open ≈-Reasoning (A) in begin FMap U_K ( FMap K_T f) ≈⟨⟩ FMap U_K ( B [ TMap ε_K (FObj F_K b) o FMap F_K (KMap f) ] ) ≈⟨ distr U_K ⟩ FMap U_K ( TMap ε_K (FObj F_K b)) o FMap U_K (FMap F_K (KMap f) ) ≈⟨⟩ TMap μ_K b o FMap T_K (KMap f) ≈⟨⟩ -- the definition FMap U_T f ∎この二つにより、
(K_T ○ F_T) ≃ F_K (U_K ○ K_T) ≃ U_Tを証明することができます。任意の Resolution F_K, U_K は、Comparison Functor K_T により、Kleisli Category による Resolution と結び付けられます。
kfmap {_} {b} f = B [ TMap ε_K (FObj F_K b) o FMap F_K (KMap f) ]の必要性が、この二つの証明から出てくることがわかります。