{-# 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.Helper.CCC
import Proarrow.Object.BinaryCoproduct (Coprod (..), HasBinaryCoproducts (..), HasCoproducts, codiag, copar, lft', rgt')
import Proarrow.Object.BinaryProduct (Cartesian, PROD (..), Prod (..), diag, fst', snd', HasBinaryProducts (..))
import Proarrow.Object.Exponential (BiCCC)
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Coproduct ((:+:) (..))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Product ((:*:) (..))

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 :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
forall (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
toCCC @(F a * InitF) @InitF (((forall (x :: FK k).
  Cast x (TermF && ('F (UN 'PR a) * InitF)) =>
  x ~> ('F (UN 'PR a) * InitF))
 -> (TermF && ('F (UN 'PR a) * InitF)) ~> InitF)
-> TermF ~> (('F (UN 'PR a) * InitF) ~~> InitF)
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \((TermF * ('F (UN 'PR a) * InitF)) ~> 'F (UN 'PR a)
_ :& (TermF * ('F (UN 'PR a) * InitF)) ~> InitF
v) -> (TermF && ('F (UN 'PR a) * InitF)) ~> InitF
(TermF * ('F (UN 'PR a) * InitF)) ~> InitF
v))
  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 :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
forall (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
toCCC @(InitF * F a) @InitF (((forall (x :: FK k).
  Cast x (TermF && (InitF * 'F (UN 'PR a))) =>
  x ~> (InitF * 'F (UN 'PR a)))
 -> (TermF && (InitF * 'F (UN 'PR a))) ~> InitF)
