{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Monoidal.Distributive where

import Data.Bifunctor (bimap)
import Data.Kind (Constraint, Type)
import Prelude qualified as P

import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))
import Proarrow.Category.Monoidal.Action (SelfAction, Strong (..))
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Profunctor (..)
  , Promonad (..)
  , lmap
  , rmap
  , src
  , tgt
  , (:~>)
  , type (+->)
  )
import Proarrow.Object.BinaryCoproduct (Coprod (..), HasBinaryCoproducts (..), HasCoproducts, codiag, copar, lft', rgt')
import Proarrow.Object.BinaryProduct
  ( Cartesian
  , HasBinaryProducts (..)
  , PROD (..)
  , Prod (..)
  , diag
  , fst'
  , snd'
  , swapProd
  )
import Proarrow.Object.Exponential (BiCCC, Closed (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Coproduct ((:+:) (..))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Product ((:*:) (..))
import Prelude (($))

class (MonoidalProfunctor p, MonoidalProfunctor (Coprod p)) => DistributiveProfunctor p
instance (MonoidalProfunctor p, MonoidalProfunctor (Coprod p)) => DistributiveProfunctor p

class (Monoidal k, HasCoproducts k, DistributiveProfunctor (Id :: CAT k)) => Distributive k where
  distL :: (Ob (a :: k), Ob b, Ob c) => (a ** (b || c)) ~> (a ** b || a ** c)
  distR :: (Ob (a :: k), Ob b, Ob c) => ((a || b) ** c) ~> (a ** c || b ** c)
  distL0 :: (Ob (a :: k)) => (a ** InitialObject) ~> InitialObject
  distR0 :: (Ob (a :: k)) => (InitialObject ** a) ~> InitialObject

instance Distributive Type where
  distL :: forall a b c.
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL (a
a, Either b c
e) = (b -> (a, b))
-> (c -> (a, c)) -> Either b c -> Either (a, b) (a, c)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: Type -> Type -> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (a
a,) (a
a,) Either b c
e
  distR :: forall a b c.
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR (Either a b
e, c
c) = (a -> (a, c))
-> (b -> (b, c)) -> Either a b -> Either (a, c) (b, c)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: Type -> Type -> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (,c
c) (,c
c) Either a b
e
  distL0 :: forall a. Ob a => (a ** InitialObject) ~> InitialObject
distL0 = (a ** InitialObject) ~> InitialObject
(a, Void) -> Void
forall a b. (a, b) -> b
P.snd
  distR0 :: forall a. Ob a => (InitialObject ** a) ~> InitialObject
distR0 = (InitialObject ** a) ~> InitialObject
(Void, a) -> Void
forall a b. (a, b) -> a
P.fst

instance Distributive () where
  distL :: forall (a :: ()) (b :: ()) (c :: ()).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL = (a ** (b || c)) ~> ((a ** b) || (a ** c))
Unit '() '()
U.Unit
  distR :: forall (a :: ()) (b :: ()) (c :: ()).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR = ((a || b) ** c) ~> ((a ** c) || (b ** c))
Unit '() '()
U.Unit
  distL0 :: forall (a :: ()). Ob a => (a ** InitialObject) ~> InitialObject
distL0 = (a ** InitialObject) ~> InitialObject
Unit '() '()
U.Unit
  distR0 :: forall (a :: ()). Ob a => (InitialObject ** a) ~> InitialObject
distR0 = (InitialObject ** a) ~> InitialObject
Unit '() '()
U.Unit

instance (BiCCC k) => Distributive (PROD k) where
  distL :: forall (a :: PROD k) (b :: PROD k) (c :: PROD k).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @(PR a) @(PR b) @(PR c) = ((UN 'PR a && (UN 'PR b || UN 'PR c))
 ~> ((UN 'PR a && UN 'PR b) || (UN 'PR a && UN 'PR c)))
-> Prod
     (~>)
     ('PR (UN 'PR a && (UN 'PR b || UN 'PR c)))
     ('PR ((UN 'PR a && UN 'PR b) || (UN 'PR a && UN 'PR c)))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod (forall (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
forall {k} (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
distLProd @a @b @c)
  distR :: forall (a :: PROD k) (b :: PROD k) (c :: PROD k).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @(PR a) @(PR b) @(PR c) = (((UN 'PR a || UN 'PR b) && UN 'PR c)
 ~> ((UN 'PR a && UN 'PR c) || (UN 'PR b && UN 'PR c)))
-> Prod
     (~>)
     ('PR ((UN 'PR a || UN 'PR b) && UN 'PR c))
     ('PR ((UN 'PR a && UN 'PR c) || (UN 'PR b && UN 'PR c)))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod (forall (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
((a || b) && c) ~> ((a && c) || (b && c))
forall {k} (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
((a || b) && c) ~> ((a && c) || (b && c))
distRProd @a @b @c)
  distL0 :: forall (a :: PROD k). Ob a => (a ** InitialObject) ~> InitialObject
distL0 @(PR a) = ((UN 'PR a && InitialObject) ~> InitialObject)
-> Prod (~>) ('PR (UN 'PR a && InitialObject)) ('PR InitialObject)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @a)
  distR0 :: forall (a :: PROD k). Ob a => (InitialObject ** a) ~> InitialObject
distR0 @(PR a) = ((InitialObject && UN 'PR a) ~> InitialObject)
-> Prod (~>) ('PR (InitialObject && UN 'PR a)) ('PR InitialObject)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @_ @a)

distLProd :: forall {k} (a :: k) (b :: k) (c :: k). (BiCCC k, Ob a, Ob b, Ob c) => (a && (b || c)) ~> (a && b || a && c)
distLProd :: forall {k} (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
distLProd = (forall (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> (b && a)
forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> (b && a)
swapProd @b @a ((b && a) ~> (a && b))
-> ((c && a) ~> (a && c))
-> ((b && a) || (c && a)) ~> ((a && b) || (a && c))
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryCoproducts k =>
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
+++ forall (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> (b && a)
forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> (b && a)
swapProd @c @a) (((b && a) || (c && a)) ~> ((a && b) || (a && c)))
-> ((a && (b || c)) ~> ((b && a) || (c && a)))
-> (a && (b || c)) ~> ((a && b) || (a && c))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
((a || b) && c) ~> ((a && c) || (b && c))
forall {k} (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
((a || b) && c) ~> ((a && c) || (b && c))
distRProd @b @c @a (((b || c) && a) ~> ((b && a) || (c && a)))
-> ((a && (b || c)) ~> ((b || c) && a))
-> (a && (b || c)) ~> ((b && a) || (c && a))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @b @c (forall (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> (b && a)
forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> (b && a)
swapProd @a @(b || c))

distRProd :: forall {k} (a :: k) (b :: k) (c :: k). (BiCCC k, Ob a, Ob b, Ob c) => ((a || b) && c) ~> (a && c || b && c)
distRProd :: forall {k} (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
((a || b) && c) ~> ((a && c) || (b && c))
distRProd =
  forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @a @c ((Ob (a && c) => ((a || b) && c) ~> ((a && c) || (b && c)))
 -> ((a || b) && c) ~> ((a && c) || (b && c)))
-> (Ob (a && c) => ((a || b) && c) ~> ((a && c) || (b && c)))
-> ((a || b) && c) ~> ((a && c) || (b && c))
forall a b. (a -> b) -> a -> b
$
    forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @b @c ((Ob (b && c) => ((a || b) && c) ~> ((a && c) || (b && c)))
 -> ((a || b) && c) ~> ((a && c) || (b && c)))
-> (Ob (b && c) => ((a || b) && c) ~> ((a && c) || (b && c)))
-> ((a || b) && c) ~> ((a && c) || (b && c))
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @(a && c) @(b && c) ((Ob ((a && c) || (b && c)) =>
  ((a || b) && c) ~> ((a && c) || (b && c)))
 -> ((a || b) && c) ~> ((a && c) || (b && c)))
-> (Ob ((a && c) || (b && c)) =>
    ((a || b) && c) ~> ((a && c) || (b && c)))
-> ((a || b) && c) ~> ((a && c) || (b && c))
forall a b. (a -> b) -> a -> b
$
        forall k (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry @k @c (forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @a @c (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @(a && c) @(b && c)) (a ~> (c ~~> ((a && c) || (b && c))))
-> (b ~> (c ~~> ((a && c) || (b && c))))
-> (a || b) ~> (c ~~> ((a && c) || (b && c)))
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @b @c (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @(a && c) @(b && c)))

type Traversable :: forall {k}. (k +-> k) -> Constraint
class (Profunctor t) => Traversable (t :: k +-> k) where
  traverse :: (DistributiveProfunctor (p :: k +-> k), Strong k p, SelfAction k) => t :.: p :~> p :.: t

instance (CategoryOf k) => Traversable (Id :: k +-> k) where
  traverse :: forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(Id :.: p) :~> (p :.: Id)
traverse (Id a ~> b
f :.: p b b
p) = (a ~> b) -> p b b -> p a b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> b
f p b b
p p a b -> Id b b -> (:.:) p Id 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
:.: (b ~> b) -> Id b b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id ((Ob b, Ob b) => (:.:) p Id a b) -> p b b -> (:.:) p Id a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p b b
p

instance Traversable (->) where
  traverse :: forall (p :: Type -> Type -> Type).
(DistributiveProfunctor p, Strong Type p, SelfAction Type) =>
((->) :.: p) :~> (p :.: (->))
traverse (a -> b
f :.: p b b
p) = (a ~> b) -> p b b -> p a b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> b
a -> b
f p b b
p p a b -> (b -> b) -> (:.:) p (->) 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
:.: b -> b
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

instance (Traversable p, Traversable q) => Traversable (p :.: q) where
  traverse :: forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
((p :.: q) :.: p) :~> (p :.: (p :.: q))
traverse ((p a b
p :.: q b b
q) :.: p b b
r) = case (:.:) q p b b -> (:.:) p q b b
(q :.: p) :~> (p :.: q)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Traversable t, DistributiveProfunctor p, Strong k p,
 SelfAction k) =>
(t :.: p) :~> (p :.: t)
forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(q :.: p) :~> (p :.: q)
traverse (q b b
q q b b -> p b b -> (:.:) q p b 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
:.: p b b
r) of
    p b b
r' :.: q b b
q' -> case (:.:) p p a b -> (:.:) p p a b
(p :.: p) :~> (p :.: p)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Traversable t, DistributiveProfunctor p, Strong k p,
 SelfAction k) =>
(t :.: p) :~> (p :.: t)
forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(p :.: p) :~> (p :.: p)
traverse (p a b
p p a b -> p b b -> (:.:) p p 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
:.: p b b
r') of
      p a b
r'' :.: p b b
p' -> p a b
r'' p a b -> (:.:) p q b b -> (:.:) p (p :.: q) 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
:.: (p b b
p' p b b -> q b b -> (:.:) p q b 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
:.: q b b
q')

instance (Cartesian k, Traversable p, Traversable q) => Traversable ((p :: k +-> k) :*: q) where
  traverse :: forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
((p :*: q) :.: p) :~> (p :.: (p :*: q))
traverse ((p a b
p :*: q a b
q) :.: p b b
r) = case ((:.:) p p a b -> (:.:) p p a b
(p :.: p) :~> (p :.: p)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Traversable t, DistributiveProfunctor p, Strong k p,
 SelfAction k) =>
(t :.: p) :~> (p :.: t)
forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(p :.: p) :~> (p :.: p)
traverse (p a b
p p a b -> p b b -> (:.:) p p 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
:.: p b b
r), (:.:) q p a b -> (:.:) p q a b
(q :.: p) :~> (p :.: q)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Traversable t, DistributiveProfunctor p, Strong k p,
 SelfAction k) =>
(t :.: p) :~> (p :.: t)
forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(q :.: p) :~> (p :.: q)
traverse (q a b
q q a b -> p b b -> (:.:) q p 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
:.: p b b
r)) of
    (p a b
r' :.: p b b
p', p a b
r'' :.: q b b
q') -> (a ~> (a && a)) -> p (a && a) (b ** b) -> p a (b ** b)
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
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
r' 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
r'') p a (b ** b) -> (:*:) p q (b ** b) b -> (:.:) p (p :*: q) 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
:.: (((b ** b) ~> b) -> p b b -> p (b ** b) b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap ((b ~> b) -> Obj b -> (b && b) ~> b
forall {k} (a :: k) (a' :: k) (b :: k).
HasBinaryProducts k =>
(a ~> a') -> Obj b -> (a && b) ~> a'
fst' (p b b -> b ~> b
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src p b b
p') (q b b -> Obj b
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src q b b
q')) p b b
p' p (b ** b) b -> q (b ** b) b -> (:*:) p q (b ** b) b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> q a b -> (:*:) p q a b
:*: ((b ** b) ~> b) -> q b b -> q (b ** b) b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap ((b ~> b) -> Obj b -> (b && b) ~> b
forall {k} (a :: k) (b :: k) (b' :: k).
HasBinaryProducts k =>
Obj a -> (b ~> b') -> (a && b) ~> b'
snd' (p b b -> b ~> b
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src p b b
p') (q b b -> Obj b
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src q b b
q')) q b b
q') ((Ob a, Ob b) => (:.:) p (p :*: q) a b)
-> p a b -> (:.:) p (p :*: q) a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

instance (Traversable p, Traversable q) => Traversable (p :+: q) where
  traverse :: forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
((p :+: q) :.: p) :~> (p :.: (p :+: q))
traverse (InjL p a b
p :.: p b b
r) = case (:.:) p p a b -> (:.:) p p a b
(p :.: p) :~> (p :.: p)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Traversable t, DistributiveProfunctor p, Strong k p,
 SelfAction k) =>
(t :.: p) :~> (p :.: t)
forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(p :.: p) :~> (p :.: p)
traverse (p a b
p p a b -> p b b -> (:.:) p p 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
:.: p b b
r) of p a b
r' :.: p b b
p' -> p a b
r' p a b -> (:+:) p q b b -> (:.:) p (p :+: q) 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
:.: p b b -> (:+:) p q b b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> (:+:) p q a b
InjL p b b
p'
  traverse (InjR q a b
q :.: p b b
r) = case (:.:) q p a b -> (:.:) p q a b
(q :.: p) :~> (p :.: q)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Traversable t, DistributiveProfunctor p, Strong k p,
 SelfAction k) =>
(t :.: p) :~> (p :.: t)
forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(q :.: p) :~> (p :.: q)
traverse (q a b
q q a b -> p b b -> (:.:) q p 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
:.: p b b
r) of p a b
r' :.: q b b
q' -> p a b
r' p a b -> (:+:) p q b b -> (:.:) p (p :+: q) 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
:.: q b b -> (:+:) p q b b
forall {j} {k} (q :: j +-> k) (a :: k) (b :: j) (p :: j +-> k).
q a b -> (:+:) p q a b
InjR q b b
q'

type Cotraversable :: forall {k}. (k +-> k) -> Constraint
class (Profunctor t) => Cotraversable (t :: k +-> k) where
  cotraverse :: (DistributiveProfunctor (p :: k +-> k), Strong k p, SelfAction k) => p :.: t :~> t :.: p

instance (CategoryOf k) => Cotraversable (Id :: k +-> k) where
  cotraverse :: forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(p :.: Id) :~> (Id :.: p)
cotraverse (p a b
p :.: Id b ~> b
f) = (a ~> a) -> Id a a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id Id a a -> p a b -> (:.:) Id p 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
:.: (b ~> b) -> p a b -> p a b
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> b
f p a b
p ((Ob a, Ob b) => (:.:) Id p a b) -> p a b -> (:.:) Id p a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

instance Cotraversable (->) where
  cotraverse :: forall (p :: Type -> Type -> Type).
(DistributiveProfunctor p, Strong Type p, SelfAction Type) =>
(p :.: (->)) :~> ((->) :.: p)
cotraverse (p a b
p :.: b -> b
f) = a -> a
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (a -> a) -> p a b -> (:.:) (->) p 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
:.: (b ~> b) -> p a b -> p a b
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> b
b -> b
f p a b
p

instance (Cotraversable p, Cotraversable q) => Cotraversable (p :.: q) where
  cotraverse :: forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(p :.: (p :.: q)) :~> ((p :.: q) :.: p)
cotraverse (p a b
r :.: (p b b
p :.: q b b
q)) = case (:.:) p p a b -> (:.:) p p a b
(p :.: p) :~> (p :.: p)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Cotraversable t, DistributiveProfunctor p, Strong k p,
 SelfAction k) =>
(p :.: t) :~> (t :.: p)
forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(p :.: p) :~> (p :.: p)
cotraverse (p a b
r p a b -> p b b -> (:.:) p p 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
:.: p b b
p) of
    p a b
p' :.: p b b
r' -> case (:.:) p q b b -> (:.:) q p b b
(p :.: q) :~> (q :.: p)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Cotraversable t, DistributiveProfunctor p, Strong k p,
 SelfAction k) =>
(p :.: t) :~> (t :.: p)
forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(p :.: q) :~> (q :.: p)
cotraverse (p b b
r' p b b -> q b b -> (:.:) p q b 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
:.: q b b
q) of
      q b b
q' :.: p b b
r'' -> (p a b
p' p a b -> q b b -> (:.:) p q 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
:.: q b b
q') (:.:) p q a b -> p b b -> (:.:) (p :.: q) p 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
:.: p b b
r''

instance (HasBinaryCoproducts k, Cotraversable p, Cotraversable q) => Cotraversable ((p :: k +-> k) :*: q) where
  cotraverse :: forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(p :.: (p :*: q)) :~> ((p :*: q) :.: p)
cotraverse (p a b
r :.: (p b b
p :*: q b b
q)) = case ((:.:) p p a b -> (:.:) p p a b
(p :.: p) :~> (p :.: p)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Cotraversable t, DistributiveProfunctor p, Strong k p,
 SelfAction k) =>
(p :.: t) :~> (t :.: p)
forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(p :.: p) :~> (p :.: p)
cotraverse (p a b
r p a b -> p b b -> (:.:) p p 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
:.: p b b
p), (:.:) p q a b -> (:.:) q p a b
(p :.: q) :~> (q :.: p)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Cotraversable t, DistributiveProfunctor p, Strong k p,
 SelfAction k) =>
(p :.: t) :~> (t :.: p)
forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(p :.: q) :~> (q :.: p)
cotraverse (p a b
r p a b -> q b b -> (:.:) p q 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
:.: q b b
q)) of
    (p a b
p' :.: p b b
r', q a b
q' :.: p b b
r'') -> ((b ~> (b || b)) -> p a b -> p a (b || b)
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap ((b ~> b) -> Obj b -> b ~> (b || b)
forall {k} (a :: k) (a' :: k) (b :: k).
HasBinaryCoproducts k =>
(a ~> a') -> Obj b -> a ~> (a' || b)
lft' (p a b -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt p a b
p') (q a b -> Obj b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt q a b
q')) p a b
p' p a (b || b) -> q a (b || b) -> (:*:) p q a (b || b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> q a b -> (:*:) p q a b
:*: (b ~> (b || b)) -> q a b -> q a (b || b)
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap ((b ~> b) -> Obj b -> b ~> (b || b)
forall {k} (a :: k) (b :: k) (b' :: k).
HasBinaryCoproducts k =>
Obj a -> (b ~> b') -> b ~> (a || b')
rgt' (p a b -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt p a b
p') (q a b -> Obj b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt q a b
q')) q a b
q') (:*:) p q a (b || b) -> p (b || b) b -> (:.:) (p :*: q) p 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
:.: ((b || b) ~> b) -> p (b || b) (b || b) -> p (b || b) b
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
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 b b
r' p b b -> p b b -> p (b || b) (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 b b
r'') ((Ob b, Ob b) => (:.:) (p :*: q) p a b)
-> p b b -> (:.:) (p :*: q) p a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p b b
p

instance (Cotraversable p, Cotraversable q) => Cotraversable (p :+: q) where
  cotraverse :: forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(p :.: (p :+: q)) :~> ((p :+: q) :.: p)
cotraverse (p a b
r :.: InjL p b b
p) = case (:.:) p p a b -> (:.:) p p a b
(p :.: p) :~> (p :.: p)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Cotraversable t, DistributiveProfunctor p, Strong k p,
 SelfAction k) =>
(p :.: t) :~> (t :.: p)
forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(p :.: p) :~> (p :.: p)
cotraverse (p a b
r p a b -> p b b -> (:.:) p p 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
:.: p b b
p) of p a b
p' :.: p b b
r' -> p a b -> (:+:) p q a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> (:+:) p q a b
InjL p a b
p' (:+:) p q a b -> p b b -> (:.:) (p :+: q) p 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
:.: p b b
r'
  cotraverse (p a b
r :.: InjR q b b
q) = case (:.:) p q a b -> (:.:) q p a b
(p :.: q) :~> (q :.: p)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Cotraversable t, DistributiveProfunctor p, Strong k p,
 SelfAction k) =>
(p :.: t) :~> (t :.: p)
forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(p :.: q) :~> (q :.: p)
cotraverse (p a b
r p a b -> q b b -> (:.:) p q 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
:.: q b b
q) of q a b
q' :.: p b b
r' -> q a b -> (:+:) p q a b
forall {j} {k} (q :: j +-> k) (a :: k) (b :: j) (p :: j +-> k).
q a b -> (:+:) p q a b
InjR q a b
q' (:+:) p q a b -> p b b -> (:.:) (p :+: q) p 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
:.: p b b
r'