{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RequiredTypeArguments #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Category.Instance.Kleisli
  ( KLEISLI (..)
  , Kleisli (..)
  , arr
  , KleisliFree (..)
  , KleisliForget (..)
  , LIFTEDF
  , pattern LiftF
  ) where

import Proarrow.Adjunction (Adjunction)
import Proarrow.Adjunction qualified as Adj
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), Strong (..))
import Proarrow.Category.Monoidal.Distributive (Distributive (..), DistributiveProfunctor)
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Is
  , Profunctor (..)
  , Promonad (..)
  , UN
  , dimapDefault
  , lmap
  , rmap
  , type (+->)
  )
import Proarrow.Functor (Functor)
import Proarrow.Object (pattern Obj, type Obj)
import Proarrow.Object.BinaryCoproduct (Coprod, HasBinaryCoproducts (..), codiag, copar)
import Proarrow.Object.BinaryProduct (Cartesian, HasBinaryProducts (..), diag)
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Costar (Costar (..))
import Proarrow.Profunctor.Star (Star (..))

newtype KLEISLI (p :: CAT k) = KL k
type instance UN KL (KL k) = k -- test

type Kleisli :: CAT (KLEISLI p)
data Kleisli (a :: KLEISLI p) b where
  Kleisli :: {forall {k} (p :: CAT k) (b :: k) (b :: k).
Kleisli ('KL b) ('KL b) -> p b b
runKleisli :: p a b} -> Kleisli (KL a :: KLEISLI p) (KL b)

instance (Promonad p) => Profunctor (Kleisli :: CAT (KLEISLI p)) where
  dimap :: forall (c :: KLEISLI p) (a :: KLEISLI p) (b :: KLEISLI p)
       (d :: KLEISLI p).
(c ~> a) -> (b ~> d) -> Kleisli a b -> Kleisli c d
dimap = (c ~> a) -> (b ~> d) -> Kleisli a b -> Kleisli c d
Kleisli c a -> Kleisli b d -> Kleisli a b -> Kleisli c d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: KLEISLI p) (b :: KLEISLI p) r.
((Ob a, Ob b) => r) -> Kleisli a b -> r
\\ Kleisli p a b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

arr :: (Promonad p) => a ~> b -> Kleisli (KL a :: KLEISLI p) (KL b)
arr :: forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr a ~> b
f = p a b -> Kleisli ('KL a) ('KL b)
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli ('KL b) ('KL b)
Kleisli ((a ~> b) -> p a a -> p a b
forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap a ~> b
f p a a
forall (a :: k). Ob a => p a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id) ((Ob a, Ob b) => Kleisli ('KL a) ('KL b))
-> (a ~> b) -> Kleisli ('KL a) ('KL b)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f

-- | Every promonad makes a category.
instance (Promonad p) => CategoryOf (KLEISLI p) where
  type (~>) = Kleisli
  type Ob a = (Is KL a, Ob (UN KL a))

instance (Promonad p) => Promonad (Kleisli :: CAT (KLEISLI p)) where
  id :: forall (a :: KLEISLI p). Ob a => Kleisli a a
id = p (UN 'KL a) (UN 'KL a)
-> Kleisli ('KL (UN 'KL a)) ('KL (UN 'KL a))
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli ('KL b) ('KL b)
Kleisli p (UN 'KL a) (UN 'KL a)
forall (a :: k). Ob a => p a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  Kleisli p a b
f . :: forall (b :: KLEISLI p) (c :: KLEISLI p) (a :: KLEISLI p).
Kleisli b c -> Kleisli a b -> Kleisli a c
. Kleisli p a b
g = p a b -> Kleisli ('KL a) ('KL b)
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli ('KL b) ('KL b)
Kleisli (p a b
f p a b -> p a a -> p a b
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p a c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a a
p a b
g)

instance (HasTerminalObject k, Promonad p) => HasTerminalObject (KLEISLI (p :: k +-> k)) where
  type TerminalObject @(KLEISLI (p :: k +-> k)) = KL (TerminalObject :: k)
  terminate :: forall (a :: KLEISLI p). Ob a => a ~> TerminalObject