-> TermF ~> ((InitF * 'F (UN 'PR a)) ~~> InitF)
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \((TermF * (InitF * 'F (UN 'PR a))) ~> InitF
v :& (TermF * (InitF * 'F (UN 'PR a))) ~> 'F (UN 'PR a)
_) -> (TermF && (InitF * 'F (UN 'PR a))) ~> InitF
(TermF * (InitF * 'F (UN 'PR a))) ~> InitF
v))

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 {k} (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
forall (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
toCCC @(F a * (F b + F c)) @((F a * F b) + (F a * F c))
  (((forall (x :: FK k).
  Cast x (TermF && ('F a * ('F b + 'F c))) =>
  x ~> ('F a * ('F b + 'F c)))
 -> (TermF && ('F a * ('F b + 'F c)))
    ~> (('F a * 'F b) + ('F a * 'F c)))
-> TermF
   ~> (('F a * ('F b + 'F c)) ~~> (('F a * 'F b) + ('F a * 'F c)))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \((TermF * ('F a * ('F b + 'F c))) ~> 'F a
a :& (TermF * ('F a * ('F b + 'F c))) ~> ('F b + 'F c)
bc) -> ((TermF * ('F a * ('F b + 'F c)))
 ~> ('F b ~~> ('F a --> (('F a * 'F b) + ('F a * 'F c)))))
-> ((TermF * ('F a * ('F b + 'F c)))
    ~> ('F c ~~> ('F a --> (('F a * 'F b) + ('F a * 'F c)))))
-> (TermF * ('F a * ('F b + 'F c)))
   ~> (('F b || 'F c) ~~> ('F a --> (('F a * 'F b) + ('F a * 'F c))))
forall {k} (a :: k) (b :: k) (c :: k) (i :: k).
(HasBinaryCoproducts k, CCC k, Ob a, Ob b, Ob c) =>
(i ~> (a ~~> c)) -> (i ~> (b ~~> c)) -> i ~> ((a || b) ~~> c)
either (((forall (x :: FK k).
  Cast x ((TermF * ('F a * ('F b + 'F c))) && 'F b) =>
  x ~> 'F b)
 -> ((TermF * ('F a * ('F b + 'F c))) && 'F b)
    ~> ('F a --> (('F a * 'F b) + ('F a * 'F c))))
-> (TermF * ('F a * ('F b + 'F c)))
   ~> ('F b ~~> ('F a --> (('F a * 'F b) + ('F a * 'F c))))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \forall (x :: FK k).
Cast x ((TermF * ('F a * ('F b + 'F c))) && 'F b) =>
x ~> 'F b
b -> ((forall (x :: FK k).
  Cast x (((TermF * ('F a * ('F b + 'F c))) * 'F b) && 'F a) =>
  x ~> 'F a)
 -> (((TermF * ('F a * ('F b + 'F c))) * 'F b) && 'F a)
    ~> (('F a * 'F b) + ('F a * 'F c)))
-> ((TermF * ('F a * ('F b + 'F c))) * 'F b)
   ~> ('F a ~~> (('F a * 'F b) + ('F a * 'F c)))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \forall (x :: FK k).
Cast x (((TermF * ('F a * ('F b + 'F c))) * 'F b) && 'F a) =>
x ~> 'F a
a' -> ((((TermF * ('F a * ('F b + 'F c))) * 'F b) * 'F a)
 ~> ('F a * 'F b))
-> (((TermF * ('F a * ('F b + 'F c))) * 'F b) * 'F a)
   ~> (('F a * 'F b) || ('F a * 'F c))
forall {k} (a :: k) (b :: k) (i :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(i ~> a) -> i ~> (a || b)
left ((((TermF * ('F a * ('F b + 'F c))) * 'F b) * 'F a) ~> 'F a
forall (x :: FK k).
Cast x (((TermF * ('F a * ('F b + 'F c))) * 'F b) && 'F a) =>
x ~> 'F a
a' ((((TermF * ('F a * ('F b + 'F c))) * 'F b) * 'F a) ~> 'F a)
-> ((((TermF * ('F a * ('F b + 'F c))) * 'F b) * 'F a) ~> 'F b)
-> (((TermF * ('F a * ('F b + 'F c))) * 'F b) * 'F a)
   ~> ('F a && 'F b)
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob a, Ob b) =>
(i ~> a) -> (i ~> b) -> i ~> (a && b)
:& (((TermF * ('F a * ('F b + 'F c))) * 'F b) * 'F a) ~> 'F b
forall (x :: FK k).
Cast x ((TermF * ('F a * ('F b + 'F c))) && 'F b) =>
x ~> 'F b
b)) (((forall (x :: FK k).
  Cast x ((TermF * ('F a * ('F b + 'F c))) && 'F c) =>
  x ~> 'F c)
 -> ((TermF * ('F a * ('F b + 'F c))) && 'F c)
    ~> ('F a --> (('F a * 'F b) + ('F a * 'F c))))
-> (TermF * ('F a * ('F b + 'F c)))
   ~> ('F c ~~> ('F a --> (('F a * 'F b) + ('F a * 'F c))))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \forall (x :: FK k).
Cast x ((TermF * ('F a * ('F b + 'F c))) && 'F c) =>
x ~> 'F c
c -> ((forall (x :: FK k).
  Cast x (((TermF * ('F a * ('F b + 'F c))) * 'F c) && 'F a) =>
  x ~> 'F a)
 -> (((TermF * ('F a * ('F b + 'F c))) * 'F c) && 'F a)
    ~> (('F a * 'F b) + ('F a * 'F c)))
-> ((TermF * ('F a * ('F b + 'F c))) * 'F c)
   ~> ('F a ~~> (('F a * 'F b) + ('F a * 'F c)))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \forall (x :: FK k).
Cast x (((TermF * ('F a * ('F b + 'F c))) * 'F c) && 'F a) =>
x ~> 'F a
a' -> ((((TermF * ('F a * ('F b + 'F c))) * 'F c) * 'F a)
 ~> ('F a * 'F c))
-> (((TermF * ('F a * ('F b + 'F c))) * 'F c) * 'F a)
   ~> (('F a * 'F b) || ('F a * 'F c))
forall {k} (a :: k) (b :: k) (i :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(i ~> b) -> i ~> (a || b)
right ((((TermF * ('F a * ('F b + 'F c))) * 'F c) * 'F a) ~> 'F a
forall (x :: FK k).
Cast x (((TermF * ('F a * ('F b + 'F c))) * 'F c) && 'F a) =>
x ~> 'F a
a' ((((TermF * ('F a * ('F b + 'F c))) * 'F c) * 'F a) ~> 'F a)
-> ((((TermF * ('F a * ('F b + 'F c))) * 'F c) * 'F a) ~> 'F c)
-> (((TermF * ('F a * ('F b + 'F c))) * 'F c) * 'F a)
   ~> ('F a && 'F c)
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob a, Ob b) =>
(i ~> a) -> (i ~> b) -> i ~> (a && b)
:& (((TermF * ('F a * ('F b + 'F c))) * 'F c) * 'F a) ~> 'F c
forall (x :: FK k).
Cast x ((TermF * ('F a * ('F b + 'F c))) && 'F c) =>
x ~> 'F c
c)) ((TermF * ('F a * ('F b + 'F c)))
 ~> (('F b + 'F c) ~~> ('F a --> (('F a * 'F b) + ('F a * 'F c)))))
-> ((TermF * ('F a * ('F b + 'F c))) ~> ('F b + 'F c))
-> (TermF * ('F a * ('F b + 'F c)))
   ~> ('F a --> (('F a * 'F b) + ('F a * 'F c)))
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob b) =>
(i ~> (a ~~> b)) -> (i ~> a) -> i ~> b
$ (TermF * ('F a * ('F b + 'F c))) ~> ('F b + 'F c)
bc ((TermF * ('F a * ('F b + 'F c)))
 ~> ('F a ~~> (('F a * 'F b) + ('F a * 'F c))))
-> ((TermF * ('F a * ('F b + 'F c))) ~> 'F a)
-> (TermF * ('F a * ('F b + 'F c)))
   ~> (('F a * 'F b) + ('F a * 'F c))
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob b) =>
(i ~> (a ~~> b)) -> (i ~> a) -> i ~> b
$ (TermF * ('F a * ('F b + 'F c))) ~> 'F a
a)

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 :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
forall (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
toCCC @((F a + F b) * F c) @((F a * F c) + (F b * F c))
  (((forall (x :: FK k).
  Cast x (TermF && (('F a + 'F b) * 'F c)) =>
  x ~> (('F a + 'F b) * 'F c))
 -> (TermF && (('F a + 'F b) * 'F c))
    ~> (('F a * 'F c) + ('F b * 'F c)))
-> TermF
   ~> ((('F a + 'F b) * 'F c) ~~> (('F a * 'F c) + ('F b * 'F c)))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \((TermF * (('F a + 'F b) * 'F c)) ~> ('F a + 'F b)
ab :& (TermF * (('F a + 'F b) * 'F c)) ~> 'F c
c) -> ((TermF * (('F a + 'F b) * 'F c))
 ~> ('F a ~~> ('F c --> (('F a * 'F c) + ('F b * 'F c)))))
-> ((TermF * (('F a + 'F b) * 'F c))
    ~> ('F b ~~> ('F c --> (('F a * 'F c) + ('F b * 'F c)))))
-> (TermF * (('F a + 'F b) * 'F c))
   ~> (('F a || 'F b) ~~> ('F c --> (('F a * 'F c) + ('F b * 'F c))))
forall {k} (a :: k) (b :: k) (c :: k) (i :: k).
(HasBinaryCoproducts k, CCC k, Ob a, Ob b, Ob c) =>
(i ~> (a ~~> c)) -> (i ~> (b ~~> c)) -> i ~> ((a || b) ~~> c)
either (((forall (x :: FK k).
  Cast x ((TermF * (('F a + 'F b) * 'F c)) && 'F a) =>
  x ~> 'F a)
 -> ((TermF * (('F a + 'F b) * 'F c)) && 'F a)
    ~> ('F c --> (('F a * 'F c) + ('F b * 'F c))))
-> (TermF * (('F a + 'F b) * 'F c))
   ~> ('F a ~~> ('F c --> (('F a * 'F c) + ('F b * 'F c))))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \forall (x :: FK k).
Cast x ((TermF * (('F a + 'F b) * 'F c)) && 'F a) =>
x ~> 'F a
a -> ((forall (x :: FK k).
  Cast x (((TermF * (('F a + 'F b) * 'F c)) * 'F a) && 'F c) =>
  x ~> 'F c)
 -> (((TermF * (('F a + 'F b) * 'F c)) * 'F a) && 'F c)
    ~> (('F a * 'F c) + ('F b * 'F c)))
-> ((TermF * (('F a + 'F b) * 'F c)) * 'F a)
   ~> ('F c ~~> (('F a * 'F c) + ('F b * 'F c)))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \forall (x :: FK k).
Cast x (((TermF * (('F a + 'F b) * 'F c)) * 'F a) && 'F c) =>
x ~> 'F c
c' -> ((((TermF * (('F a + 'F b) * 'F c)) * 'F a) * 'F c)
 ~> ('F a * 'F c))
-> (((TermF * (('F a + 'F b) * 'F c)) * 'F a) * 'F c)
   ~> (('F a * 'F c) || ('F b * 'F c))
forall {k} (a :: k) (b :: k) (i :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(i ~> a) -> i ~> (a || b)
left ((((TermF * (('F a + 'F b) * 'F c)) * 'F a) * 'F c) ~> 'F a
forall (x :: FK k).
Cast x ((TermF * (('F a + 'F b) * 'F c)) && 'F a) =>
x ~> 'F a
a ((((TermF * (('F a + 'F b) * 'F c)) * 'F a) * 'F c) ~> 'F a)
-> ((((TermF * (('F a + 'F b) * 'F c)) * 'F a) * 'F c) ~> 'F c)
-> (((TermF * (('F a + 'F b) * 'F c)) * 'F a) * 'F c)
   ~> ('F a && 'F c)
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob a, Ob b) =>
(i ~> a) -> (i ~> b) -> i ~> (a && b)
:& (((TermF * (('F a + 'F b) * 'F c)) * 'F a) * 'F c) ~> 'F c
forall (x :: FK k).
Cast x (((TermF * (('F a + 'F b) * 'F c)) * 'F a) && 'F c) =>
x ~> 'F c
c')) (((forall (x :: FK k).
  Cast x ((TermF * (('F a + 'F b) * 'F c)) && 'F b) =>
  x ~> 'F b)
 -> ((TermF * (('F a + 'F b) * 'F c)) && 'F b)
    ~> ('F c --> (('F a * 'F c) + ('F b * 'F c))))
-> (TermF * (('F a + 'F b) * 'F c))
   ~> ('F b ~~> ('F c --> (('F a * 'F c) + ('F b * 'F c))))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \forall (x :: FK k).
Cast x ((TermF * (('F a + 'F b) * 'F c)) && 'F b) =>
x ~> 'F b
b -> ((forall (x :: FK k).
  Cast x (((TermF * (('F a + 'F b) * 'F c)) * 'F b) && 'F c) =>
  x ~> 'F c)
 -> (((TermF * (('F a + 'F b) * 'F c)) * 'F b) && 'F c)
    ~> (('F a * 'F c) + ('F b * 'F c)))
-> ((TermF * (('F a + 'F b) * 'F c)) * 'F b)
   ~> ('F c ~~> (('F a * 'F c) + ('F b * 'F c)))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \forall (x :: FK k).
Cast x (((TermF * (('F a + 'F b) * 'F c)) * 'F b) && 'F c) =>
x ~> 'F c
c' -> ((((TermF * (('F a + 'F b) * 'F c)) * 'F b) * 'F c)
 ~> ('F b * 'F c))
-> (((TermF * (('F a + 'F b) * 'F c)) * 'F b) * 'F c)
   ~> (('F a * 'F c) || ('F b * 'F c))
forall {k} (a :: k) (b :: k) (i :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(i ~> b) -> i ~> (a || b)
right ((((TermF * (('F a + 'F b) * 'F c)) * 'F b) * 'F c) ~> 'F b
forall (x :: FK k).
Cast x ((TermF * (('F a + 'F b) * 'F c)) && 'F b) =>
x ~> 'F b
b ((((TermF * (('F a + 'F b) * 'F c)) * 'F b) * 'F c) ~> 'F b)
-> ((((TermF * (('F a + 'F b) * 'F c)) * 'F b) * 'F c) ~> 'F c)
-> (((TermF * (('F a + 'F b) * 'F c)) * 'F b) * 'F c)
   ~> ('F b && 'F c)
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob a, Ob b) =>
(i ~> a) -> (i ~> b) -> i ~> (a && b)
:& (((TermF * (('F a + 'F b) * 'F c)) * 'F b) * 'F c) ~> 'F c
forall (x :: FK k).
Cast x (((TermF * (('F a + 'F b) * 'F c)) * 'F b) && 'F c) =>
x ~> 'F c
c')) ((TermF * (('F a + 'F b) * 'F c))
 ~> (('F a + 'F b) ~~> ('F c --> (('F a * 'F c) + ('F b * 'F c)))))
-> ((TermF * (('F a + 'F b) * 'F c)) ~> ('F a + 'F b))
-> (TermF * (('F a + 'F b) * 'F c))
   ~> ('F c --> (('F a * 'F c) + ('F b * 'F c)))
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob b) =>
(i ~> (a ~~> b)) -> (i ~> a) -> i ~> b
$ (TermF * (('F a + 'F b) * 'F c)) ~> ('F a + 'F b)
ab ((TermF * (('F a + 'F b) * 'F c))
 ~> ('F c ~~> (('F a * 'F c) + ('F b * 'F c))))
-> ((TermF * (('F a + 'F b) * 'F c)) ~> 'F c)
-> (TermF * (('F a + 'F b) * 'F c))
   ~> (('F a * 'F c) + ('F b * 'F c))
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob b) =>
(i ~> (a ~~> b)) -> (i ~> a) -> i ~> b
$ (TermF * (('F a + 'F b) * 'F c)) ~> 'F c
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 :: PRO j k) (c :: j) (a :: j) (b :: k).
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 :: PRO 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 :: PRO j k) (a :: j) (b :: k) 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 :: PRO j k) (c :: j) (a :: j) (b :: k).
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 :: PRO 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 :: 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
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 :: PRO j k) (c :: j) (a :: j) (b :: k).
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 {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src p b b
p') (q b b -> Obj b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
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 :: PRO j k) (a :: j) (b :: k) (q :: PRO 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 :: PRO j k) (c :: j) (a :: j) (b :: k).
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 {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src p b b
p') (q b b -> Obj b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
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 :: PRO j k) (a :: j) (b :: k) 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 :: PRO j k) (a :: j) (b :: k) (q :: PRO 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 :: PRO j k) (a :: j) (b :: k) (p :: PRO 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 :: PRO 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 :: PRO j k) (b :: k) (d :: k) (a :: j).
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 :: PRO j k) (a :: j) (b :: k) 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 :: PRO 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 :: PRO j k) (b :: k) (d :: k) (a :: j).
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 :: PRO j k) (b :: k) (d :: k) (a :: j).
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 :: PRO k2 k1).
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 :: PRO k2 k1).
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 :: PRO j k) (a :: j) (b :: k) (q :: PRO 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 :: PRO j k) (b :: k) (d :: k) (a :: j).
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 :: PRO k2 k1).
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 :: PRO k2 k1).
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 :: 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 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 :: PRO j k) (a :: j) (b :: k) 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 :: PRO j k) (a :: j) (b :: k) (q :: PRO 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 :: PRO j k) (a :: j) (b :: k) (p :: PRO 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'