{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE RankNTypes #-}
-----------------------------------------------------------------------------
-- |
-- 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.Identity
import Data.Functor.Rep
#ifdef __GLASGOW_HASKELL__
import Data.Typeable
#endif
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)
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
  deriving Typeable
#endif

-- | 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

#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 707
instance (Typeable1 f, Typeable1 g) => Typeable1 (Day f g) where
    typeOf1 tfga = mkTyConApp dayTyCon [typeOf1 (fa tfga), typeOf1 (ga tfga)]
        where fa :: t f (g :: * -> *) a -> f a
              fa = undefined
              ga :: t (f :: * -> *) g a -> g a
              ga = undefined

dayTyCon :: TyCon
#if MIN_VERSION_base(4,4,0)
dayTyCon = mkTyCon3 "contravariant" "Data.Functor.Day" "Day"
#else
dayTyCon = mkTyCon "Data.Functor.Day.Day"
#endif

#endif

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 (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
(.)