Kleisli Category
Menu MenuKleisli Category
examples/kleisli.agda Monad の join は単位元と結合則が成り立つので、Aの対象と join を射とする圏を作ることができます。これを使って、さらに、Monad から Adjoint Functor (随伴関手) を作ることもできます。これを Monad の Resolution と言います。これが次の目標です。Kleisli Category を作るために、まず射を定義します。 Monad M とその T, η, μは、module のパラメータとして定義します。
module kleisli { 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 η μ } where
このようにすることにより、任意のMonadから、この module を使って、Kleisli Category を作れるようになります。(任意の Resolution と Kelsli Category を結ぶ Comparison Functor を作る時に使います)
射は record として定義します。Sets では record にする必要はありませでした。
record KleisliHom { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } (a : Obj A) (b : Obj A)
: Set c₂ where
field
KMap : Hom A a ( FObj T b )
射は、元のMonadの圏 A の対象 a から、T(b) への(Aの)射です。Monad では、常に何かのFunctor を返します。Functor の中には、A の対象 b
が格納されています。T を通して、b にアクセスすることができます。
圏の射として使うには、対象二つから、このrecordを返す形式でなければなりません。射である KMap に access するために open します。残りの情報は暗黙の引数にします。
open KleisliHom
KHom = \(a b : Obj A) -> KleisliHom {c₁} {c₂} {ℓ} {A} {T} a b
K-id : {a : Obj A} → KHom a a
K-id {a = a} = record { KMap = TMap η a }
単位射は、自然変換ηでした。射に対する結合と等式を定義します。
open import Relation.Binary.Core
_⋍_ : { a : Obj A } { b : Obj A } (f g : KHom a b ) -> Set ℓ
_⋍_ {a} {b} f g = A [ KMap f ≈ KMap g ]
_*_ : { a b c : Obj A } → ( KHom b c) → ( KHom a b) → KHom a c
_*_ {a} {b} {c} g f = record { KMap = join M {a} {b} {c} (KMap g) (KMap f) }
変な記号を使うのは monomorphism による名前の衝突を避けるためです。比較は元のAの射の比較をそのまま使います。結合は、前に定義した join です。暗黙の引数 (implicit parameter )により余計な引数が隠れてくれるので、きれいな二項演算子になっています。(主に黄色を消すために)必要があれば{a}などを指定することもできます。順序は重要なので {_} などで飛ばして、正しい位置の暗黙の引数の値を指定します。
あとは Category を作るだけです。
isKleisliCategory : IsCategory ( Obj A ) KHom _⋍_ _*_ K-id
isKleisliCategory = record { isEquivalence = isEquivalence
; identityL = KidL
; identityR = KidR
; o-resp-≈ = Ko-resp
; associative = Kassoc
}
where
open ≈-Reasoning (A)
isEquivalence : { a b : Obj A } ->
IsEquivalence {_} {_} {KHom a b} _⋍_
isEquivalence {C} {D} = -- this is the same function as A's equivalence but has different types
record { refl = refl-hom
; sym = sym
; trans = trans-hom
}
KidL : {C D : Obj A} -> {f : KHom C D} → (K-id * f) ⋍ f
KidL {_} {_} {f} = Lemma7 (KMap f)
KidR : {C D : Obj A} -> {f : KHom C D} → (f * K-id) ⋍ f
KidR {_} {_} {f} = Lemma8 (KMap f)
Ko-resp : {a b c : Obj A} -> {f g : KHom a b } → {h i : KHom b c } →
f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g)
Ko-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = Lemma10 {a} {b} {c} (KMap f) (KMap g) (KMap h) (KMap i) eq-fg eq-hi
Kassoc : {a b c d : Obj A} -> {f : KHom c d } → {g : KHom b c } → {h : KHom a b } →
(f * (g * h)) ⋍ ((f * g) * h)
Kassoc {_} {_} {_} {_} {f} {g} {h} = Lemma9 (KMap f) (KMap g) (KMap h)
KleisliCategory : Category c₁ c₂ ℓ
KleisliCategory =
record { Obj = Obj A
; Hom = KHom
; _o_ = _*_
; _≈_ = _⋍_
; Id = K-id
; isCategory = isKleisliCategory
}
Category の性質のほとんどは証明済ですが、そういえば、 o-resp-≈ は、まだ証明してませんでした。
-- o-resp in Kleisli Category ( for Functor definitions )
--
Lemma10 : {a b c : Obj A} -> (f g : Hom A a (FObj T b) ) → (h i : Hom A b (FObj T c) ) →
A [ f ≈ g ] → A [ h ≈ i ] → A [ (join M h f) ≈ (join M i g) ]
Lemma10 {a} {b} {c} f g h i eq-fg eq-hi = let open ≈-Reasoning (A) in
begin
join M h f
≈⟨⟩
TMap μ c o ( FMap T h o f )
≈⟨ cdr ( IsCategory.o-resp-≈ (Category.isCategory A) eq-fg ((IsFunctor.≈-cong (isFunctor T)) eq-hi )) ⟩
TMap μ c o ( FMap T i o g )
≈⟨⟩
join M i g
∎
射の行き先がFunctor Tなので、 Functor の ≈-cong と元の圏Aの o-resp-≈ を使って証明します。cong が使えないので、こういう証明になります。引数で、 f ≈ g を(の型に対応する証明を)直接受け取っています。これは Rel という集合であって、_≈_ という constructor ではありません。なので、cong は使えないわけです。
圏AもMonad M も、ここでは抽象的な「ある性質を満たすもの」であり、_≈_ が実際に何かは定義されていません。Sets の場合は _≡_ と集合の等号と指定されていました。つまり、圏 Sets は具体的な圏であり、ここのA は抽象的な仮定された圏なわけです。具体的な射の中身に立ち入らずに証明できたものは、具体的なものに応用することができます。
実際、
Monoid Monad から、
open import kleisli {_} {_} {_} {A} {T} {η} {μ} {MonoidMonad}
とすると、kleisli Category を作ることができます。