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

module Proarrow.Category.Instance.Kleisli where

import Proarrow.Adjunction (Adjunction)
import Proarrow.Adjunction qualified as Adj
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), Strong (..))
import Proarrow.Category.Monoidal.Distributive (distL)
import Proarrow.Category.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Is
  , Profunctor (..)
  , Promonad (..)
  , UN
  , dimapDefault
  , lmap
  , rmap
  , type (+->)
  )
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..), codiag)
import Proarrow.Object.BinaryProduct
  ( HasBinaryProducts (..)
  , PROD (..)
  , Prod (..)
  , StrongProd
  , associatorProd
  , associatorProdInv
  , diag
  , first'
  , leftUnitorProd
  , leftUnitorProdInv
  , rightUnitorProd
  , rightUnitorProdInv
  , second'
  )
import Proarrow.Object.Exponential (BiCCC)
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Composition ((:.:) (..))

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

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 (forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id @p)
  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)

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)

-- | This is not monoidal but premonoidal, i.e. no sliding.
-- So with `par f g` the effects of f happen before the effects of g.
instance (Promonad p, StrongProd p) => MonoidalProfunctor (Kleisli :: CAT (KLEISLI (p :: k +-> k))) where
  par0 :: Kleisli Unit Unit
par0 = p TerminalObject TerminalObject
-> Kleisli ('KL TerminalObject) ('KL TerminalObject)
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli ('KL b) ('KL b)
Kleisli p TerminalObject TerminalObject
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 @_ @_ @b1 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 @_ @a2 @_ 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 (forall {k} (p :: CAT k) (c :: k) (a :: k) (b :: k).
(StrongProd p, Ob c) =>
p a b -> p (c && a) (c && b)
forall (p :: PRO k k) (c :: k) (a :: k) (b :: k).
(StrongProd p, Ob c) =>
p a b -> p (c && a) (c && b)
second' @_ @b1 p a b
g p (b && a) (b && b) -> p (a && a) (b && a) -> p (a && a) (b && 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
. forall {k} (p :: CAT k) (c :: k) (a :: k) (b :: k).
(StrongProd p, Ob c) =>
p a b -> p (a && c) (b && c)
forall (p :: PRO k k) (c :: k) (a :: k) (b :: k).
(StrongProd p, Ob c) =>
p a b -> p (a && c) (b && c)
first' @_ @a2 p a b
f) ((Ob a, Ob b) => Kleisli ('KL (a && a)) ('KL (b && b)))
-> p a b -> Kleisli ('KL (a && 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 ((Ob a, Ob b) => Kleisli ('KL (a && a)) ('KL (b && b)))
-> p a b -> Kleisli ('KL (a && 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
g

instance (Promonad p, StrongProd p) => Monoidal (KLEISLI (p :: k +-> k)) where
  type Unit @(KLEISLI (p :: k +-> k)) = KL (TerminalObject :: k)
  type a ** b = KL (UN KL a && UN KL b)
  leftUnitor :: forall (a :: KLEISLI p). Ob a => (Unit ** a) ~> a
leftUnitor = ((TerminalObject && UN 'KL a) ~> UN 'KL a)
-> Kleisli ('KL (TerminalObject && 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 (TerminalObject && UN 'KL a) ~> UN 'KL a
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(TerminalObject && a) ~> a
leftUnitorProd
  leftUnitorInv :: forall (a :: KLEISLI p). Ob a => a ~> (Unit ** a)
leftUnitorInv = (UN 'KL a ~> (TerminalObject && UN 'KL a))
-> Kleisli ('KL (UN 'KL a)) ('KL (TerminalObject && 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 ~> (TerminalObject && UN 'KL a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (TerminalObject && a)
leftUnitorProdInv
  rightUnitor :: forall (a :: KLEISLI p). Ob a => (a ** Unit) ~> a
rightUnitor = ((UN 'KL a && TerminalObject) ~> UN 'KL a)
-> Kleisli ('KL (UN 'KL a && TerminalObject)) ('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 && TerminalObject) ~> UN 'KL a
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(a && TerminalObject) ~> a
rightUnitorProd
  rightUnitorInv :: forall (a :: KLEISLI p). Ob a => a ~> (a ** Unit)
rightUnitorInv = (UN 'KL a ~> (UN 'KL a && TerminalObject))
-> Kleisli ('KL (UN 'KL a)) ('KL (UN 'KL a && TerminalObject))
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 && TerminalObject)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (a && TerminalObject)
rightUnitorProdInv
  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 (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
associatorProd @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 (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
associatorProdInv @a @b @c)

instance (Strong w p, Strong ((~>) :: CAT k) p, Promonad p, Monoidal k) => Strong (w :: k +-> k) (Kleisli :: CAT (KLEISLI (p :: k +-> k))) where
  act :: forall (a :: k) (b :: k) (x :: KLEISLI p) (y :: KLEISLI p).
w a b -> Kleisli x y -> Kleisli (Act a x) (Act b y)
act w 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 (w a b -> p a b -> p (Act a a) (Act b b)
forall (a :: k) (b :: k) (x :: k) (y :: k).
w a b -> p x y -> p (Act a x) (Act b y)
forall {m} {m'} {c} {d} (w :: m +-> m') (p :: c +-> d) (a :: m')
       (b :: m) (x :: d) (y :: c).
Strong w p =>
w a b -> p x y -> p (Act a x) (Act b y)
act w a b
f p a b
p)
instance (Strong ((~>) :: CAT k) p, Promonad p, Monoidal k) => MonoidalAction k (KLEISLI (p :: k +-> k)) where
  type Act y (KL x) = KL (Act y x)
  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 DUAL (a :: KLEISLI p) = KL (OP (UN KL a)) :: KLEISLI (Op p)
type UNDUAL (a :: KLEISLI (Op p)) = KL (UN OP (UN KL a)) :: KLEISLI p
type (++) :: forall {k} {p}. KLEISLI (p :: k +-> k) -> KLEISLI p -> KLEISLI p
type (a :: KLEISLI p) ++ b = UNDUAL (DUAL a ** DUAL b)

dual :: a ~> b -> DUAL b ~> DUAL a
dual :: forall {k} {p :: CAT k} (a :: KLEISLI p) (b :: KLEISLI p).
(a ~> b) -> DUAL b ~> DUAL a
dual (Kleisli p a b
p) = Op p ('OP b) ('OP a) -> Kleisli ('KL ('OP b)) ('KL ('OP a))
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli ('KL b) ('KL b)
Kleisli (p a b -> Op p ('OP b) ('OP a)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op p a b
p)

