• Dual of an end
• A cowedge is defined by injections into the co-end of all diagonal elements.

p(a, a)   p(b, b)  \          /  π[a]      π[b]   \        /    v      v     \int^x p(x, x)

• It's a universal cowedge, so every cowedge c other must factor.

p(a, a)   p(b, b)  \   \  /    /  π[a]  c   π[b]  \     |    /   \    ∃!  /    \   |  /    v   v  v     \int^x p(x, x)

• Now we have the cowedge condition. For every morphism h: b -> a, and for every cowedge c, the following must hold:

   [p b a]  /      \[p a a]   [p b b]  \      /      c

• By curry howard, type coend p = exists a. p a a

data Coend p where  MkCoend :: p a a -> Coend p

type End (p :: * -> * -> *) = forall x. p x x

• A functor is continuous if it preserves limits.
• Recall that Hom functor preserves limits.

-- Hom(\int^x p(x, x), r) ~= \int_x (Hom(p x x, r))type Hom a b = a -> b

• Set(\int^x p(x, r), s) is asking for a function Coend p -> r.
• But e claim this is the same as having forall a. (p a a -> r).
• So we can write Set(\int^x p(x, x), r) ~= \int_x Set(p(x, x), r).

-- | \int_x Set(p(x, x), r)-- | \int_x Hom(p(x, x), r)-- | \int_x RHS(x,x)       where RHS a b = Hom(p(a, b), r)type RHS p r a b = Hom (p a b) r -- rhs of the above expression

The isomorphisms are witnessed below, reminiscent of building a continuation

-- fwd :: (Coend p -> r) -> End (RHS p r)-- fwd :: (Coend p -> r) -> (forall x. (RHS r) x x)-- fwd :: (Coend p -> r) -> (forall x. Hom (p x x) r)-- fwd :: (Coend p -> r) -> (forall x. (p x x) -> r)fwd :: Profunctor p => (Coend p -> r) -> (forall x. (p x x) -> r)fwd coendp2r  pxx = coendp2r (MkCoend pxx)

• The backward iso, reminiscent of just applying a continuation.

-- bwd :: End (RHS p r)             -> (Coend p -> r)-- bwd :: (forall x. (RHS r) x x)   -> (Coend p -> r)-- bwd :: (forall x. Hom (p x x) r) -> (Coend p -> r)-- bwd :: (forall x. (p x x) -> r)  -> (Coend p -> r)bwd :: Profunctor p => (forall x. (p x x) -> r) -> Coend p -> rbwd pxx2r (MkCoend paa) = pxx2r paa

• Ninja coyoneda lemma: \int^x C(x, a) * f(x) ~= f(a)
• Witnessed by the following:

-- ninja coyoneda lemma:-- \int^x C(x, a) * f(x) ~= f(a)-- the profunctor is \int^x NinjaLHS[f, a](x, y)--   wherenewtype NinjaLHS g b y z = MkNinjaLHS (y -> b, g z)

• Forward iso:

-- ninjaFwd :: Functor f => Coend (NinjaLHS f a) -> f aninjaFwd :: Functor g => Coend (NinjaLHS g r) -> g rninjaFwd (MkCoend (MkNinjaLHS (x2r, gx))) = fmap x2r gx

• Backward iso:

-- ninjaBwd :: Functor f => g r -> (Coend (NinjaLHS g r))-- ninjaBwd :: Functor f => g r -> (∃ x. (NinjaLHS g r x x))-- ninjaBwd :: Functor f => g r -> (∃ x. (NinjaLHS (x -> r, g x))ninjaBwd :: Functor g => g r -> Coend (NinjaLHS g r)ninjaBwd gr = MkCoend (MkNinjaLHS (x2r, gx)) where   x2r = id -- choose x = r, then x2r = r2r   gx = gr -- choose x = r

• We can prove the ninja coyoneda via coend calculus plus yoneda embedding, by using the fact that yoneda is full and faithful.
• So instead of showing LHS ~= RHS in the ninja coyoneda, we will show that Hom(LHS, -) ~= Hom(RHS, -).

• We compute as:

Set(\int^x C(x, a) * f(x), s) ~? Set(f(a), x)[continuity:]\int_x Set(C(x, a) * f(x), s) ~? Set(f(a), x)[currying:]\int_x Set(C(x, a), Set(f(x) s)) ~? Set(f(a), x)[ninja yoneda on Set(f(-), s):]Set(f(a) s)) ~? Set(f(a), x)Set(f(a) s)) ~= Set(f(a), x)

§ Ninja Coyoneda for containers

• The type of NinjaLHS, when specialized to NinjaLHS g b r r becomes (r -> b, g r).
• This is sorta the way you can get a Functor instance on any g, by essentially accumulating the changes into the (r -> b). I learnt this trick from some kmett library, but I'm not sure what the original reference is.

• Start with NinjaLHS:

-- ninja coyoneda lemma:-- \int^x C(x, a) * f(x) ~= f(a)-- the profunctor is \int^x NinjaLHS[f, a](x, y)--   wherenewtype NinjaLHS g b y z = MkNinjaLHS (y -> b, g z)

• Specialize by taking the diagonal:

-- newtype NinjaLHS' g i o = MkNinjaLHS' (i -> o, g i)newtype NinjaLHS' g i o = MkNinjaLHS' (NinjaLHS g o i i)

• Write a smart constructor to lift values into NinjaLHS':

mkNinjaLHS' :: g i -> NinjaLHS' g i imkNinjaLHS' gi = MkNinjaLHS' (MkNinjaLHS (id, gi))

• Implement functor instance for NinjaLHS' g i:

-- convert any storage of shape `g`, input type `i` into a functorinstance Functor (NinjaLHS' g i) where  -- f:: (o -> o') -> NinjaLHS' g i o -> NinjaLHS' g i o'  fmap o2o' (MkNinjaLHS' (MkNinjaLHS (i2o, gi))) =    MkNinjaLHS' $ MkNinjaLHS (\i -> o2o' (i2o i), gi)

See that to be able to extract out values, we need g to be a functor:

extract :: Functor g => NinjaLHS' g i o -> g oextract (MkNinjaLHS' (MkNinjaLHS (i2o, gi))) = fmap i2o gi