terminate = (UN 'KL a ~> TerminalObject)
-> Kleisli ('KL (UN 'KL a)) ('KL TerminalObject)
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr UN 'KL a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate

instance (HasInitialObject k, Promonad p) => HasInitialObject (KLEISLI (p :: k +-> k)) where
  type InitialObject @(KLEISLI (p :: k +-> k)) = KL (InitialObject :: k)
  initiate :: forall (a :: KLEISLI p). Ob a => InitialObject ~> a
initiate = (InitialObject ~> UN 'KL a)
-> Kleisli ('KL InitialObject) ('KL (UN 'KL a))
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr InitialObject ~> UN 'KL a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate

instance (Cartesian k, Promonad p, MonoidalProfunctor p) => HasBinaryProducts (KLEISLI (p :: k +-> k)) where
  type a && b = KL (UN KL a && UN KL b)
  withObProd :: forall (a :: KLEISLI p) (b :: KLEISLI p) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @(KL a) @(KL b) Ob (a && b) => r
r = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @a @b r
Ob (UN 'KL a && UN 'KL b) => r
Ob (a && b) => r
r
  fst :: forall (a :: KLEISLI p) (b :: KLEISLI p).
(Ob a, Ob b) =>
(a && b) ~> a
fst @(KL a) @(KL b) = ((UN 'KL a && UN 'KL b) ~> UN 'KL a)
-> Kleisli ('KL (UN 'KL a && UN 'KL b)) ('KL (UN 'KL a))
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @a @b)
  snd :: forall (a :: KLEISLI p) (b :: KLEISLI p).
(Ob a, Ob b) =>
(a && b) ~> b
snd @(KL a) @(KL b) = ((UN 'KL a && UN 'KL b) ~> UN 'KL b)
-> Kleisli ('KL (UN 'KL a && UN 'KL b)) ('KL (UN 'KL b))
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @a @b)
  Kleisli p a b
f &&& :: forall (a :: KLEISLI p) (x :: KLEISLI p) (y :: KLEISLI p).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Kleisli p a b
g = p a (b && b) -> Kleisli ('KL a) ('KL (b && b))
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli ('KL b) ('KL b)
Kleisli ((a ~> (a && a)) -> p (a && a) (b && b) -> p a (b && b)
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> (a && a)
forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
diag (p a b
f p a b -> p a b -> p (a ** a) (b ** b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` p a b
p a b
g)) ((Ob a, Ob b) => Kleisli ('KL a) ('KL (b && b)))
-> p a b -> Kleisli ('KL a) ('KL (b && b))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
f

instance (HasBinaryCoproducts k, Promonad p, MonoidalProfunctor (Coprod p)) => HasBinaryCoproducts (KLEISLI (p :: k +-> k)) where
  type a || b = KL (UN KL a || UN KL b)
  withObCoprod :: forall (a :: KLEISLI p) (b :: KLEISLI p) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @(KL a) @(KL b) Ob (a || b) => r
r = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a @b r
Ob (UN 'KL a || UN 'KL b) => r
Ob (a || b) => r
r
  lft :: forall (a :: KLEISLI p) (b :: KLEISLI p).
(Ob a, Ob b) =>
a ~> (a || b)
lft @(KL a) @(KL b) = (UN 'KL a ~> (UN 'KL a || UN 'KL b))
-> Kleisli ('KL (UN 'KL a)) ('KL (UN 'KL a || UN 'KL b))
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @a @b)
  rgt :: forall (a :: KLEISLI p) (b :: KLEISLI p).
(Ob a, Ob b) =>
b ~> (a || b)
rgt @(KL a) @(KL b) = (UN 'KL b ~> (UN 'KL a || UN 'KL b))
-> Kleisli ('KL (UN 'KL b)) ('KL (UN 'KL a || UN 'KL b))
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @a @b)
  Kleisli p a b
f ||| :: forall (x :: KLEISLI p) (a :: KLEISLI p) (y :: KLEISLI p).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Kleisli p a b
g = p (a || a) b -> Kleisli ('KL (a || a)) ('KL b)
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli ('KL b) ('KL b)
Kleisli (((b || b) ~> b) -> p (a || a) (b || b) -> p (a || a) b
forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap (b || b) ~> b
forall {k} (a :: k). (HasBinaryCoproducts k, Ob a) => (a || a) ~> a
codiag (p a b
f p a b -> p a b -> p (a || a) (b || b)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) (c :: k2)
       (d :: k1).
MonoidalProfunctor (Coprod p) =>
p a b -> p c d -> p (a || c) (b || d)
`copar` p a b
p a b
g)) ((Ob a, Ob b) => Kleisli ('KL (a || a)) ('KL b))
-> p a b -> Kleisli ('KL (a || a)) ('KL b)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
f

instance (Promonad p, MonoidalProfunctor p) => MonoidalProfunctor (Kleisli :: CAT (KLEISLI (p :: k +-> k))) where
  par0 :: Kleisli Unit Unit
par0 = p Unit Unit -> Kleisli ('KL Unit) ('KL Unit)
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli ('KL b) ('KL b)
Kleisli p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0
  Kleisli p a b
f par :: forall (x1 :: KLEISLI p) (x2 :: KLEISLI p) (y1 :: KLEISLI p)
       (y2 :: KLEISLI p).
Kleisli x1 x2 -> Kleisli y1 y2 -> Kleisli (x1 ** y1) (x2 ** y2)
`par` Kleisli p a b
g = p (a ** a) (b ** b) -> Kleisli ('KL (a ** a)) ('KL (b ** b))
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli ('KL b) ('KL b)
Kleisli (p a b
f p a b -> p a b -> p (a ** a) (b ** b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` p a b
g)

instance (Promonad p, MonoidalProfunctor p) => Monoidal (KLEISLI (p :: k +-> k)) where
  type Unit @(KLEISLI (p :: k +-> k)) = KL (Unit :: k)
  type a ** b = KL (UN KL a ** UN KL b)
  withOb2 :: forall (a :: KLEISLI p) (b :: KLEISLI p) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @(KL a) @(KL b) = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @b
  leftUnitor :: forall (a :: KLEISLI p). Ob a => (Unit ** a) ~> a
leftUnitor = ((Unit ** UN 'KL a) ~> UN 'KL a)
-> Kleisli ('KL (Unit ** UN 'KL a)) ('KL (UN 'KL a))
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr (Unit ** UN 'KL a) ~> UN 'KL a
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor
  leftUnitorInv :: forall (a :: KLEISLI p). Ob a => a ~> (Unit ** a)
leftUnitorInv = (UN 'KL a ~> (Unit ** UN 'KL a))
-> Kleisli ('KL (UN 'KL a)) ('KL (Unit ** UN 'KL a))
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr UN 'KL a ~> (Unit ** UN 'KL a)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv
  rightUnitor :: forall (a :: KLEISLI p). Ob a => (a ** Unit) ~> a
rightUnitor = ((UN 'KL a ** Unit) ~> UN 'KL a)
-> Kleisli ('KL (UN 'KL a ** Unit)) ('KL (UN 'KL a))
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr (UN 'KL a ** Unit) ~> UN 'KL a
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor
  rightUnitorInv :: forall (a :: KLEISLI p). Ob a => a ~> (a ** Unit)
rightUnitorInv = (UN 'KL a ~> (UN 'KL a ** Unit))
-> Kleisli ('KL (UN 'KL a)) ('KL (UN 'KL a ** Unit))
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr UN 'KL a ~> (UN 'KL a ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv
  associator :: forall (a :: KLEISLI p) (b :: KLEISLI p) (c :: KLEISLI p).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(KL a) @(KL b) @(KL c) = (((UN 'KL a ** UN 'KL b) ** UN 'KL c)
 ~> (UN 'KL a ** (UN 'KL b ** UN 'KL c)))
-> Kleisli
     ('KL ((UN 'KL a ** UN 'KL b) ** UN 'KL c))
     ('KL (UN 'KL a ** (UN 'KL b ** UN 'KL c)))
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @a @b @c)
  associatorInv :: forall (a :: KLEISLI p) (b :: KLEISLI p) (c :: KLEISLI p).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(KL a) @(KL b) @(KL c) = ((UN 'KL a ** (UN 'KL b ** UN 'KL c))
 ~> ((UN 'KL a ** UN 'KL b) ** UN 'KL c))
-> Kleisli
     ('KL (UN 'KL a ** (UN 'KL b ** UN 'KL c)))
     ('KL ((UN 'KL a ** UN 'KL b) ** UN 'KL c))
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @a @b @c)
instance (Promonad p, MonoidalProfunctor p, SymMonoidal k) => SymMonoidal (KLEISLI (p :: k +-> k)) where
  swap :: forall (a :: KLEISLI p) (b :: KLEISLI p).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @(KL a) @(KL b) = ((UN 'KL a ** UN 'KL b) ~> (UN 'KL b ** UN 'KL a))
-> Kleisli
     ('KL (UN 'KL a ** UN 'KL b)) ('KL (UN 'KL b ** UN 'KL a))
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @a @b)

instance (Distributive k, Promonad p, DistributiveProfunctor p) => Distributive (KLEISLI (p :: k +-> k)) where
  distL :: forall (a :: KLEISLI p) (b :: KLEISLI p) (c :: KLEISLI p).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @(KL a) @(KL b) @(KL c) = ((UN 'KL a ** (UN 'KL b || UN 'KL c))
 ~> ((UN 'KL a ** UN 'KL b) || (UN 'KL a ** UN 'KL c)))
-> Kleisli
     ('KL (UN 'KL a ** (UN 'KL b || UN 'KL c)))
     ('KL ((UN 'KL a ** UN 'KL b) || (UN 'KL a ** UN 'KL c)))
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr (forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @k @a @b @c)
  distR :: forall (a :: KLEISLI p) (b :: KLEISLI p) (c :: KLEISLI p).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @(KL a) @(KL b) @(KL c) = (((UN 'KL a || UN 'KL b) ** UN 'KL c)
 ~> ((UN 'KL a ** UN 'KL c) || (UN 'KL b ** UN 'KL c)))
-> Kleisli
     ('KL ((UN 'KL a || UN 'KL b) ** UN 'KL c))
     ('KL ((UN 'KL a ** UN 'KL c) || (UN 'KL b ** UN 'KL c)))
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr (forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @k @a @b @c)
  distL0 :: forall (a :: KLEISLI p).
Ob a =>
(a ** InitialObject) ~> InitialObject
distL0 @(KL a) = ((UN 'KL a ** InitialObject) ~> InitialObject)
-> Kleisli ('KL (UN 'KL a ** InitialObject)) ('KL InitialObject)
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr (forall k (a :: k).
(Distributive k, Ob a) =>
(a ** InitialObject) ~> InitialObject
distL0 @k @a)
  distR0 :: forall (a :: KLEISLI p).
Ob a =>
(InitialObject ** a) ~> InitialObject
distR0 @(KL a) = ((InitialObject ** UN 'KL a) ~> InitialObject)
-> Kleisli ('KL (InitialObject ** UN 'KL a)) ('KL InitialObject)
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr (forall k (a :: k).
(Distributive k, Ob a) =>
(InitialObject ** a) ~> InitialObject
distR0 @k @a)

instance (Strong k p, Promonad p, Monoidal k) => Strong k (Kleisli :: CAT (KLEISLI (p :: k +-> k))) where
  act :: forall (a :: k) (b :: k) (x :: KLEISLI p) (y :: KLEISLI p).
(a ~> b) -> Kleisli x y -> Kleisli (Act a x) (Act b y)
act a ~> b
f (Kleisli p a b
p) = p (Act a a) (Act b b) -> Kleisli ('KL (Act a a)) ('KL (Act b b))
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli ('KL b) ('KL b)
Kleisli ((a ~> b) -> p a b -> p (Act a a) (Act b b)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> b) -> p x y -> p (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act a ~> b
f p a b
p)
instance (Strong k p, Promonad p, Monoidal k) => MonoidalAction k (KLEISLI (p :: k +-> k)) where
  type Act y (KL x) = KL (Act y x)
  withObAct :: forall (a :: k) (x :: KLEISLI p) r.
(Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @y @(KL x) Ob (Act a x) => r
r = forall m k (a :: m) (x :: k) r.
(MonoidalAction m k, Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @k @k @y @x r
Ob (Act a (UN 'KL x)) => r
Ob (Act a x) => r
r
  unitor :: forall (x :: KLEISLI p). Ob x => Act Unit x ~> x
unitor = (Act Unit (UN 'KL x) ~> UN 'KL x)
-> Kleisli ('KL (Act Unit (UN 'KL x))) ('KL (UN 'KL x))
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr (forall m k (x :: k). (MonoidalAction m k, Ob x) => Act Unit x ~> x
unitor @k)
  unitorInv :: forall (x :: KLEISLI p). Ob x => x ~> Act Unit x
unitorInv = (UN 'KL x ~> Act Unit (UN 'KL x))
-> Kleisli ('KL (UN 'KL x)) ('KL (Act Unit (UN 'KL x)))
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr (forall m k (x :: k). (MonoidalAction m k, Ob x) => x ~> Act Unit x
unitorInv @k)
  multiplicator :: forall (a :: k) (b :: k) (x :: KLEISLI p).
(Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator @a @b @(KL c) = (Act a (Act b (UN 'KL x)) ~> Act (a ** b) (UN 'KL x))
-> Kleisli
     ('KL (Act a (Act b (UN 'KL x)))) ('KL (Act (a ** b) (UN 'KL x)))
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr (forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator @k @k @a @b @c)
  multiplicatorInv :: forall (a :: k) (b :: k) (x :: KLEISLI p).
(Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv @a @b @(KL c) = (Act (a ** b) (UN 'KL x) ~> Act a (Act b (UN 'KL x)))
-> Kleisli
     ('KL (Act (a ** b) (UN 'KL x))) ('KL (Act a (Act b (UN 'KL x))))
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli ('KL a) ('KL b)
arr (forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv @k @k @a @b @c)

