objective覚書

objective-0.6.1

O' = data Object e m
= forall x. e x -> m (x, Object e m)
= hom(e, m . (-,O'))   (as Nat)

functor Kを用いてe = hom(a,K-) = forall x. a -> K xと書けるとき(Data.Functor.Kan.Ranを見よ)

O' = hom(hom(a,K-), m . (-,O'))
= hom(K^-1(hom(a,-)), m . (-,O'))
  -- by K^-1 -| Ran K
= hom(hom(a,-), Ran K (m . (-,O')))
  -- covariant yoneda
= Ran K (m . (-,O')) a
= forall r. (a -> K r) -> m (r,O')

Object e mがわかっているとき, eと適当な型の直積をとっても良い:

O' = data Object (forall x. (a,e x)) m
= hom((a×-) . e, m . (-,O'))
= hom(e , hom(a,-) . m . (-,O'))
= data Object e (forall x. a -> m x)

eとして Request a b r = (a,b->r) を取ったものはProcessとして定義されている.

P' = data Process a b m
= Object (Request a b) m
= hom((a×-) . hom(b,-), m . (-,P'))
= hom(hom(b,-), hom(a,-) . m . (-,P'))
= a -> m (b, P')

左Kan拡張を使ってもいいけれど同値な式以上の意味はなさそう.
Lanがより単純な項に書き換えられるなら何かあるのかも？

O' = data Object e m = Hom(Lan (-,O') e, m)