    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE ExistentialQuantification #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE UndecidableInstances #-}
    -----------------------------------------------------------------------------
    -- |
    -- Copyright   :  (C) 2014-2016 Edward Kmett
    -- License     :  BSD-style (see the file LICENSE)
    --
    -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
    -- Stability   :  provisional
    -- Portability :  portable
    --
    -- Eitan Chatav first introduced me to this construction
    --
    -- The Day convolution of two covariant functors is a covariant functor.
    --
    -- Day convolution is usually defined in terms of contravariant functors,
    -- however, it just needs a monoidal category, and Hask^op is also monoidal.
    --
    -- Day convolution can be used to nicely describe monoidal functors as monoid
    -- objects w.r.t this product.
    --
    -- <http://ncatlab.org/nlab/show/Day+convolution>
    ----------------------------------------------------------------------------

    module Data.Functor.Day
      ( Day(..)
      , day
      , dap
      , assoc, disassoc
      , swapped
      , intro1, intro2
      , elim1, elim2
      , trans1, trans2
      , cayley, dayley
      ) where

    import Control.Applicative
    import Control.Category
    import Control.Comonad
    import Control.Comonad.Trans.Class
    import Data.Distributive
    import Data.Profunctor.Cayley (Cayley(..))
    import Data.Profunctor.Composition (Procompose(..))
    import Data.Functor.Adjunction
    import Data.Functor.Identity
    import Data.Functor.Rep
    import Prelude hiding (id,(.))

    -- | The Day convolution of two covariant functors.
    data Day f g a = forall b c. Day (f b) (g c) (b -> c -> a)

    -- | Construct the Day convolution
    day :: f (a -> b) -> g a -> Day f g b
    day :: forall (f :: * -> *) a b (g :: * -> *).
    f (a -> b) -> g a -> Day f g b
    day f (a -> b)
    fa g a
    gb = f (a -> b) -> g a -> ((a -> b) -> a -> b) -> Day f g b
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day f (a -> b)
    fa g a
    gb (a -> b) -> a -> b
    forall a. a -> a
    forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id

    instance Functor (Day f g) where
      fmap :: forall a b. (a -> b) -> Day f g a -> Day f g b
    fmap a -> b
    f (Day f b
    fb g c
    gc b -> c -> a
    bca) = f b -> g c -> (b -> c -> b) -> Day f g b
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day f b
    fb g c
    gc ((b -> c -> b) -> Day f g b) -> (b -> c -> b) -> Day f g b
    forall a b. (a -> b) -> a -> b
    $ \b
    b c
    c -> a -> b
    f (b -> c -> a
    bca b
    b c
    c)

    instance (Applicative f, Applicative g) => Applicative (Day f g) where
      pure :: forall a. a -> Day f g a
    pure a
    x = f () -> g () -> (() -> () -> a) -> Day f g a
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day (() -> f ()
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()) (() -> g ()
    forall a. a -> g a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()) (\()
    _ ()
    _ -> a
    x)
      (Day f b
    fa g c
    fb b -> c -> a -> b
    u) <*> :: forall a b. Day f g (a -> b) -> Day f g a -> Day f g b
    <*> (Day f b
    gc g c
    gd b -> c -> a
    v) =
        f (b, b) -> g (c, c) -> ((b, b) -> (c, c) -> b) -> Day f g b
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day ((,) (b -> b -> (b, b)) -> f b -> f (b -> (b, b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f b
    fa f (b -> (b, b)) -> f b -> f (b, b)
    forall a b. f (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> f b
    gc) ((,) (c -> c -> (c, c)) -> g c -> g (c -> (c, c))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> g c
    fb g (c -> (c, c)) -> g c -> g (c, c)
    forall a b. g (a -> b) -> g a -> g b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> g c
    gd)
            (\(b
    a,b
    c) (c
    b,c
    d) -> b -> c -> a -> b
    u b
    a c
    b (b -> c -> a
    v b
    c c
    d))

    instance (Representable f, Representable g) => Distributive (Day f g) where
      distribute :: forall (f :: * -> *) a. Functor f => f (Day f g a) -> Day f g (f a)
    distribute f (Day f g a)
    f = f (Rep f) -> g (Rep g) -> (Rep f -> Rep g -> f a) -> Day f g (f a)
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day ((Rep f -> Rep f) -> f (Rep f)
    forall a. (Rep f -> a) -> f a
    forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
    tabulate Rep f -> Rep f
    forall a. a -> a
    forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id) ((Rep g -> Rep g) -> g (Rep g)
    forall a. (Rep g -> a) -> g a
    forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
    tabulate Rep g -> Rep g
    forall a. a -> a
    forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id) ((Rep f -> Rep g -> f a) -> Day f g (f a))
    -> (Rep f -> Rep g -> f a) -> Day f g (f a)
    forall a b. (a -> b) -> a -> b
    $ \Rep f
    x Rep g
    y ->
        (Day f g a -> a) -> f (Day f g a) -> f a
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\(Day f b
    m g c
    n b -> c -> a
    o) -> b -> c -> a
    o (f b -> Rep f -> b
    forall a. f a -> Rep f -> a
    forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
    index f b
    m Rep f
    x) (g c -> Rep g -> c
    forall a. g a -> Rep g -> a
    forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
    index g c
    n Rep g
    y)) f (Day f g a)
    f

      collect :: forall (f :: * -> *) a b.
    Functor f =>
    (a -> Day f g b) -> f a -> Day f g (f b)
    collect a -> Day f g b
    g f a
    f = f (Rep f) -> g (Rep g) -> (Rep f -> Rep g -> f b) -> Day f g (f b)
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day ((Rep f -> Rep f) -> f (Rep f)
    forall a. (Rep f -> a) -> f a
    forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
    tabulate Rep f -> Rep f
    forall a. a -> a
    forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id) ((Rep g -> Rep g) -> g (Rep g)
    forall a. (Rep g -> a) -> g a
    forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
    tabulate Rep g -> Rep g
    forall a. a -> a
    forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id) ((Rep f -> Rep g -> f b) -> Day f g (f b))
    -> (Rep f -> Rep g -> f b) -> Day f g (f b)
    forall a b. (a -> b) -> a -> b
    $ \Rep f
    x Rep g
    y ->
        (a -> b) -> f a -> f b
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\a
    q -> case a -> Day f g b
    g a
    q of Day f b
    m g c
    n b -> c -> b
    o -> b -> c -> b
    o (f b -> Rep f -> b
    forall a. f a -> Rep f -> a
    forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
    index f b
    m Rep f
    x) (g c -> Rep g -> c
    forall a. g a -> Rep g -> a
    forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
    index g c
    n Rep g
    y)) f a
    f

    instance (Representable f, Representable g) => Representable (Day f g) where
      type Rep (Day f g) = (Rep f, Rep g)
      tabulate :: forall a. (Rep (Day f g) -> a) -> Day f g a
    tabulate Rep (Day f g) -> a
    f = f (Rep f) -> g (Rep g) -> (Rep f -> Rep g -> a) -> Day f g a
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day ((Rep f -> Rep f) -> f (Rep f)
    forall a. (Rep f -> a) -> f a
    forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
    tabulate Rep f -> Rep f
    forall a. a -> a
    forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id) ((Rep g -> Rep g) -> g (Rep g)
    forall a. (Rep g -> a) -> g a
    forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
    tabulate Rep g -> Rep g
    forall a. a -> a
    forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id) (((Rep f, Rep g) -> a) -> Rep f -> Rep g -> a
    forall a b c. ((a, b) -> c) -> a -> b -> c
    curry (Rep f, Rep g) -> a
    Rep (Day f g) -> a
    f)
      index :: forall a. Day f g a -> Rep (Day f g) -> a
    index (Day f b
    m g c
    n b -> c -> a
    o) (Rep f
    x,Rep g
    y) = b -> c -> a
    o (f b -> Rep f -> b
    forall a. f a -> Rep f -> a
    forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
    index f b
    m Rep f
    x) (g c -> Rep g -> c
    forall a. g a -> Rep g -> a
    forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
    index g c
    n Rep g
    y)

    instance (Adjunction f u, Adjunction f' u') => Adjunction (Day f f') (Day u u') where
      unit :: forall a. a -> Day u u' (Day f f' a)
    unit a
    a = u (f ())
    -> u' (f' ())
    -> (f () -> f' () -> Day f f' a)
    -> Day u u' (Day f f' a)
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day (() -> u (f ())
    forall a. a -> u (f a)
    forall (f :: * -> *) (u :: * -> *) a.
    Adjunction f u =>
    a -> u (f a)
    unit ()) (() -> u' (f' ())
    forall a. a -> u' (f' a)
    forall (f :: * -> *) (u :: * -> *) a.
    Adjunction f u =>
    a -> u (f a)
    unit ()) (\f ()
    f f' ()
    f' -> f () -> f' () -> (() -> () -> a) -> Day f f' a
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day f ()
    f f' ()
    f' (\() () -> a
    a))
      counit :: forall a. Day f f' (Day u u' a) -> a
    counit (Day f b
    f f' c
    f' b -> c -> Day u u' a
    h) = case b -> c -> Day u u' a
    h b
    a c
    a' of Day u b
    u u' c
    u' b -> c -> a
    g -> b -> c -> a
    g (u b -> f () -> b
    forall (f :: * -> *) (u :: * -> *) b a.
    Adjunction f u =>
    u b -> f a -> b
    indexAdjunction u b
    u f ()
    f_) (u' c -> f' () -> c
    forall (f :: * -> *) (u :: * -> *) b a.
    Adjunction f u =>
    u b -> f a -> b
    indexAdjunction u' c
    u' f' ()
    f_')
        where
          (b
    a, f ()
    f_) = f b -> (b, f ())
    forall (f :: * -> *) (u :: * -> *) a.
    Adjunction f u =>
    f a -> (a, f ())
    splitL f b
    f
          (c
    a', f' ()
    f_') = f' c -> (c, f' ())
    forall (f :: * -> *) (u :: * -> *) a.
    Adjunction f u =>
    f a -> (a, f ())
    splitL f' c
    f'

    instance (Comonad f, Comonad g) => Comonad (Day f g) where
      extract :: forall a. Day f g a -> a
    extract (Day f b
    fb g c
    gc b -> c -> a
    bca) = b -> c -> a
    bca (f b -> b
    forall a. f a -> a
    forall (w :: * -> *) a. Comonad w => w a -> a
    extract f b
    fb) (g c -> c
    forall a. g a -> a
    forall (w :: * -> *) a. Comonad w => w a -> a
    extract g c
    gc)
      duplicate :: forall a. Day f g a -> Day f g (Day f g a)
    duplicate (Day f b
    fb g c
    gc b -> c -> a
    bca) = f (f b)
    -> g (g c) -> (f b -> g c -> Day f g a) -> Day f g (Day f g a)
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day (f b -> f (f b)
    forall a. f a -> f (f a)
    forall (w :: * -> *) a. Comonad w => w a -> w (w a)
    duplicate f b
    fb) (g c -> g (g c)
    forall a. g a -> g (g a)
    forall (w :: * -> *) a. Comonad w => w a -> w (w a)
    duplicate g c
    gc) (\f b
    fb' g c
    gc' -> f b -> g c -> (b -> c -> a) -> Day f g a
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day f b
    fb' g c
    gc' b -> c -> a
    bca)

    instance (ComonadApply f, ComonadApply g) => ComonadApply (Day f g) where
      Day f b
    fa g c
    fb b -> c -> a -> b
    u <@> :: forall a b. Day f g (a -> b) -> Day f g a -> Day f g b
    <@> Day f b
    gc g c
    gd b -> c -> a
    v =
        f (b, b) -> g (c, c) -> ((b, b) -> (c, c) -> b) -> Day f g b
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day ((,) (b -> b -> (b, b)) -> f b -> f (b -> (b, b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f b
    fa f (b -> (b, b)) -> f b -> f (b, b)
    forall a b. f (a -> b) -> f a -> f b
    forall (w :: * -> *) a b.
    ComonadApply w =>
    w (a -> b) -> w a -> w b
    <@> f b
    gc) ((,) (c -> c -> (c, c)) -> g c -> g (c -> (c, c))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> g c
    fb g (c -> (c, c)) -> g c -> g (c, c)
    forall a b. g (a -> b) -> g a -> g b
    forall (w :: * -> *) a b.
    ComonadApply w =>
    w (a -> b) -> w a -> w b
    <@> g c
    gd)
            (\(b
    a,b
    c) (c
    b,c
    d) -> b -> c -> a -> b
    u b
    a c
    b (b -> c -> a
    v b
    c c
    d))

    instance Comonad f => ComonadTrans (Day f) where
      lower :: forall (w :: * -> *) a. Comonad w => Day f w a -> w a
    lower (Day f b
    fb w c
    gc b -> c -> a
    bca) = b -> c -> a
    bca (f b -> b
    forall a. f a -> a
    forall (w :: * -> *) a. Comonad w => w a -> a
    extract f b
    fb) (c -> a) -> w c -> w a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> w c
    gc

    -- | Day convolution provides a monoidal product. The associativity
    -- of this monoid is witnessed by 'assoc' and 'disassoc'.
    --
    -- @
    -- 'assoc' . 'disassoc' = 'id'
    -- 'disassoc' . 'assoc' = 'id'
    -- 'fmap' f '.' 'assoc' = 'assoc' '.' 'fmap' f
    -- @
    assoc :: Day f (Day g h) a -> Day (Day f g) h a
    assoc :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a.
    Day f (Day g h) a -> Day (Day f g) h a
    assoc (Day f b
    fb (Day g b
    gd h c
    he b -> c -> c
    dec) b -> c -> a
    bca) = Day f g (b, b) -> h c -> ((b, b) -> c -> a) -> Day (Day f g) h a
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day (f b -> g b -> (b -> b -> (b, b)) -> Day f g (b, b)
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day f b
    fb g b
    gd (,)) h c
    he (((b, b) -> c -> a) -> Day (Day f g) h a)
    -> ((b, b) -> c -> a) -> Day (Day f g) h a
    forall a b. (a -> b) -> a -> b
    $
      \ (b
    b,b
    d) c
    e -> b -> c -> a
    bca b
    b (b -> c -> c
    dec b
    d c
    e)

    -- | Day convolution provides a monoidal product. The associativity
    -- of this monoid is witnessed by 'assoc' and 'disassoc'.
    --
    -- @
    -- 'assoc' . 'disassoc' = 'id'
    -- 'disassoc' . 'assoc' = 'id'
    -- 'fmap' f '.' 'disassoc' = 'disassoc' '.' 'fmap' f
    -- @
    disassoc :: Day (Day f g) h a -> Day f (Day g h) a
    disassoc :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a.
    Day (Day f g) h a -> Day f (Day g h) a
    disassoc (Day (Day f b
    fb g c
    gc b -> c -> b
    bce) h c
    hd b -> c -> a
    eda) = f b -> Day g h (c, c) -> (b -> (c, c) -> a) -> Day f (Day g h) a
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day f b
    fb (g c -> h c -> (c -> c -> (c, c)) -> Day g h (c, c)
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day g c
    gc h c
    hd (,)) ((b -> (c, c) -> a) -> Day f (Day g h) a)
    -> (b -> (c, c) -> a) -> Day f (Day g h) a
    forall a b. (a -> b) -> a -> b
    $ \ b
    b (c
    c,c
    d) ->
      b -> c -> a
    eda (b -> c -> b
    bce b
    b c
    c) c
    d

    -- | The monoid for 'Day' convolution on the cartesian monoidal structure is symmetric.
    --
    -- @
    -- 'fmap' f '.' 'swapped' = 'swapped' '.' 'fmap' f
    -- @
    swapped :: Day f g a -> Day g f a
    swapped :: forall (f :: * -> *) (g :: * -> *) a. Day f g a -> Day g f a
    swapped (Day f b
    fb g c
    gc b -> c -> a
    abc) = g c -> f b -> (c -> b -> a) -> Day g f a
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day g c
    gc f b
    fb ((b -> c -> a) -> c -> b -> a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip b -> c -> a
    abc)

    -- | 'Identity' is the unit of 'Day' convolution
    --
    -- @
    -- 'intro1' '.' 'elim1' = 'id'
    -- 'elim1' '.' 'intro1' = 'id'
    -- @
    intro1 :: f a -> Day Identity f a
    intro1 :: forall (f :: * -> *) a. f a -> Day Identity f a
    intro1 f a
    fa = Identity () -> f a -> (() -> a -> a) -> Day Identity f a
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day (() -> Identity ()
    forall a. a -> Identity a
    Identity ()) f a
    fa ((() -> a -> a) -> Day Identity f a)
    -> (() -> a -> a) -> Day Identity f a
    forall a b. (a -> b) -> a -> b
    $ \()
    _ a
    a -> a
    a

    -- | 'Identity' is the unit of 'Day' convolution
    --
    -- @
    -- 'intro2' '.' 'elim2' = 'id'
    -- 'elim2' '.' 'intro2' = 'id'
    -- @
    intro2 :: f a -> Day f Identity a
    intro2 :: forall (f :: * -> *) a. f a -> Day f Identity a
    intro2 f a
    fa = f a -> Identity () -> (a -> () -> a) -> Day f Identity a
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day f a
    fa (() -> Identity ()
    forall a. a -> Identity a
    Identity ()) a -> () -> a
    forall a b. a -> b -> a
    const

    -- | 'Identity' is the unit of 'Day' convolution
    --
    -- @
    -- 'intro1' '.' 'elim1' = 'id'
    -- 'elim1' '.' 'intro1' = 'id'
    -- @
    elim1 :: Functor f => Day Identity f a -> f a
    elim1 :: forall (f :: * -> *) a. Functor f => Day Identity f a -> f a
    elim1 (Day (Identity b
    b) f c
    fc b -> c -> a
    bca) = b -> c -> a
    bca b
    b (c -> a) -> f c -> f a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f c
    fc

    -- | 'Identity' is the unit of 'Day' convolution
    --
    -- @
    -- 'intro2' '.' 'elim2' = 'id'
    -- 'elim2' '.' 'intro2' = 'id'
    -- @
    elim2 :: Functor f => Day f Identity a -> f a
    elim2 :: forall (f :: * -> *) a. Functor f => Day f Identity a -> f a
    elim2 (Day f b
    fb (Identity c
    c) b -> c -> a
    bca) = (b -> c -> a) -> c -> b -> a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip b -> c -> a
    bca c
    c (b -> a) -> f b -> f a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f b
    fb

    -- | Collapse via a monoidal functor.
    --
    -- @
    -- 'dap' ('day' f g) = f '<*>' g
    -- @
    dap :: Applicative f => Day f f a -> f a
    dap :: forall (f :: * -> *) a. Applicative f => Day f f a -> f a
    dap (Day f b
    fb f c
    fc b -> c -> a
    abc) = (b -> c -> a) -> f b -> f c -> f a
    forall a b c. (a -> b -> c) -> f a -> f b -> f c
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 b -> c -> a
    abc f b
    fb f c
    fc

    -- | Apply a natural transformation to the left-hand side of a Day convolution.
    --
    -- This respects the naturality of the natural transformation you supplied:
    --
    -- @
    -- 'fmap' f '.' 'trans1' fg = 'trans1' fg '.' 'fmap' f
    -- @
    trans1 :: (forall x. f x -> g x) -> Day f h a -> Day g h a
    trans1 :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a.
    (forall x. f x -> g x) -> Day f h a -> Day g h a
    trans1 forall x. f x -> g x
    fg (Day f b
    fb h c
    hc b -> c -> a
    bca) = g b -> h c -> (b -> c -> a) -> Day g h a
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day (f b -> g b
    forall x. f x -> g x
    fg f b
    fb) h c
    hc b -> c -> a
    bca

    -- | Apply a natural transformation to the right-hand side of a Day convolution.
    --
    -- This respects the naturality of the natural transformation you supplied:
    --
    -- @
    -- 'fmap' f '.' 'trans2' fg = 'trans2' fg '.' 'fmap' f
    -- @
    trans2 :: (forall x. g x -> h x) -> Day f g a -> Day f h a
    trans2 :: forall (g :: * -> *) (h :: * -> *) (f :: * -> *) a.
    (forall x. g x -> h x) -> Day f g a -> Day f h a
    trans2 forall x. g x -> h x
    gh (Day f b
    fb g c
    gc b -> c -> a
    bca) = f b -> h c -> (b -> c -> a) -> Day f h a
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day f b
    fb (g c -> h c
    forall x. g x -> h x
    gh g c
    gc) b -> c -> a
    bca

    cayley :: Procompose (Cayley f p) (Cayley g q) a b -> Cayley (Day f g) (Procompose p q) a b
    cayley :: forall (f :: * -> *) (p :: * -> * -> *) (g :: * -> *)
           (q :: * -> * -> *) a b.
    Procompose (Cayley f p) (Cayley g q) a b
    -> Cayley (Day f g) (Procompose p q) a b
    cayley (Procompose (Cayley f (p x b)
    p) (Cayley g (q a x)
    q)) = Day f g (Procompose p q a b)
    -> Cayley (Day f g) (Procompose p q) a b
    forall {k} {k1} {k2} (f :: k -> *) (p :: k1 -> k2 -> k) (a :: k1)
           (b :: k2).
    f (p a b) -> Cayley f p a b
    Cayley (Day f g (Procompose p q a b)
     -> Cayley (Day f g) (Procompose p q) a b)
    -> Day f g (Procompose p q a b)
    -> Cayley (Day f g) (Procompose p q) a b
    forall a b. (a -> b) -> a -> b
    $ f (p x b)
    -> g (q a x)
    -> (p x b -> q a x -> Procompose p q a b)
    -> Day f g (Procompose p q a b)
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day f (p x b)
    p g (q a x)
    q p x b -> q a x -> Procompose p q a b
    forall {k} {k1} {k2} (p :: k -> k1 -> *) (x :: k) (c :: k1)
           (q :: k2 -> k -> *) (d :: k2).
    p x c -> q d x -> Procompose p q d c
    Procompose

    -- | Proposition 4.1 from Pastro and Street
    dayley :: Category p => Procompose (Cayley f p) (Cayley g p) a b -> Cayley (Day f g) p a b
    dayley :: forall (p :: * -> * -> *) (f :: * -> *) (g :: * -> *) a b.
    Category p =>
    Procompose (Cayley f p) (Cayley g p) a b -> Cayley (Day f g) p a b
    dayley (Procompose (Cayley f (p x b)
    p) (Cayley g (p a x)
    q)) = Day f g (p a b) -> Cayley (Day f g) p a b
    forall {k} {k1} {k2} (f :: k -> *) (p :: k1 -> k2 -> k) (a :: k1)
           (b :: k2).
    f (p a b) -> Cayley f p a b
    Cayley (Day f g (p a b) -> Cayley (Day f g) p a b)
    -> Day f g (p a b) -> Cayley (Day f g) p a b
    forall a b. (a -> b) -> a -> b
    $ f (p x b)
    -> g (p a x) -> (p x b -> p a x -> p a b) -> Day f g (p a b)
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day f (p x b)
    p g (p a x)
    q p x b -> p a x -> p a b
    forall b c a. p b c -> p a b -> p a c
    forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    (.)