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

-- | Binary coproducts: 'HasBinaryCoproducts' provides @a '||' b@ with injections 'lft'\/'rgt' and
-- copairing @('|||')@, and 'HasCoproducts' adds the initial object. Also biproducts ('HasBiproducts')
-- and the 'COPROD' kind wrapper, which makes @('||')@ the tensor of a monoidal structure on the same
-- objects.
module Proarrow.Colimit.BinaryCoproduct where

import Data.Kind (Type)
import Prelude (Show, ($), type (~))
import Prelude qualified as P

import Proarrow.Category.Instance.Bool (BOOL (..), Booleans (..))
import Proarrow.Category.Instance.Free
  ( Elem (..)
  , FREE (..)
  , HasStructure (..)
  , IsFreeOb (..)
  , Lower
  , WithShow
  , withLowerOb
  )
import Proarrow.Category.Instance.Free qualified as F
import Proarrow.Category.Instance.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Category.Instance.Product (Diag, Fst, Snd, (:**:) (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Core (CAT, CategoryOf (..), Hom, Profunctor (..), Promonad (..), UN, WrappedOb, type (+->))
import Proarrow.Functor (Functor (..), FunctorForRep (..))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..), PROD (..), Prod (..), diag)
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Object (Obj, obj, tgt)
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), withObCorep)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Coproduct (coproduct, (:+:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Instance.Product ((:*:) (..))
import Proarrow.Profunctor.Instance.Terminal (TerminalProfunctor (..))
import Proarrow.Profunctor.Representable (CorepStar (..), Rep (..), Representable (..))
import Proarrow.Tools.Laws (Law (..), Laws (..), (===))

infixl 4 ||
infixl 4 |||
infixl 4 +++

-- | Binary coproducts, dual to 'Proarrow.Limit.BinaryProduct.HasBinaryProducts': an object
-- @a '||' b@ with injections 'lft' and 'rgt', universal among all pairs of arrows into a common
-- target. Each such pair factors through it uniquely via '(|||)'.
--
-- __Laws:__
--
-- * @(f '|||' g) . 'lft' = f@
-- * @(f '|||' g) . 'rgt' = g@
-- * Uniqueness: @(h . f) '|||' (h . g) = h . (f '|||' g)@
--
-- Checked by 'Proarrow.Testing.Laws.testBinaryCoproducts'.
class (CategoryOf k) => HasBinaryCoproducts k where
  -- | The coproduct object.
  type (a :: k) || (b :: k) :: k

  -- | Recovers @'Ob' (a '||' b)@ from the objecthood of the summands.
  withObCoprod :: (Ob (a :: k), Ob b) => ((Ob (a || b)) => r) -> r

  -- | The left injection.
  lft :: (Ob (a :: k), Ob b) => a ~> (a || b)

  -- | The right injection.
  rgt :: (Ob (a :: k), Ob b) => b ~> (a || b)

  -- | The mediating arrow: case-splits two arrows into a common target.
  (|||) :: (x :: k) ~> a -> y ~> a -> (x || y) ~> a

  -- | The coproduct of two arrows, acting on each summand independently.
  (+++) :: forall a b x y. (a :: k) ~> x -> b ~> y -> a || b ~> x || y
  a ~> x
l +++ b ~> y
r = forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @x @y (x ~> (x || y)) -> (a ~> x) -> a ~> (x || y)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> x
l (a ~> (x || y)) -> (b ~> (x || y)) -> (a || b) ~> (x || y)
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).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @x @y (y ~> (x || y)) -> (b ~> y) -> b ~> (x || y)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b ~> y
r ((Ob a, Ob x) => (a || b) ~> (x || y))
-> (a ~> x) -> (a || b) ~> (x || y)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ a ~> x
l ((Ob b, Ob y) => (a || b) ~> (x || y))
-> (b ~> y) -> (a || b) ~> (x || y)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ b ~> y
r

lft' :: forall {k} (a :: k) a' b. (HasBinaryCoproducts k) => a ~> a' -> Obj b -> a ~> (a' || b)
lft' :: forall {k} (a :: k) (a' :: k) (b :: k).
HasBinaryCoproducts k =>
(a ~> a') -> Obj b -> a ~> (a' || b)
lft' a ~> a'
a Obj b
b = forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a' @b (a' ~> (a' || b)) -> (a ~> a') -> a ~> (a' || b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> a'
a ((Ob a, Ob a') => a ~> (a' || b)) -> (a ~> a') -> a ~> (a' || b)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ a ~> a'
a ((Ob b, Ob b) => a ~> (a' || b)) -> Obj b -> a ~> (a' || b)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ Obj b
b

rgt' :: forall {k} (a :: k) b b'. (HasBinaryCoproducts k) => Obj a -> b ~> b' -> b ~> (a || b')
rgt' :: forall {k} (a :: k) (b :: k) (b' :: k).
HasBinaryCoproducts k =>
Obj a -> (b ~> b') -> b ~> (a || b')
rgt' Obj a
a b ~> b'
b = forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @b' (b' ~> (a || b')) -> (b ~> b') -> b ~> (a || b')
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b ~> b'
b ((Ob a, Ob a) => b ~> (a || b')) -> Obj a -> b ~> (a || b')
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ Obj a
a ((Ob b, Ob b') => b ~> (a || b')) -> (b ~> b') -> b ~> (a || b')
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ b ~> b'
b

left :: forall {k} (c :: k) (a :: k) (b :: k). (HasBinaryCoproducts k, Ob c) => a ~> b -> (a || c) ~> (b || c)
left :: forall {k} (c :: k) (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob c) =>
(a ~> b) -> (a || c) ~> (b || c)
left a ~> b
f = a ~> b
f (a ~> b) -> (c ~> c) -> (a || c) ~> (b || 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). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c

right :: forall {k} (c :: k) (a :: k) (b :: k). (HasBinaryCoproducts k, Ob c) => a ~> b -> (c || a) ~> (c || b)
right :: forall {k} (c :: k) (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob c) =>
(a ~> b) -> (c || a) ~> (c || b)
right a ~> b
f = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c Obj c -> (a ~> b) -> (c || a) ~> (c || b)
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)
+++ a ~> b
f

codiag :: forall {k} (a :: k). (HasBinaryCoproducts k, Ob a) => (a || a) ~> a
codiag :: forall {k} (a :: k). (HasBinaryCoproducts k, Ob a) => (a || a) ~> a
codiag = a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id (a ~> a) -> (a ~> a) -> (a || a) ~> a
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
||| a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id

swapCoprod' :: forall {k} (a :: k) a' b b'. (HasBinaryCoproducts k) => a ~> a' -> b ~> b' -> (a || b) ~> (b' || a')
swapCoprod' :: forall {k} (a :: k) (a' :: k) (b :: k) (b' :: k).
HasBinaryCoproducts k =>
(a ~> a') -> (b ~> b') -> (a || b) ~> (b' || a')
swapCoprod' a ~> a'
a b ~> b'
b = Obj b' -> (a ~> a') -> a ~> (b' || a')
forall {k} (a :: k) (b :: k) (b' :: k).
HasBinaryCoproducts k =>
Obj a -> (b ~> b') -> b ~> (a || b')
rgt' ((b ~> b') -> Obj b'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt b ~> b'
b) a ~> a'
a (a ~> (b' || a')) -> (b ~> (b' || a')) -> (a || b) ~> (b' || a')
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
||| (b ~> b') -> Obj a' -> b ~> (b' || a')
forall {k} (a :: k) (a' :: k) (b :: k).
HasBinaryCoproducts k =>
(a ~> a') -> Obj b -> a ~> (a' || b)
lft' b ~> b'
b ((a ~> a') -> Obj a'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt a ~> a'
a)

swapCoprod :: forall {k} (a :: k) b. (HasBinaryCoproducts k, Ob a, Ob b) => a || b ~> b || a
swapCoprod :: forall {k} (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(a || b) ~> (b || a)
swapCoprod = (a ~> a) -> (b ~> b) -> (a || b) ~> (b || a)
forall {k} (a :: k) (a' :: k) (b :: k) (b' :: k).
HasBinaryCoproducts k =>
(a ~> a') -> (b ~> b') -> (a || b) ~> (b' || a')
swapCoprod' (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b)

-- | The coproduct as a functor from the product category, @'(a, b) ↦ a || b@. The coproduct
-- analogue of 'Proarrow.Category.Monoidal.MultRep'.
data PlusRep :: (k, k) +-> k

instance (HasBinaryCoproducts k) => FunctorForRep (PlusRep :: (k, k) +-> k) where
  type PlusRep @ '(a, b) = a || b
  fmap :: forall (a :: (k, k)) (b :: (k, k)).
(a ~> b) -> (PlusRep @ a) ~> (PlusRep @ b)
fmap (a1 ~> b1
f :**: a2 ~> b2
g) = a1 ~> b1
f (a1 ~> b1) -> (a2 ~> b2) -> (a1 || a2) ~> (b1 || b2)
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)
+++ a2 ~> b2
g

data family Coproduct :: k -> k +-> k
instance (HasBinaryCoproducts k, Ob a) => FunctorForRep (Coproduct a :: k +-> k) where
  type Coproduct a @ b = a || b
  fmap :: forall (a :: k) (b :: k).
(a ~> b) -> (Coproduct a @ a) ~> (Coproduct a @ b)
fmap a ~> b
f = forall (c :: k) (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob c) =>
(a ~> b) -> (c || a) ~> (c || b)
forall {k} (c :: k) (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob c) =>
(a ~> b) -> (c || a) ~> (c || b)
right @a a ~> b
f

type HasCoproducts k = (HasInitialObject k, HasBinaryCoproducts k)

class ((a ** b) ~ (a || b)) => TensorIsCoproduct a b
instance ((a ** b) ~ (a || b)) => TensorIsCoproduct a b
class
  (HasCoproducts k, Monoidal k, (Unit :: k) ~ InitialObject, forall (a :: k) (b :: k). TensorIsCoproduct a b) =>
  Cocartesian k
instance
  (HasCoproducts k, Monoidal k, (Unit :: k) ~ InitialObject, forall (a :: k) (b :: k). TensorIsCoproduct a b)
  => Cocartesian k

-- | Every functor between cocartesian categories is lax monoidal, @f a || f b ~> f (a || b)@ by the
-- injections and @InitialObject ~> f InitialObject@ by initiality. On the 'CorepStar' of its
-- corepresentable profunctor this is 'Proarrow.Category.Monoidal.LaxMonoidal'.
instance (Corepresentable p, Cocartesian j, Cocartesian k) => MonoidalProfunctor (CorepStar (p :: j +-> k)) where
  one :: CorepStar p Unit Unit
one = forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: j +-> k) (a :: k) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withObCorep @p @Unit ((InitialObject ~> (p %% InitialObject))
-> CorepStar p InitialObject InitialObject
forall {j} {k} (b :: j) (a :: k) (p :: k +-> j).
Ob b =>
(a ~> (p %% b)) -> CorepStar p a b
CorepStar InitialObject ~> (p %% InitialObject)
forall (a :: j). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate)
  CorepStar @a x1 ~> (p %% x2)
f ** :: forall (x1 :: j) (x2 :: k) (y1 :: j) (y2 :: k).
CorepStar p x1 x2
-> CorepStar p y1 y2 -> CorepStar p (x1 ** y1) (x2 ** y2)
** CorepStar @b y1 ~> (p %% y2)
g = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @b (((x1 ** y1) ~> (p %% (x2 ** y2)))
-> CorepStar p (x1 ** y1) (x2 ** y2)
forall {j} {k} (b :: j) (a :: k) (p :: k +-> j).
Ob b =>
(a ~> (p %% b)) -> CorepStar p a b
CorepStar (forall {j} {k} (p :: j +-> k) (a :: k) (b :: k) (a' :: j)
       (b' :: j).
(Corepresentable p, Cocartesian j, Cocartesian k,
 TensorIsCoproduct a b, TensorIsCoproduct a' b', Ob a, Ob b) =>
(a' ~> (p %% a))
-> (b' ~> (p %% b)) -> (a' ** b') ~> (p %% (a ** b))
forall (p :: j +-> k) (a :: k) (b :: k) (a' :: j) (b' :: j).
(Corepresentable p, Cocartesian j, Cocartesian k,
 TensorIsCoproduct a b, TensorIsCoproduct a' b', Ob a, Ob b) =>
(a' ~> (p %% a))
-> (b' ~> (p %% b)) -> (a' ** b') ~> (p %% (a ** b))
parCorepCocartesian @p @a @b x1 ~> (p %% x2)
f y1 ~> (p %% y2)
g))

parCorepCocartesian
  :: forall {j} {k} p (a :: k) b a' b'
   . ( Corepresentable (p :: j +-> k)
     , Cocartesian j
     , Cocartesian k
     , TensorIsCoproduct a b
     , TensorIsCoproduct a' b'
     , Ob a
     , Ob b
     )
  => (a' ~> p %% a) -> (b' ~> p %% b) -> (a' ** b') ~> p %% (a ** b)
parCorepCocartesian :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: k) (a' :: j)
       (b' :: j).
(Corepresentable p, Cocartesian j, Cocartesian k,
 TensorIsCoproduct a b, TensorIsCoproduct a' b', Ob a, Ob b) =>
(a' ~> (p %% a))
-> (b' ~> (p %% b)) -> (a' ** b') ~> (p %% (a ** b))
parCorepCocartesian a' ~> (p %% a)
f b' ~> (p %% b)
g = forall {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @p (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @b) ((p %% a) ~> (p %% (a || b)))
-> (a' ~> (p %% a)) -> a' ~> (p %% (a || b))
forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a' ~> (p %% a)
f (a' ~> (p %% (a || b)))
-> (b' ~> (p %% (a || b))) -> (a' || b') ~> (p %% (a || b))
forall (x :: j) (a :: j) (y :: j).
(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 {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @p (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @b) ((p %% b) ~> (p %% (a || b)))
-> (b' ~> (p %% b)) -> b' ~> (p %% (a || b))
forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b' ~> (p %% b)
g

instance HasBinaryCoproducts Type where
  type a || b = P.Either a b
  withObCoprod :: forall a b r. (Ob a, Ob b) => (Ob (a || b) => r) -> r
withObCoprod Ob (a || b) => r
r = r
Ob (a || b) => r
r
  lft :: forall a b. (Ob a, Ob b) => a ~> (a || b)
lft = a ~> (a || b)
a -> Either a b
forall a b. a -> Either a b
P.Left
  rgt :: forall a b. (Ob a, Ob b) => b ~> (a || b)
rgt = b ~> (a || b)
b -> Either a b
forall a b. b -> Either a b
P.Right
  ||| :: forall x a y. (x ~> a) -> (y ~> a) -> (x || y) ~> a
(|||) = (x ~> a) -> (y ~> a) -> (x || y) ~> a
(x -> a) -> (y -> a) -> Either x y -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
P.either

instance HasBinaryCoproducts () where
  -- a wildcard, not @'()@, so that @a || b@ reduces for an abstract @a@, as on pairs
  type _ || _ = '()
  withObCoprod :: forall (a :: ()) (b :: ()) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod Ob (a || b) => r
r = r
Ob (a || b) => r
r
  lft :: forall (a :: ()) (b :: ()). (Ob a, Ob b) => a ~> (a || b)
lft = a ~> (a || b)
Unit '() '()
U.Unit
  rgt :: forall (a :: ()) (b :: ()). (Ob a, Ob b) => b ~> (a || b)
rgt = b ~> (a || b)
Unit '() '()
U.Unit
  x ~> a
Unit x a
U.Unit ||| :: forall (x :: ()) (a :: ()) (y :: ()).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| y ~> a
Unit y '()
U.Unit = (x || y) ~> a
Unit '() '()
U.Unit

instance HasBinaryCoproducts BOOL where
  type FLS || b = b
  type TRU || b = TRU
  type a || FLS = a
  type a || TRU = TRU
  withObCoprod :: forall (a :: BOOL) (b :: BOOL) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @a Ob (a || b) => r
r = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a of
    Obj a
Booleans a a
Tru -> r
Ob (a || b) => r
r
    Obj a
Booleans a a
Fls -> r
Ob (a || b) => r
r
  lft :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => a ~> (a || b)
lft @a @b = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a of
    Obj a
Booleans a a
Fls -> forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @b
    Obj a
Booleans a a
Tru -> a ~> (a || b)
Booleans 'TRU 'TRU
Tru
  rgt :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => b ~> (a || b)
rgt @a @b = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @b of
    Obj b
Booleans b b
Fls -> forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @a
    Obj b
Booleans b b
Tru -> b ~> (a || b)
Booleans 'TRU 'TRU
Tru
  x ~> a
Booleans x a
Fls ||| :: forall (x :: BOOL) (a :: BOOL) (y :: BOOL).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| y ~> a
Booleans y 'FLS
Fls = (x || y) ~> a
Booleans 'FLS 'FLS
Fls
  x ~> a
Booleans x a
F2T ||| y ~> a
b = y ~> a
(x || y) ~> a
b
  x ~> a
Booleans x a
Tru ||| y ~> a
_ = (x || y) ~> a
Booleans 'TRU 'TRU
Tru

-- | Coproducts in a product category are componentwise. Through the projections, as products are
-- there, so that @a || b@ reduces for an abstract pair.
instance (HasBinaryCoproducts j, HasBinaryCoproducts k) => HasBinaryCoproducts (j, k) where
  type a || b = '(Fst @ a || Fst @ b, Snd @ a || Snd @ b)
  withObCoprod :: forall (a :: (j, k)) (b :: (j, k)) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @'(a1, a2) @'(b1, b2) Ob (a || b) => r
r = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @j @a1 @b1 (forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a2 @b2 r
Ob ((Snd @ a) || (Snd @ b)) => r
Ob (a || b) => r
r)
  lft :: forall (a :: (j, k)) (b :: (j, k)). (Ob a, Ob b) => a ~> (a || b)
lft @'(a1, a2) @'(b1, b2) = forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @a1 @b1 ((Fst @ a) ~> ((Fst @ a) || (Fst @ b)))
-> ((Snd @ a) ~> ((Snd @ a) || (Snd @ b)))
-> (:**:)
     (~>)
     (~>)
     '(Fst @ a, Snd @ a)
     '((Fst @ a) || (Fst @ b), (Snd @ a) || (Snd @ b))
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @a2 @b2
  rgt :: forall (a :: (j, k)) (b :: (j, k)). (Ob a, Ob b) => b ~> (a || b)
rgt @'(a1, a2) @'(b1, b2) = forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @a1 @b1 ((Fst @ b) ~> ((Fst @ a) || (Fst @ b)))
-> ((Snd @ b) ~> ((Snd @ a) || (Snd @ b)))
-> (:**:)
     (~>)
     (~>)
     '(Fst @ b, Snd @ b)
     '((Fst @ a) || (Fst @ b), (Snd @ a) || (Snd @ b))
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @a2 @b2
  (a1 ~> b1
f1 :**: a2 ~> b2
f2) ||| :: forall (x :: (j, k)) (a :: (j, k)) (y :: (j, k)).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| (a1 ~> b1
g1 :**: a2 ~> b2
g2) = (a1 ~> b1
f1 (a1 ~> b1) -> (a1 ~> b1) -> (a1 || a1) ~> b1
forall (x :: j) (a :: j) (y :: j).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| a1 ~> b1
a1 ~> b1
g1) ((a1 || a1) ~> b1)
-> ((a2 || a2) ~> b2)
-> (:**:) (~>) (~>) '(a1 || a1, a2 || a2) '(b1, b2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (a2 ~> b2
f2 (a2 ~> b2) -> (a2 ~> b2) -> (a2 || a2) ~> b2
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
||| a2 ~> b2
a2 ~> b2
g2)

instance (CategoryOf j, CategoryOf k) => HasBinaryCoproducts (j +-> k) where
  type p || q = p :+: q
  withObCoprod :: forall (a :: j +-> k) (b :: j +-> k) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod Ob (a || b) => r
r = r
Ob (a || b) => r
r
  lft :: forall (a :: j +-> k) (b :: j +-> k). (Ob a, Ob b) => a ~> (a || b)
lft = (a :~> (a :+: b)) -> Prof a (a :+: b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof a a b -> (:+:) a b a b
a :~> (a :+: b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> (:+:) p q a b
InjL
  rgt :: forall (a :: j +-> k) (b :: j +-> k). (Ob a, Ob b) => b ~> (a || b)
rgt = (b :~> (a :+: b)) -> Prof b (a :+: b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof b a b -> (:+:) a b a b
b :~> (a :+: b)
forall {j} {k} (q :: j +-> k) (a :: k) (b :: j) (p :: j +-> k).
q a b -> (:+:) p q a b
InjR
  Prof x :~> a
l ||| :: forall (x :: j +-> k) (a :: j +-> k) (y :: j +-> k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Prof y :~> a
r = ((x :+: y) :~> a) -> Prof (x :+: y) a
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof ((x a b -> a a b) -> (y a b -> a a b) -> (:+:) x y a b -> a a b
forall {k} {j} (p :: k -> j -> Type) (x :: k) (y :: j) r
       (q :: k -> j -> Type).
(p x y -> r) -> (q x y -> r) -> (:+:) p q x y -> r
coproduct x a b -> a a b
x :~> a
l y a b -> a a b
y :~> a
r)

instance (HasBinaryCoproducts j, Corepresentable (p :: j +-> k), Corepresentable q) => Corepresentable (p :*: q) where
  type (p :*: q) %% a = (p %% a) || (q %% a)
  coindex :: forall (a :: k) (b :: j). (:*:) p q a b -> ((p :*: q) %% a) ~> b
coindex (p a b
p :*: q a b
q) = p a b -> (p %% a) ~> b
forall (a :: k) (b :: j). p a b -> (p %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex p a b
p ((p %% a) ~> b) -> ((q %% a) ~> b) -> ((p %% a) || (q %% a)) ~> b
forall (x :: j) (a :: j) (y :: j).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| q a b -> (q %% a) ~> b
forall (a :: k) (b :: j). q a b -> (q %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex q a b
q
  cotabulate :: forall (a :: k) (b :: j).
Ob a =>
(((p :*: q) %% a) ~> b) -> (:*:) p q a b
cotabulate @a ((p :*: q) %% a) ~> b
f =
    forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: j +-> k) (a :: k) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withObCorep @p @a
      (forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: j +-> k) (a :: k) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withObCorep @q @a (((p %% a) ~> b) -> p a b
forall (a :: k) (b :: j). Ob a => ((p %% a) ~> b) -> p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate (((p :*: q) %% a) ~> b
((p %% a) || (q %% a)) ~> b
f (((p %% a) || (q %% a)) ~> b)
-> ((p %% a) ~> ((p %% a) || (q %% a))) -> (p %% a) ~> b
forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @(p %% a) @(q %% a)) p a b -> q a b -> (:*:) p q a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> q a b -> (:*:) p q a b
:*: ((q %% a) ~> b) -> q a b
forall (a :: k) (b :: j). Ob a => ((q %% a) ~> b) -> q a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate (((p :*: q) %% a) ~> b
((p %% a) || (q %% a)) ~> b
f (((p %% a) || (q %% a)) ~> b)
-> ((q %% a) ~> ((p %% a) || (q %% a))) -> (q %% a) ~> b
forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @(p %% a) @(q %% a))))
  corepMap :: forall (a :: k) (b :: k).
(a ~> b) -> ((p :*: q) %% a) ~> ((p :*: q) %% b)
corepMap a ~> b
f = forall {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @p a ~> b
f ((p %% a) ~> (p %% b))
-> ((q %% a) ~> (q %% b))
-> ((p %% a) || (q %% a)) ~> ((p %% b) || (q %% b))
forall (a :: j) (b :: j) (x :: j) (y :: j).
(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 {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @q a ~> b
f

instance (HasBinaryCoproducts k) => HasBinaryCoproducts (PROD k) where
  type PR a || PR b = PR (a || b)
  withObCoprod :: forall (a :: PROD k) (b :: PROD k) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @(PR a) @(PR 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 PR a || UN PR b) => r
Ob (a || b) => r
r
  lft :: forall (a :: PROD k) (b :: PROD k). (Ob a, Ob b) => a ~> (a || b)
lft @(PR a) @(PR b) = (UN PR a ~> (UN PR a || UN PR b))
-> Prod (~>) (PR (UN PR a)) (PR (UN PR a || UN PR b))
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).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @a @b)
  rgt :: forall (a :: PROD k) (b :: PROD k). (Ob a, Ob b) => b ~> (a || b)
rgt @(PR a) @(PR b) = (UN PR b ~> (UN PR a || UN PR b))
-> Prod (~>) (PR (UN PR b)) (PR (UN PR a || UN PR b))
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).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @a @b)
  Prod a1 ~> b1
l ||| :: forall (x :: PROD k) (a :: PROD k) (y :: PROD k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Prod a1 ~> b1
r = ((a1 || a1) ~> b1) -> Prod (~>) (PR (a1 || a1)) (PR b1)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod (a1 ~> b1
l (a1 ~> b1) -> (a1 ~> b1) -> (a1 || a1) ~> b1
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
||| a1 ~> b1
a1 ~> b1
r)

type data COPROD k = COPR k

-- | Lifts a profunctor to the 'COPROD'-wrapped kinds, where the monoidal structure is the
-- coproduct.
type Coprod :: j +-> k -> COPROD j +-> COPROD k
data Coprod p a b where
  Coprod :: {forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Coprod p (COPR a) (COPR b) -> p a b
unCoprod :: p a b} -> Coprod p (COPR a) (COPR b)

instance (CategoryOf k) => Functor (COPR :: k -> COPROD k) where
  map :: forall (a :: k) (b :: k). (a ~> b) -> COPR a ~> COPR b
map = (a ~> b) -> COPR a ~> COPR b
(a ~> b) -> Coprod (~>) (COPR a) (COPR b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod

instance (Profunctor p) => Profunctor (Coprod p) where
  dimap :: forall (c :: COPROD k) (a :: COPROD k) (b :: COPROD j)
       (d :: COPROD j).
(c ~> a) -> (b ~> d) -> Coprod p a b -> Coprod p c d
dimap (Coprod a ~> b
l) (Coprod a ~> b
r) (Coprod p a b
p) = p a b -> Coprod p (COPR a) (COPR b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod ((a ~> a) -> (b ~> b) -> p a b -> p a b
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a ~> b
a ~> a
l a ~> b
b ~> b
r p a b
p)
  (Ob a, Ob b) => r
r \\ :: forall (a :: COPROD k) (b :: COPROD j) r.
((Ob a, Ob b) => r) -> Coprod p a b -> r
\\ Coprod p a b
f = 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 :: j) 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
f
instance (Promonad p) => Promonad (Coprod p) where
  id :: forall (a :: COPROD j). Ob a => Coprod p a a
id = p (UN COPR a) (UN COPR a)
-> Coprod p (COPR (UN COPR a)) (COPR (UN COPR a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod p (UN COPR a) (UN COPR a)
forall (a :: j). Ob a => p a a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
  Coprod p a b
f . :: forall (b :: COPROD j) (c :: COPROD j) (a :: COPROD j).
Coprod p b c -> Coprod p a b -> Coprod p a c
. Coprod p a b
g = p a b -> Coprod p (COPR a) (COPR b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod (p a b
f p a b -> p a a -> p a b
forall (b :: j) (c :: j) (a :: j). p b c -> p a b -> p a c
forall {k} (p :: CAT 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 (Representable p) => Representable (Coprod p) where
  type Coprod p % (COPR a) = COPR (p % a)
  index :: forall (a :: COPROD k) (b :: COPROD j).
Coprod p a b -> a ~> (Coprod p % b)
index (Coprod p a b
p) = (a ~> (p % b)) -> Coprod (~>) (COPR a) (COPR (p % b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod (p a b -> a ~> (p % b)
forall (a :: k) (b :: j). p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index p a b
p)
  tabulate :: forall (b :: COPROD j) (a :: COPROD k).
Ob b =>
(a ~> (Coprod p % b)) -> Coprod p a b
tabulate (Coprod a ~> b
f) = p a (UN COPR b) -> Coprod p (COPR a) (COPR (UN COPR b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod ((a ~> (p % UN COPR b)) -> p a (UN COPR b)
forall (b :: j) (a :: k). Ob b => (a ~> (p % b)) -> p a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate a ~> b
a ~> (p % UN COPR b)
f)
  repMap :: forall (a :: COPROD j) (b :: COPROD j).
(a ~> b) -> (Coprod p % a) ~> (Coprod p % b)
repMap (Coprod a ~> b
f) = ((p % a) ~> (p % b)) -> Coprod (~>) (COPR (p % a)) (COPR (p % b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p a ~> b
f)

instance
  (Profunctor f, Profunctor g, MonoidalProfunctor (Coprod f), MonoidalProfunctor (Coprod g))
  => MonoidalProfunctor (Coprod (f :.: g))
  where
  one :: Coprod (f :.: g) Unit Unit
one = (:.:) f g InitialObject InitialObject
-> Coprod (f :.: g) (COPR InitialObject) (COPR InitialObject)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod (f InitialObject InitialObject
forall {j} {k} (p :: j +-> k).
MonoidalProfunctor (Coprod p) =>
p InitialObject InitialObject
nil f InitialObject InitialObject
-> g InitialObject InitialObject
-> (:.:) f g InitialObject InitialObject
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: g InitialObject InitialObject
forall {j} {k} (p :: j +-> k).
MonoidalProfunctor (Coprod p) =>
p InitialObject InitialObject
nil)
  Coprod (f a b
f :.: g b b
g) ** :: forall (x1 :: COPROD k) (x2 :: COPROD j) (y1 :: COPROD k)
       (y2 :: COPROD j).
Coprod (f :.: g) x1 x2
-> Coprod (f :.: g) y1 y2 -> Coprod (f :.: g) (x1 ** y1) (x2 ** y2)
** Coprod (f a b
h :.: g b b
i) = (:.:) f g (a || a) (b || b)
-> Coprod (f :.: g) (COPR (a || a)) (COPR (b || b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod ((f a b
f f a b -> f a b -> f (a || a) (b || b)
forall {k} {k} (p :: k +-> k) (a :: k) (b :: k) (c :: k) (d :: k).
MonoidalProfunctor (Coprod p) =>
p a b -> p c d -> p (a || c) (b || d)
++ f a b
h) f (a || a) (b || b)
-> g (b || b) (b || b) -> (:.:) f g (a || a) (b || b)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (g b b
g g b b -> g b b -> g (b || b) (b || b)
forall {k} {k} (p :: k +-> k) (a :: k) (b :: k) (c :: k) (d :: k).
MonoidalProfunctor (Coprod p) =>
p a b -> p c d -> p (a || c) (b || d)
++ g b b
i))

-- | The same category as the category of @k@, but with coproducts as the tensor.
instance (CategoryOf k) => CategoryOf (COPROD k) where
  type (~>) = Coprod (~>)
  type Ob a = WrappedOb COPR a

instance (HasCoproducts k, cat ~ Hom k) => MonoidalProfunctor (Coprod cat :: COPROD k +-> COPROD k) where
  one :: Coprod cat Unit Unit
one = cat InitialObject InitialObject
-> Coprod cat (COPR InitialObject) (COPR InitialObject)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod cat InitialObject InitialObject
forall (a :: k). Ob a => cat a a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
  Coprod cat a b
f ** :: forall (x1 :: COPROD k) (x2 :: COPROD k) (y1 :: COPROD k)
       (y2 :: COPROD k).
Coprod cat x1 x2
-> Coprod cat y1 y2 -> Coprod cat (x1 ** y1) (x2 ** y2)
** Coprod cat a b
g = cat (a || a) (b || b) -> Coprod cat (COPR (a || a)) (COPR (b || b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod (cat a b
a ~> b
f (a ~> b) -> (a ~> b) -> (a || a) ~> (b || b)
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)
+++ cat a b
a ~> b
g)

instance (HasCoproducts k) => MonoidalProfunctor (Coprod (Id :: k +-> k)) where
  one :: Coprod Id Unit Unit
one = Id InitialObject InitialObject
-> Coprod Id (COPR InitialObject) (COPR InitialObject)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod ((InitialObject ~> InitialObject) -> Id InitialObject InitialObject
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id InitialObject ~> InitialObject
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id)
  Coprod (Id a ~> b
f) ** :: forall (x1 :: COPROD k) (x2 :: COPROD k) (y1 :: COPROD k)
       (y2 :: COPROD k).
Coprod Id x1 x2
-> Coprod Id y1 y2 -> Coprod Id (x1 ** y1) (x2 ** y2)
** Coprod (Id a ~> b
g) = Id (a || a) (b || b) -> Coprod Id (COPR (a || a)) (COPR (b || b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod (((a || a) ~> (b || b)) -> Id (a || a) (b || b)
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (a ~> b
f (a ~> b) -> (a ~> b) -> (a || a) ~> (b || b)
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)
+++ a ~> b
g))

instance (HasCoproducts j, HasCoproducts k) => MonoidalProfunctor (Coprod (TerminalProfunctor :: j +-> k)) where
  one :: Coprod TerminalProfunctor Unit Unit
one = TerminalProfunctor InitialObject InitialObject
-> Coprod
     TerminalProfunctor (COPR InitialObject) (COPR InitialObject)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod TerminalProfunctor InitialObject InitialObject
forall {j} {k} (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor
  Coprod (TerminalProfunctor @a1 @b1) ** :: forall (x1 :: COPROD k) (x2 :: COPROD j) (y1 :: COPROD k)
       (y2 :: COPROD j).
Coprod TerminalProfunctor x1 x2
-> Coprod TerminalProfunctor y1 y2
-> Coprod TerminalProfunctor (x1 ** y1) (x2 ** y2)
** Coprod (TerminalProfunctor @a2 @b2) =
    forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a1 @a2 ((Ob (a || a) => Coprod TerminalProfunctor (x1 ** y1) (x2 ** y2))
 -> Coprod TerminalProfunctor (x1 ** y1) (x2 ** y2))
-> (Ob (a || a) => Coprod TerminalProfunctor (x1 ** y1) (x2 ** y2))
-> Coprod TerminalProfunctor (x1 ** y1) (x2 ** y2)
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 @j @b1 @b2 ((Ob (b || b) => Coprod TerminalProfunctor (x1 ** y1) (x2 ** y2))
 -> Coprod TerminalProfunctor (x1 ** y1) (x2 ** y2))
-> (Ob (b || b) => Coprod TerminalProfunctor (x1 ** y1) (x2 ** y2))
-> Coprod TerminalProfunctor (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$ TerminalProfunctor (a || a) (b || b)
-> Coprod TerminalProfunctor (COPR (a || a)) (COPR (b || b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod TerminalProfunctor (a || a) (b || b)
forall {j} {k} (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor

nil :: (MonoidalProfunctor (Coprod p)) => p InitialObject InitialObject
nil :: forall {j} {k} (p :: j +-> k).
MonoidalProfunctor (Coprod p) =>
p InitialObject InitialObject
nil = Coprod p (COPR InitialObject) (COPR InitialObject)
-> p InitialObject InitialObject
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Coprod p (COPR a) (COPR b) -> p a b
unCoprod Coprod p Unit Unit
Coprod p (COPR InitialObject) (COPR InitialObject)
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one

(++) :: (MonoidalProfunctor (Coprod p)) => p a b -> p c d -> p (a || c) (b || d)
p a b
p ++ :: forall {k} {k} (p :: k +-> k) (a :: k) (b :: k) (c :: k) (d :: k).
MonoidalProfunctor (Coprod p) =>
p a b -> p c d -> p (a || c) (b || d)
++ p c d
q = Coprod p (COPR (a || c)) (COPR (b || d)) -> p (a || c) (b || d)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Coprod p (COPR a) (COPR b) -> p a b
unCoprod (p a b -> Coprod p (COPR a) (COPR b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod p a b
p Coprod p (COPR a) (COPR b)
-> Coprod p (COPR c) (COPR d)
-> Coprod p (COPR a ** COPR c) (COPR b ** COPR d)
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)
forall (x1 :: COPROD k) (x2 :: COPROD k) (y1 :: COPROD k)
       (y2 :: COPROD k).
Coprod p x1 x2 -> Coprod p y1 y2 -> Coprod p (x1 ** y1) (x2 ** y2)
** p c d -> Coprod p (COPR c) (COPR d)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod p c d
q)

instance (HasInitialObject k) => HasInitialObject (COPROD k) where
  type InitialObject = COPR InitialObject
  initiate :: forall (a :: COPROD k). Ob a => InitialObject ~> a
initiate = (InitialObject ~> UN COPR a)
-> Coprod (~>) (COPR InitialObject) (COPR (UN COPR a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod InitialObject ~> UN COPR a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate

instance (HasBinaryCoproducts k) => HasBinaryCoproducts (COPROD k) where
  type a || b = COPR (UN COPR a || UN COPR b)
  withObCoprod :: forall (a :: COPROD k) (b :: COPROD k) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @(COPR a) @(COPR 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 COPR a || UN COPR b) => r
Ob (a || b) => r
r
  lft :: forall (a :: COPROD k) (b :: COPROD k).
(Ob a, Ob b) =>
a ~> (a || b)
lft @(COPR a) @(COPR b) = (UN COPR a ~> (UN COPR a || UN COPR b))
-> Coprod (~>) (COPR (UN COPR a)) (COPR (UN COPR a || UN COPR b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @b)
  rgt :: forall (a :: COPROD k) (b :: COPROD k).
(Ob a, Ob b) =>
b ~> (a || b)
rgt @(COPR a) @(COPR b) = (UN COPR b ~> (UN COPR a || UN COPR b))
-> Coprod (~>) (COPR (UN COPR b)) (COPR (UN COPR a || UN COPR b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @b)
  Coprod a ~> b
f ||| :: forall (x :: COPROD k) (a :: COPROD k) (y :: COPROD k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Coprod a ~> b
g = ((a || a) ~> b) -> Coprod (~>) (COPR (a || a)) (COPR b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod (a ~> b
f (a ~> b) -> (a ~> b) -> (a || a) ~> b
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
||| a ~> b
a ~> b
g)

instance (HasTerminalObject k) => HasTerminalObject (COPROD k) where
  type TerminalObject = COPR TerminalObject
  terminate :: forall (a :: COPROD k). Ob a => a ~> TerminalObject
terminate = (UN COPR a ~> TerminalObject)
-> Coprod (~>) (COPR (UN COPR a)) (COPR TerminalObject)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod UN COPR a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate

instance (HasBinaryProducts k) => HasBinaryProducts (COPROD k) where
  type COPR a && COPR b = COPR (a && b)
  withObProd :: forall (a :: COPROD k) (b :: COPROD k) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @(COPR a) @(COPR 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 COPR a && UN COPR b) => r
Ob (a && b) => r
r
  fst :: forall (a :: COPROD k) (b :: COPROD k).
(Ob a, Ob b) =>
(a && b) ~> a
fst @(COPR a) @(COPR b) = ((UN COPR a && UN COPR b) ~> UN COPR a)
-> Coprod (~>) (COPR (UN COPR a && UN COPR b)) (COPR (UN COPR a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @a @b)
  snd :: forall (a :: COPROD k) (b :: COPROD k).
(Ob a, Ob b) =>
(a && b) ~> b
snd @(COPR a) @(COPR b) = ((UN COPR a && UN COPR b) ~> UN COPR b)
-> Coprod (~>) (COPR (UN COPR a && UN COPR b)) (COPR (UN COPR b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @a @b)
  Coprod a ~> b
f &&& :: forall (a :: COPROD k) (x :: COPROD k) (y :: COPROD k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Coprod a ~> b
g = (a ~> (b && b)) -> Coprod (~>) (COPR a) (COPR (b && b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod (a ~> b
f (a ~> b) -> (a ~> b) -> a ~> (b && b)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> b
a ~> b
g)

-- | Coproducts as monoidal tensor.
instance (HasCoproducts k) => Monoidal (COPROD k) where
  type Unit = COPR InitialObject
  type a ** b = COPR (UN COPR a || UN COPR b)
  withOb2 :: forall (a :: COPROD k) (b :: COPROD k) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @(COPR a) @(COPR 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 COPR a || UN COPR b) => r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: COPROD k). Ob a => (Unit ** a) ~> a
leftUnitor = ((InitialObject || UN COPR a) ~> UN COPR a)
-> Coprod
     (~>) (COPR (InitialObject || UN COPR a)) (COPR (UN COPR a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod (InitialObject || UN COPR a) ~> UN COPR a
forall {k} (a :: k).
(HasCoproducts k, Ob a) =>
(InitialObject || a) ~> a
leftUnitorCoprod
  leftUnitorInv :: forall (a :: COPROD k). Ob a => a ~> (Unit ** a)
leftUnitorInv = (UN COPR a ~> (InitialObject || UN COPR a))
-> Coprod
     (~>) (COPR (UN COPR a)) (COPR (InitialObject || UN COPR a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod UN COPR a ~> (InitialObject || UN COPR a)
forall {k} (a :: k).
(HasCoproducts k, Ob a) =>
a ~> (InitialObject || a)
leftUnitorCoprodInv
  rightUnitor :: forall (a :: COPROD k). Ob a => (a ** Unit) ~> a
rightUnitor = ((UN COPR a || InitialObject) ~> UN COPR a)
-> Coprod
     (~>) (COPR (UN COPR a || InitialObject)) (COPR (UN COPR a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod (UN COPR a || InitialObject) ~> UN COPR a
forall {k} (a :: k).
(HasCoproducts k, Ob a) =>
(a || InitialObject) ~> a
rightUnitorCoprod
  rightUnitorInv :: forall (a :: COPROD k). Ob a => a ~> (a ** Unit)
rightUnitorInv = (UN COPR a ~> (UN COPR a || InitialObject))
-> Coprod
     (~>) (COPR (UN COPR a)) (COPR (UN COPR a || InitialObject))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod UN COPR a ~> (UN COPR a || InitialObject)
forall {k} (a :: k).
(HasCoproducts k, Ob a) =>
a ~> (a || InitialObject)
rightUnitorCoprodInv
  associator :: forall (a :: COPROD k) (b :: COPROD k) (c :: COPROD k).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(COPR a) @(COPR b) @(COPR c) = (((UN COPR a || UN COPR b) || UN COPR c)
 ~> (UN COPR a || (UN COPR b || UN COPR c)))
-> Coprod
     (~>)
     (COPR ((UN COPR a || UN COPR b) || UN COPR c))
     (COPR (UN COPR a || (UN COPR b || UN COPR c)))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod (forall (a :: k) (b :: k) (c :: k).
(HasCoproducts k, Ob a, Ob b, Ob c) =>
((a || b) || c) ~> (a || (b || c))
forall {k} (a :: k) (b :: k) (c :: k).
(HasCoproducts k, Ob a, Ob b, Ob c) =>
((a || b) || c) ~> (a || (b || c))
associatorCoprod @a @b @c)
  associatorInv :: forall (a :: COPROD k) (b :: COPROD k) (c :: COPROD k).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(COPR a) @(COPR b) @(COPR c) = ((UN COPR a || (UN COPR b || UN COPR c))
 ~> ((UN COPR a || UN COPR b) || UN COPR c))
-> Coprod
     (~>)
     (COPR (UN COPR a || (UN COPR b || UN COPR c)))
     (COPR ((UN COPR a || UN COPR b) || UN COPR c))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod (forall (a :: k) (b :: k) (c :: k).
(HasCoproducts k, Ob a, Ob b, Ob c) =>
(a || (b || c)) ~> ((a || b) || c)
forall {k} (a :: k) (b :: k) (c :: k).
(HasCoproducts k, Ob a, Ob b, Ob c) =>
(a || (b || c)) ~> ((a || b) || c)
associatorCoprodInv @a @b @c)

leftUnitorCoprod :: forall {k} (a :: k). (HasCoproducts k, Ob a) => (InitialObject || a) ~> a
leftUnitorCoprod :: forall {k} (a :: k).
(HasCoproducts k, Ob a) =>
(InitialObject || a) ~> a
leftUnitorCoprod = InitialObject ~> a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate (InitialObject ~> a) -> (a ~> a) -> (InitialObject || a) ~> a
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
||| a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id

leftUnitorCoprodInv :: forall {k} (a :: k). (HasCoproducts k, Ob a) => a ~> (InitialObject || a)
leftUnitorCoprodInv :: forall {k} (a :: k).
(HasCoproducts k, Ob a) =>
a ~> (InitialObject || a)
leftUnitorCoprodInv = forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @InitialObject @a

rightUnitorCoprod :: forall {k} (a :: k). (HasCoproducts k, Ob a) => (a || InitialObject) ~> a
rightUnitorCoprod :: forall {k} (a :: k).
(HasCoproducts k, Ob a) =>
(a || InitialObject) ~> a
rightUnitorCoprod = a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id (a ~> a) -> (InitialObject ~> a) -> (a || InitialObject) ~> a
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
||| InitialObject ~> a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate

rightUnitorCoprodInv :: forall {k} (a :: k). (HasCoproducts k, Ob a) => a ~> (a || InitialObject)
rightUnitorCoprodInv :: forall {k} (a :: k).
(HasCoproducts k, Ob a) =>
a ~> (a || InitialObject)
rightUnitorCoprodInv = forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @InitialObject

associatorCoprod :: forall {k} (a :: k) b c. (HasCoproducts k, Ob a, Ob b, Ob c) => (a || b) || c ~> a || (b || c)
associatorCoprod :: forall {k} (a :: k) (b :: k) (c :: k).
(HasCoproducts k, Ob a, Ob b, Ob c) =>
((a || b) || c) ~> (a || (b || c))
associatorCoprod = (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (b ~> (b || c)) -> (a || b) ~> (a || (b || 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 k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @b @c) ((a || b) ~> (a || (b || c)))
-> (c ~> (a || (b || c))) -> ((a || b) || c) ~> (a || (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) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @b @c (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @(b || c)) ((b || c) ~> (a || (b || c)))
-> (c ~> (b || c)) -> c ~> (a || (b || c))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @b @c

associatorCoprodInv :: forall {k} (a :: k) b c. (HasCoproducts k, Ob a, Ob b, Ob c) => a || (b || c) ~> (a || b) || c
associatorCoprodInv :: forall {k} (a :: k) (b :: k) (c :: k).
(HasCoproducts k, Ob a, Ob b, Ob c) =>
(a || (b || c)) ~> ((a || b) || c)
associatorCoprodInv = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a @b (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @(a || b) @c) ((a || b) ~> ((a || b) || c))
-> (a ~> (a || b)) -> a ~> ((a || b) || c)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @b (a ~> ((a || b) || c))
-> ((b || c) ~> ((a || b) || c))
-> (a || (b || c)) ~> ((a || 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).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @b (b ~> (a || b)) -> (c ~> c) -> (b || c) ~> ((a || b) || 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). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c)

instance (HasCoproducts k) => SymMonoidal (COPROD k) where
  swap :: forall (a :: COPROD k) (b :: COPROD k).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @(COPR a) @(COPR b) = ((UN COPR a || UN COPR b) ~> (UN COPR b || UN COPR a))
-> Coprod
     (~>)
     (COPR (UN COPR a || UN COPR b))
     (COPR (UN COPR b || UN COPR a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod (forall (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(a || b) ~> (b || a)
forall {k} (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(a || b) ~> (b || a)
swapCoprod @a @b)

-- | Inverse to 'Coprod': strips the 'COPR' wrappers from a profunctor between 'COPROD'-wrapped
-- kinds.
type Uncoprod :: (COPROD j +-> COPROD k) -> j +-> k
data Uncoprod p a b where
  Uncoprod :: p (COPR a) (COPR b) -> Uncoprod p a b

instance (Profunctor p, CategoryOf j, CategoryOf k) => Profunctor (Uncoprod p :: j +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Uncoprod p a b -> Uncoprod p c d
dimap c ~> a
l b ~> d
r (Uncoprod p (COPR a) (COPR b)
p) = p (COPR c) (COPR d) -> Uncoprod p c d
forall {k} {k} (p :: COPROD k +-> COPROD k) (a :: k) (b :: k).
p (COPR a) (COPR b) -> Uncoprod p a b
Uncoprod ((COPR c ~> COPR a)
-> (COPR b ~> COPR d) -> p (COPR a) (COPR b) -> p (COPR c) (COPR d)
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall (c :: COPROD k) (a :: COPROD k) (b :: COPROD j)
       (d :: COPROD j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap ((c ~> a) -> Coprod (~>) (COPR c) (COPR a)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod c ~> a
l) ((b ~> d) -> Coprod (~>) (COPR b) (COPR d)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p (COPR a) (COPR b)
Coprod b ~> d
r) p (COPR a) (COPR b)
p ((Ob (COPR a), Ob (COPR b)) => p (COPR c) (COPR d))
-> p (COPR a) (COPR b) -> p (COPR c) (COPR d)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: COPROD k) (b :: COPROD j) r.
((Ob a, Ob b) => r) -> p a b -> r
\\ p (COPR a) (COPR b)
p)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> Uncoprod p a b -> r
\\ Uncoprod p (COPR a) (COPR b)
f = r
(Ob a, Ob b) => r
(Ob (COPR a), Ob (COPR b)) => r
r ((Ob (COPR a), Ob (COPR b)) => r) -> p (COPR a) (COPR b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: COPROD k) (b :: COPROD j) r.
((Ob a, Ob b) => r) -> p a b -> r
\\ p (COPR a) (COPR b)
f

data family (+) (a :: k) (b :: k) :: k
instance (IsFreeOb (a :: FREE cs p), IsFreeOb b, HasBinaryCoproducts `Elem` cs) => IsFreeOb (a + b) where
  type Lower f (a + b) = Lower f a || Lower f b
  lowerOb :: forall k' (f :: k +-> k') r.
(Representable f, All cs k') =>
(Ob (Lower f (a + b)) => r) -> r
lowerOb @k' @f Ob (Lower f (a + b)) => r
r =
    forall (c :: Type -> Constraint) (cs :: [Type -> Constraint]) k r.
(Elem c cs, All cs k) =>
(c k => r) -> r
fromAll @HasBinaryCoproducts @cs @k'
      (forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a (forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @b (forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k' @(Lower f a) @(Lower f b) r
Ob (Lower f (a + b)) => r
Ob (Lower f a || Lower f b) => r
r)))
instance (HasBinaryCoproducts `Elem` cs) => HasStructure cs (p :: CAT k) HasBinaryCoproducts where
  data Struct HasBinaryCoproducts i o where
    Lft :: (Ob a, Ob b) => Struct HasBinaryCoproducts a (a + b)
    Rgt :: (Ob a, Ob b) => Struct HasBinaryCoproducts b (a + b)
    Sum :: a ~> o -> b ~> o -> Struct HasBinaryCoproducts (a + b) o
  foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p).
(HasBinaryCoproducts k', All cs k', Representable f) =>
(forall (x :: FREE cs p) (y :: FREE cs p).
 (x ~> y) -> Lower f x ~> Lower f y)
-> Struct HasBinaryCoproducts a b -> Lower f a ~> Lower f b
foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (Lft @a @b) = forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a (forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @b (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @(Lower f a) @(Lower f b)))
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (Rgt @a @b) = forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a (forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @b (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @(Lower f a) @(Lower f b)))
  foldStructure forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go (Sum a ~> b
g b ~> b
h) = (a ~> b) -> Lower f a ~> Lower f b
forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go a ~> b
g (Lower f a ~> Lower f b)
-> (Lower f b ~> Lower f b)
-> (Lower f a || Lower f b) ~> Lower f b
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
||| (b ~> b) -> Lower f b ~> Lower f b
forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go b ~> b
h
instance (WithShow a) => Show (Struct HasBinaryCoproducts a b) where
  showsPrec :: Int -> Struct HasBinaryCoproducts a b -> ShowS
showsPrec Int
_ Struct HasBinaryCoproducts a b
R:StructkcspHasBinaryCoproductsio k cs p a b
Lft = String -> ShowS
P.showString String
"lft"
  showsPrec Int
_ Struct HasBinaryCoproducts a b
R:StructkcspHasBinaryCoproductsio k cs p a b
Rgt = String -> ShowS
P.showString String
"rgt"
  showsPrec Int
d (Sum a ~> b
f b ~> b
g) =
    Bool -> ShowS -> ShowS
P.showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
P.> Int
4) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
P.$
      Int -> Free a b -> ShowS
forall a. Show a => Int -> a -> ShowS
P.showsPrec Int
5 a ~> b
Free a b
f ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. String -> ShowS
P.showString String
" ||| " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Int -> Free b b -> ShowS
forall a. Show a => Int -> a -> ShowS
P.showsPrec Int
5 b ~> b
Free b b
g
instance (HasBinaryCoproducts `Elem` cs) => HasBinaryCoproducts (FREE cs (p :: CAT k)) where
  type a || b = a + b
  withObCoprod :: forall (a :: FREE cs p) (b :: FREE cs p) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod Ob (a || b) => r
r = r
Ob (a || b) => r
r
  lft :: forall (a :: FREE cs p) (b :: FREE cs p).
(Ob a, Ob b) =>
a ~> (a || b)
lft = Struct HasBinaryCoproducts a (a + b) -> Free a a -> Free a (a + b)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
F.St Struct HasBinaryCoproducts a (a + b)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p) (a :: FREE cs p).
(Ob a, Ob a) =>
Struct HasBinaryCoproducts a (a + a)
Lft Free a a
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
F.Nil
  rgt :: forall (a :: FREE cs p) (b :: FREE cs p).
(Ob a, Ob b) =>
b ~> (a || b)
rgt = Struct HasBinaryCoproducts b (a + b) -> Free b b -> Free b (a + b)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
F.St Struct HasBinaryCoproducts b (a + b)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p) (b :: FREE cs p).
(Ob a, Ob b) =>
Struct HasBinaryCoproducts b (a + b)
Rgt Free b b
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
F.Nil
  x ~> a
f ||| :: forall (x :: FREE cs p) (a :: FREE cs p) (y :: FREE cs p).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| y ~> a
g = Struct HasBinaryCoproducts (x + y) a
-> Free (x + y) (x + y) -> Free (x + y) a
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
F.St ((x ~> a) -> (y ~> a) -> Struct HasBinaryCoproducts (x + y) a
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p) (o :: FREE cs p) (b :: FREE cs p).
(a ~> o) -> (b ~> o) -> Struct HasBinaryCoproducts (a + b) o
Sum x ~> a
f y ~> a
g) Free (x + y) (x + y)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
F.Nil ((Ob x, Ob a) => Free (x + y) a) -> Free x a -> Free (x + y) a
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FREE cs p) (b :: FREE cs p) r.
((Ob a, Ob b) => r) -> Free a b -> r
\\ x ~> a
Free x a
f ((Ob y, Ob a) => Free (x + y) a) -> Free y a -> Free (x + y) a
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FREE cs p) (b :: FREE cs p) r.
((Ob a, Ob b) => r) -> Free a b -> r
\\ y ~> a
Free y a
g

class ((a && b) ~ (a || b)) => CheckBiproduct a b
instance ((a && b) ~ (a || b)) => CheckBiproduct a b

class
  (HasBinaryCoproducts k, HasBinaryProducts k, forall (a :: k) (b :: k). (Ob a, Ob b) => CheckBiproduct a b) =>
  HasBiproducts k
  where
  sum :: (a :: k) ~> b -> a ~> b -> a ~> b
  sum a ~> b
f a ~> b
g = (b || b) ~> b
forall {k} (a :: k). (HasBinaryCoproducts k, Ob a) => (a || a) ~> a
codiag ((b || b) ~> b) -> (a ~> (b || b)) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ~> b
f (a ~> b) -> (a ~> b) -> (a || a) ~> (b || b)
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)
+++ a ~> b
g) ((a || a) ~> (b || b)) -> (a ~> (a || a)) -> a ~> (b || b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (a && a)
a ~> (a || a)
forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
diag ((Ob a, Ob b) => a ~> b) -> (a ~> b) -> a ~> b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ a ~> b
f ((Ob a, Ob b) => a ~> b) -> (a ~> b) -> a ~> b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ a ~> b
g

instance (HasBinaryCoproducts k) => HasBinaryProducts (OPPOSITE k) where
  type a && b = OP (UN OP a || UN OP b)
  withObProd :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @(OP a) @(OP 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 OP a || UN OP b) => r
Ob (a && b) => r
r
  fst :: forall (a :: OPPOSITE k) (b :: OPPOSITE k).
(Ob a, Ob b) =>
(a && b) ~> a
fst @(OP a) @(OP b) = (UN OP a ~> (UN OP a || UN OP b))
-> Op (~>) (OP (UN OP a || UN OP b)) (OP (UN OP a))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p (OP a1) (OP b1)
Op (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @a @b)
  snd :: forall (a :: OPPOSITE k) (b :: OPPOSITE k).
(Ob a, Ob b) =>
(a && b) ~> b
snd @(OP a) @(OP b) = (UN OP b ~> (UN OP a || UN OP b))
-> Op (~>) (OP (UN OP a || UN OP b)) (OP (UN OP b))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p (OP a1) (OP b1)
Op (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @a @b)
  Op b1 ~> a1
a &&& :: forall (a :: OPPOSITE k) (x :: OPPOSITE k) (y :: OPPOSITE k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Op b1 ~> a1
b = ((b1 || b1) ~> a1) -> Op (~>) (OP a1) (OP (b1 || b1))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p (OP a1) (OP b1)
Op (b1 ~> a1
a (b1 ~> a1) -> (b1 ~> a1) -> (b1 || b1) ~> a1
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
||| b1 ~> a1
b1 ~> a1
b)

instance (HasBinaryProducts k) => HasBinaryCoproducts (OPPOSITE k) where
  type a || b = OP (UN OP a && UN OP b)
  withObCoprod :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @(OP a) @(OP 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 OP a && UN OP b) => r
Ob (a || b) => r
r
  lft :: forall (a :: OPPOSITE k) (b :: OPPOSITE k).
(Ob a, Ob b) =>
a ~> (a || b)
lft @(OP a) @(OP b) = ((UN OP a && UN OP b) ~> UN OP a)
-> Op (~>) (OP (UN OP a)) (OP (UN OP a && UN OP b))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p (OP a1) (OP b1)
Op (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @a @b)
  rgt :: forall (a :: OPPOSITE k) (b :: OPPOSITE k).
(Ob a, Ob b) =>
b ~> (a || b)
rgt @(OP a) @(OP b) = ((UN OP a && UN OP b) ~> UN OP b)
-> Op (~>) (OP (UN OP b)) (OP (UN OP a && UN OP b))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p (OP a1) (OP b1)
Op (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @a @b)
  Op b1 ~> a1
a ||| :: forall (x :: OPPOSITE k) (a :: OPPOSITE k) (y :: OPPOSITE k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Op b1 ~> a1
b = (b1 ~> (a1 && a1)) -> Op (~>) (OP (a1 && a1)) (OP b1)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p (OP a1) (OP b1)
Op (b1 ~> a1
a (b1 ~> a1) -> (b1 ~> a1) -> b1 ~> (a1 && a1)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& b1 ~> a1
b1 ~> a1
b)

-- | The left adjoint to the diagonal functor.
instance (HasBinaryCoproducts k) => Corepresentable (Rep Diag :: k +-> (k, k)) where
  type Rep Diag %% '(a, b) = a || b
  coindex :: forall (a :: (k, k)) (b :: k). Rep Diag a b -> (Rep Diag %% a) ~> b
coindex (Rep (a1 ~> b1
f :**: a2 ~> b2
g)) = a1 ~> b
a1 ~> b1
f (a1 ~> b) -> (a2 ~> b) -> (a1 || a2) ~> b
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
||| a2 ~> b
a2 ~> b2
g
  corepUniv :: forall (a :: (k, k)). Ob a => Rep Diag a (Rep Diag %% a)
corepUniv @'(a, b) = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a @b (('(Fst @ a, Snd @ a) ~> (Diag @ ((Fst @ a) || (Snd @ a))))
-> Rep Diag '(Fst @ a, Snd @ a) ((Fst @ a) || (Snd @ a))
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @b ((Fst @ a) ~> ((Fst @ a) || (Snd @ a)))
-> ((Snd @ a) ~> ((Fst @ a) || (Snd @ a)))
-> (:**:)
     (~>)
     (~>)
     '(Fst @ a, Snd @ a)
     '((Fst @ a) || (Snd @ a), (Fst @ a) || (Snd @ a))
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @b))

-- | The universal property of the binary coproduct: the injections recover the components of
-- @f '|||' g@, and every arrow out of the coproduct is the copairing of its components.
instance Laws '[HasBinaryCoproducts] where
  laws :: [Law '[HasBinaryCoproducts]]
laws =
    [ String
-> LawBody '[HasBinaryCoproducts] -> Law '[HasBinaryCoproducts]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"lft" \ @a @b @c forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> do
        f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @a @c String
"f"
        g <- mor @b @c "g"
        f === (f ||| g) . lft @_ @a @b
    , String
-> LawBody '[HasBinaryCoproducts] -> Law '[HasBinaryCoproducts]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"rgt" \ @a @b @c forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> do
        f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @a @c String
"f"
        g <- mor @b @c "g"
        g === (f ||| g) . rgt @_ @a @b
    , String
-> LawBody '[HasBinaryCoproducts] -> Law '[HasBinaryCoproducts]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"copairing naturality" \ @a @b @c @d forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> do
        f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @a @c String
"f"
        g <- mor @b @c "g"
        h <- mor @c @d "h"
        (h . f) ||| (h . g) === h . (f ||| g)
    , String
-> LawBody '[HasBinaryCoproducts] -> Law '[HasBinaryCoproducts]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"copairing the injections" \ @a @b forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ ->
        forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @a @b (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @a @b (a ~> (a || b)) -> (b ~> (a || b)) -> (a || b) ~> (a || b)
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).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @a @b ((a || b) ~> (a || b)) -> ((a || b) ~> (a || b)) -> m (Equation k)
forall {i} (m :: Type -> Type) r (a :: i) (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== (a || b) ~> (a || b)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id)
    , String
-> LawBody '[HasBinaryCoproducts] -> Law '[HasBinaryCoproducts]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"copairing uniqueness" \ @a @b @c forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @a @b do
        p <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @(a || b) @c String
"p"
        p === (p . lft @_ @a @b) ||| (p . rgt @_ @a @b)
    ]