coyoneda-dinat.md

type A :: Type
type X :: Type
type F :: Type -> Type
instance Functor F

p :: forall x. (F x, x -> A) -> X

newtype H a = H { runH :: (a -> A) -> X }
instance Functor H where
  fmap g hc = H $ \k -> runH hc (k . g))

p' :: forall r. f r -> H r
p' fc = H (\k -> p (fc, k))

forall (c :: Type) (fc :: F c) (g :: c -> A).
  p @c (fc,g)
   = runH (p' @c fc) g
   = (\k -> runH (p' @c fc) (k . g)) id
   = runH ( H (\k -> runH (p' fc) (k . g)) ) id
   = runH (fmap g (p' @c fc)) id
   -- naturality
   = runH (p' @A (fmap g fc)) id
   = p @A (fmap g fc, id)