A Universe of Sorts

§ Coends

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 -> r
bwd 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)
--   where
newtype NinjaLHS g b y z = MkNinjaLHS (y -> b, g z)

Forward iso:

-- ninjaFwd :: Functor f => Coend (NinjaLHS f a) -> f a
ninjaFwd :: Functor g => Coend (NinjaLHS g r) -> g r
ninjaFwd (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)
--   where
newtype 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 i
mkNinjaLHS' gi = MkNinjaLHS' (MkNinjaLHS (id, gi))

Implement functor instance for NinjaLHS' g i:

-- convert any storage of shape `g`, input type `i` into a functor
instance 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 o
extract (MkNinjaLHS' (MkNinjaLHS (i2o, gi))) = fmap i2o gi