module Proarrow.Category.Instance.Coproduct where

import Data.Kind (Constraint)

import Proarrow.Core (CAT, CategoryOf(..), Promonad(..), Profunctor(..), IsCategoryOf)

data COPRODUCT j k = L j | R k

type (:++:) :: CAT j -> CAT k -> CAT (COPRODUCT j k)
data (c :++: d) a b where
  InjL :: c a b -> (c :++: d) (L a) (L b)
  InjR :: d a b -> (c :++: d) (R a) (R b)

type IsCoproduct :: forall {j} {k}. COPRODUCT j k -> Constraint
class IsCoproduct (a :: COPRODUCT j k) where
  coproductId :: ((~>) :++: (~>)) a a
instance (Ob a, Promonad ((~>) :: CAT k)) => IsCoproduct (L (a :: k)) where
  coproductId :: (:++:) (~>) (~>) ('L a) ('L a)
coproductId = (a ~> a) -> (:++:) (~>) (~>) ('L a) ('L a)
forall {j} {k} (c :: CAT j) (a :: j) (b :: j) (d :: CAT k).
c a b -> (:++:) c d ('L a) ('L b)
InjL 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
instance (Ob a, Promonad ((~>) :: CAT k)) => IsCoproduct (R (a :: k)) where
  coproductId :: (:++:) (~>) (~>) ('R a) ('R a)
coproductId = (a ~> a) -> (:++:) (~>) (~>) ('R a) ('R a)
forall {k} {j} (d :: CAT k) (a :: k) (b :: k) (c :: CAT j).
d a b -> (:++:) c d ('R a) ('R b)
InjR 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

instance (CategoryOf j, CategoryOf k) => CategoryOf (COPRODUCT j k) where
  type (~>) = (~>) :++: (~>)
  type Ob a = IsCoproduct a

-- | The coproduct category of the categories `c` and `d`.
instance (IsCategoryOf j c, IsCategoryOf k d) => Promonad ((c :++: d) :: CAT (COPRODUCT j k)) where
  id :: forall (a :: COPRODUCT j k). Ob a => (:++:) c d a a
id = (:++:) c d a a
(:++:) (~>) (~>) a a
forall {j} {k} (a :: COPRODUCT j k).
IsCoproduct a =>
(:++:) (~>) (~>) a a
coproductId
  InjL c a b
f . :: forall (b :: COPRODUCT j k) (c :: COPRODUCT j k)
       (a :: COPRODUCT j k).
(:++:) c d b c -> (:++:) c d a b -> (:++:) c d a c
. InjL c a b
g = c a b -> (:++:) c d ('L a) ('L b)
forall {j} {k} (c :: CAT j) (a :: j) (b :: j) (d :: CAT k).
c a b -> (:++:) c d ('L a) ('L b)
InjL (c a b
f c a b -> c a a -> c a b
forall (b :: j) (c :: j) (a :: j). c b c -> c a b -> c a c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c a a
c a b
g)
  InjR d a b
f . InjR d a b
g = d a b -> (:++:) c d ('R a) ('R b)
forall {k} {j} (d :: CAT k) (a :: k) (b :: k) (c :: CAT j).
d a b -> (:++:) c d ('R a) ('R b)
InjR (d a b
f d a b -> d a a -> d a b
forall (b :: k) (c :: k) (a :: k). d b c -> d a b -> d a c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. d a a
d a b
g)

instance (Profunctor c, Profunctor d) => Profunctor (c :++: d) where
  dimap :: forall (c :: COPRODUCT j k) (a :: COPRODUCT j k)
       (b :: COPRODUCT j k) (d :: COPRODUCT j k).
(c ~> a) -> (b ~> d) -> (:++:) c d a b -> (:++:) c d c d
dimap (InjL a ~> b
l) (InjL a ~> b
r) (InjL c a b
f) = c a b -> (:++:) c d ('L a) ('L b)
forall {j} {k} (c :: CAT j) (a :: j) (b :: j) (d :: CAT k).
c a b -> (:++:) c d ('L a) ('L b)
InjL ((a ~> a) -> (b ~> b) -> c a b -> c a b
forall (c :: j) (a :: j) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> c a b -> c c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a ~> b
a ~> a
l a ~> b
b ~> b
r c a b
f)
  dimap (InjR a ~> b
l) (InjR a ~> b
r) (InjR d a b
f) = d a b -> (:++:) c d ('R a) ('R b)
forall {k} {j} (d :: CAT k) (a :: k) (b :: k) (c :: CAT j).
d a b -> (:++:) c d ('R a) ('R b)
InjR ((a ~> a) -> (b ~> b) -> d a b -> d a b
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> d a b -> d c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a ~> b
a ~> a
l a ~> b
b ~> b
r d a b
f)
  dimap (InjL a ~> b
_) (InjR a ~> b
_) (:++:) c d a b
f = case (:++:) c d a b
f of
  dimap (InjR a ~> b
_) (InjL a ~> b
_) (:++:) c d a b
f = case (:++:) c d a b
f of
  (Ob a, Ob b) => r
r \\ :: forall (a :: COPRODUCT j k) (b :: COPRODUCT j k) r.
((Ob a, Ob b) => r) -> (:++:) c d a b -> r
\\ InjL c a b
f = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> c a b -> r
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> c 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
\\ c a b
f
  (Ob a, Ob b) => r
r \\ InjR d a b
f = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> d a b -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> d 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
\\ d a b
f