§ Natural Transformations as ends

-----p a' b'-------
a' -> [a -> b] -> b'
       --pab---
dimap :: (a' -> a) -> (b -> b') -> (f a -> g b) -> (f a' -> g b')
dimap a'2a b2b' fa2gb = \fa' -> 
  let fa = fmap a'2a fa'
  let gb = fa2gb fa
  let gb' - fmap b2b' gb
  in gb'
dimap a'2a b2b' fa2gb = (@fmap g b2b')  . fa2gb  . (@fmap f a'2a)
 (p x x, p y y, p z z, ... infinite product)
\int_x p(x,x)
 /[πa]  [πb]\
v            v
p(a,a)       p(b,b)
 \            /
[p(id, k)]  [p(k,id)]
   \        /
    v      v
     p a b
    (forall x. f x -> g x)
    /               \
  [@ a]            [@ b]
   v                v
 τa:(f a -> g a)     τb:(f b -> g b)
   \                  /
dimap id(a) k τa    dimap k id(b) τb
   \                 /
    \               τb.(@fmap f k): (f a-> g b) 
     \              /
     \           COMMUTES?
     \            /
    (@fmap g k).τa(f a -> g b)
    

§ Invoking Yoneda