dist
  :: forall {k} {p} a b c
   . (BiCCC k, Promonad p, Ob (a :: KLEISLI (p :: k +-> k)), Ob b, Ob c)
  => (a ** (b ++ c)) ~> ((a ** b) ++ (a ** c))
dist :: forall {k} {p :: PRO k k} (a :: KLEISLI p) (b :: KLEISLI p)
       (c :: KLEISLI p).
(BiCCC k, Promonad p, Ob a, Ob b, Ob c) =>
(a ** (b ++ c)) ~> ((a ** b) ++ (a ** c))
dist @(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 (Prod
  (~>)
  ('PR (UN 'KL a && (UN 'KL b || UN 'KL c)))
  ('PR ((UN 'KL a && UN 'KL b) || (UN 'KL a && UN 'KL c)))
-> (UN 'KL a && (UN 'KL b || UN 'KL c))
   ~> ((UN 'KL a && UN 'KL b) || (UN 'KL a && UN 'KL c))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Prod p ('PR a) ('PR b) -> p a b
unProd (forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @_ @(PR a') @(PR b') @(PR c')))

copy :: (HasBinaryProducts k, Promonad p, Ob (a :: KLEISLI (p :: k +-> k))) => a ~> (a ** a)
copy :: forall k (p :: PRO k k) (a :: KLEISLI p).
(HasBinaryProducts k, Promonad p, Ob a) =>
a ~> (a ** a)
copy = (UN 'KL a ~> (UN 'KL a && UN 'KL a))
-> Kleisli ('KL (UN 'KL a)) ('KL (UN 'KL a && 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 ~> (UN 'KL a && UN 'KL a)
forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
diag

discard :: (HasTerminalObject k, Promonad p, Ob (a :: KLEISLI (p :: k +-> k))) => a ~> Unit
discard :: forall k (p :: PRO k k) (a :: KLEISLI p).
(HasTerminalObject k, Promonad p, Ob a) =>
a ~> Unit
discard = (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

add :: (HasBinaryCoproducts k, Promonad p, Ob (a :: KLEISLI (p :: k +-> k))) => (a ++ a) ~> a
add :: forall k (p :: PRO k k) (a :: KLEISLI p).
(HasBinaryCoproducts k, Promonad p, Ob a) =>
(a ++ a) ~> a
add = ((UN 'KL a || UN 'KL a) ~> UN 'KL a)
-> Kleisli ('KL (UN 'KL a || 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 (UN 'KL a || UN 'KL a) ~> UN 'KL a
forall {k} (a :: k). (HasBinaryCoproducts k, Ob a) => (a || a) ~> a
codiag

zero :: (HasInitialObject k, Promonad p, Ob (a :: KLEISLI (p :: k +-> k))) => UNDUAL Unit ~> a
zero :: forall k (p :: PRO k k) (a :: KLEISLI p).
(HasInitialObject k, Promonad p, Ob a) =>
UNDUAL Unit ~> a
zero = (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