type KleisliFree :: forall (p :: k +-> k) -> k +-> KLEISLI p
data KleisliFree p a b where
  KleisliFree :: p a b -> KleisliFree p (KL a) b
instance (Promonad p) => Profunctor (KleisliFree p) where
  dimap :: forall (c :: KLEISLI p) (a :: KLEISLI p) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> KleisliFree p a b -> KleisliFree p c d
dimap (Kleisli p a b
l) b ~> d
r (KleisliFree p a b
p) = p a d -> KleisliFree p ('KL a) d
forall {k} (p :: k +-> k) (b :: k) (b :: k).
p b b -> KleisliFree p ('KL b) b
KleisliFree ((b ~> d) -> p a b -> p a d
forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> d
r p a b
p p a d -> p a a -> p a d
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p a c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a b
p a a
l)
  (Ob a, Ob b) => r
r \\ :: forall (a :: KLEISLI p) (b :: k) r.
((Ob a, Ob b) => r) -> KleisliFree p a b -> r
\\ KleisliFree p a b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

type KleisliForget :: forall (p :: k +-> k) -> KLEISLI p +-> k
data KleisliForget p a b where
  KleisliForget :: p a b -> KleisliForget p a (KL b)
instance (Promonad p) => Profunctor (KleisliForget p) where
  dimap :: forall (c :: j) (a :: j) (b :: KLEISLI p) (d :: KLEISLI p).
(c ~> a) -> (b ~> d) -> KleisliForget p a b -> KleisliForget p c d
dimap c ~> a
l (Kleisli p a b
r) (KleisliForget p a b
p) = p c b -> KleisliForget p c ('KL b)
forall {k} (p :: k +-> k) (a :: k) (b :: k).
p a b -> KleisliForget p a ('KL b)
KleisliForget (p a b
p b b
r p b b -> p c b -> p c b
forall (b :: j) (c :: j) (a :: j). p b c -> p a b -> p a c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap c ~> a
l p a b
p)
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: KLEISLI p) r.
((Ob a, Ob b) => r) -> KleisliForget p a b -> r
\\ KleisliForget p a b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

instance (Promonad p) => Adjunction (KleisliFree p) (KleisliForget p) where
  unit :: forall (a :: k).
Ob a =>
(:.:) (KleisliForget p) (KleisliFree p) a a
unit = p a a -> KleisliForget p a ('KL a)
forall {k} (p :: k +-> k) (a :: k) (b :: k).
p a b -> KleisliForget p a ('KL b)
KleisliForget p a a
forall (a :: k). Ob a => p a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id KleisliForget p a ('KL a)
-> KleisliFree p ('KL a) a
-> (:.:) (KleisliForget p) (KleisliFree p) a a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p a a -> KleisliFree p ('KL a) a
forall {k} (p :: k +-> k) (b :: k) (b :: k).
p b b -> KleisliFree p ('KL b) b
KleisliFree p a a
forall (a :: k). Ob a => p a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  counit :: (KleisliFree p :.: KleisliForget p) :~> (~>)
counit (KleisliFree p a b
p :.: KleisliForget p b b
q) = p a b -> Kleisli ('KL a) ('KL b)
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli ('KL b) ('KL b)
Kleisli (p b b
q p b b -> p a b -> p a b
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p a c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a b
p)

-- | Categories lifted by a functor: @f a ~> f b@.
type LIFTEDF (f :: j -> k) = KLEISLI (Costar f :.: Star f)

unlift :: (Functor f) => Kleisli (KL a :: LIFTEDF f) (KL b) -> (f a ~> f b, Obj a, Obj b)
unlift :: forall {k} {k} (f :: k -> k) (a :: k) (b :: k).
Functor f =>
Kleisli ('KL a) ('KL b) -> (f a ~> f b, Obj a, Obj b)
unlift (Kleisli (Costar f a ~> b
f :.: Star b ~> f b
g)) = (b ~> f b
b ~> f b
g (b ~> f b) -> (f a ~> b) -> f a ~> f b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. f a ~> b
f a ~> b
f, Obj a
forall k (a :: k). (CategoryOf k, Ob a) => Obj a
Obj, Obj b
forall k (a :: k). (CategoryOf k, Ob a) => Obj a
Obj)

pattern LiftF :: (Functor f) => (Ob a, Ob b) => (f a ~> f b) -> Kleisli (KL a :: LIFTEDF f) (KL b)
pattern $mLiftF :: forall {r} {k1} {k2} {f :: k1 -> k2} {a :: k1} {b :: k1}.
Functor f =>
Kleisli ('KL a) ('KL b)
-> ((Ob a, Ob b) => (f a ~> f b) -> r) -> ((# #) -> r) -> r
$bLiftF :: forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
(Functor f, Ob a, Ob b) =>
(f a ~> f b) -> Kleisli ('KL a) ('KL b)
LiftF f <- (unlift -> (f, Obj, Obj))
  where
    LiftF f a ~> f b
f = (:.:) (Costar f) (Star f) a b -> Kleisli ('KL a) ('KL b)
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli ('KL b) ('KL b)
Kleisli ((f a ~> f b) -> Costar f a (f b)
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar f a ~> f b
f Costar f a (f b) -> Star f (f b) b -> (:.:) (Costar f) (Star f) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (f b ~> f b) -> Star f (f b) b
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star f b ~> f b
forall (a :: k2). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)

{-# COMPLETE LiftF #-}