module Proarrow.Profunctor.Instance.Cocone where

import Proarrow.Category.Monoidal (MonoidalProfunctor (..))
import Proarrow.Colimit.BinaryCoproduct (COPROD (..), Coprod (..), HasBinaryCoproducts (..), HasCoproducts)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), UN, rmap, type (+->))
import Proarrow.Profunctor.Instance.List (LIST (..), List (..))

-- | A cocone is a bunch of arrows with a shared target.
data Cocone (bs :: LIST k) (a :: COPROD k) where
  Coapex :: (Ob a) => Cocone (L '[]) (COPR a)
  Coleg :: b ~> a -> Cocone (L bs) (COPR a) -> Cocone (L (b : bs)) (COPR a)

instance (CategoryOf k) => Profunctor (Cocone :: COPROD k +-> LIST k) where
  dimap :: forall (c :: LIST k) (a :: LIST k) (b :: COPROD k) (d :: COPROD k).
(c ~> a) -> (b ~> d) -> Cocone a b -> Cocone c d
dimap c ~> a
List (~>) c a
Nil b ~> d
r Cocone a b
Coapex = Cocone c d
Cocone (L '[]) ('COPR (UN 'COPR d))
(Ob ('COPR a), Ob d) => Cocone c d
forall {k} (b :: k). Ob b => Cocone (L '[]) ('COPR b)
Coapex ((Ob ('COPR a), Ob d) => Cocone c d)
-> Coprod (~>) ('COPR a) d -> Cocone c 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 k) r.
((Ob a, Ob b) => r) -> Coprod (~>) a b -> r
\\ b ~> d
Coprod (~>) ('COPR a) d
r
  dimap (Cons a ~> b
l List (~>) (L as1) (L bs1)
ls) r :: b ~> d
r@(Coprod a1 ~> b1
r') (Coleg b ~> a
f Cocone (L bs) ('COPR a)
fs) = (a ~> b1)
-> Cocone (L as1) ('COPR b1) -> Cocone (L (a : as1)) ('COPR b1)
forall {k} (b :: k) (a :: k) (bs :: [k]).
(b ~> a)
-> Cocone (L bs) ('COPR a) -> Cocone (L (b : bs)) ('COPR a)
Coleg (a1 ~> b1
r' (a1 ~> b1) -> (a ~> a1) -> a ~> b1
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b ~> a1
b ~> a
f (b ~> a1) -> (a ~> b) -> a ~> a1
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b
l) ((L as1 ~> L bs)
-> ('COPR a ~> 'COPR b1)
-> Cocone (L bs) ('COPR a)
-> Cocone (L as1) ('COPR b1)
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 :: LIST k) (a :: LIST k) (b :: COPROD k) (d :: COPROD k).
(c ~> a) -> (b ~> d) -> Cocone a b -> Cocone c d
dimap L as1 ~> L bs
List (~>) (L as1) (L bs1)
ls b ~> d
'COPR a ~> 'COPR b1
r Cocone (L bs) ('COPR a)
fs)
  (Ob a, Ob b) => r
r \\ :: forall (a :: LIST k) (b :: COPROD k) r.
((Ob a, Ob b) => r) -> Cocone a b -> r
\\ Cocone a b
Coapex = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ Coleg b ~> a
l Cocone (L bs) ('COPR a)
Coapex = r
(Ob b, Ob a) => r
(Ob a, Ob b) => r
r ((Ob b, Ob a) => r) -> (b ~> a) -> r
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 ~> a
l
  (Ob a, Ob b) => r
r \\ Coleg b ~> a
l c :: Cocone (L bs) ('COPR a)
c@(Coleg b ~> a
_ Cocone (L bs) ('COPR a)
c1) = r
(Ob b, Ob a) => r
(Ob a, Ob b) => r
r ((Ob b, Ob a) => r) -> (b ~> a) -> r
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 ~> a
l ((Ob (L bs), Ob ('COPR a)) => r) -> Cocone (L bs) ('COPR a) -> 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 :: LIST k) (b :: COPROD k) r.
((Ob a, Ob b) => r) -> Cocone a b -> r
\\ Cocone (L bs) ('COPR a)
c ((Ob (L bs), Ob ('COPR a)) => r) -> Cocone (L bs) ('COPR a) -> 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 :: LIST k) (b :: COPROD k) r.
((Ob a, Ob b) => r) -> Cocone a b -> r
\\ Cocone (L bs) ('COPR a)
c1

instance (HasCoproducts k) => MonoidalProfunctor (Cocone :: COPROD k +-> LIST k) where
  one :: Cocone Unit Unit
one = Cocone Unit Unit
Cocone (L '[]) ('COPR InitialObject)
forall {k} (b :: k). Ob b => Cocone (L '[]) ('COPR b)
Coapex
  Coapex @l ** :: forall (x1 :: LIST k) (x2 :: COPROD k) (y1 :: LIST k)
       (y2 :: COPROD k).
Cocone x1 x2 -> Cocone y1 y2 -> Cocone (x1 ** y1) (x2 ** y2)
** Cocone y1 y2
rs = (y2 ~> 'COPR (a || UN 'COPR y2))
-> Cocone y1 y2 -> Cocone y1 ('COPR (a || UN 'COPR y2))
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
forall (b :: COPROD k) (d :: COPROD k) (a :: LIST k).
(b ~> d) -> Cocone a b -> Cocone a d
rmap ((UN 'COPR y2 ~> (a || UN 'COPR y2))
-> Coprod (~>) ('COPR (UN 'COPR y2)) ('COPR (a || UN 'COPR y2))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @l)) Cocone y1 y2
rs ((Ob y1, Ob y2) => Cocone (L (UN L y1)) ('COPR (a || UN 'COPR y2)))
-> Cocone y1 y2 -> Cocone (L (UN L y1)) ('COPR (a || UN 'COPR y2))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: LIST k) (b :: COPROD k) r.
((Ob a, Ob b) => r) -> Cocone a b -> r
\\ Cocone y1 y2
rs
  Coleg b ~> a
l Cocone (L bs) ('COPR a)
ls ** (Cocone y1 y2
rs :: Cocone rs r) = (b ~> (a || UN 'COPR y2))
-> Cocone (L (bs ++ UN L y1)) ('COPR (a || UN 'COPR y2))
-> Cocone (L (b : (bs ++ UN L y1))) ('COPR (a || UN 'COPR y2))
forall {k} (b :: k) (a :: k) (bs :: [k]).
(b ~> a)
-> Cocone (L bs) ('COPR a) -> Cocone (L (b : bs)) ('COPR a)
Coleg (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @_ @(UN COPR r) (a ~> (a || UN 'COPR y2)) -> (b ~> a) -> b ~> (a || UN 'COPR y2)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b ~> a
l) (Cocone (L bs) ('COPR a)
ls Cocone (L bs) ('COPR a)
-> Cocone y1 y2 -> Cocone (L bs ** y1) ('COPR a ** 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)
forall (x1 :: LIST k) (x2 :: COPROD k) (y1 :: LIST k)
       (y2 :: COPROD k).
Cocone x1 x2 -> Cocone y1 y2 -> Cocone (x1 ** y1) (x2 ** y2)
** Cocone y1 y2
rs) ((Ob b, Ob a) =>
 Cocone (L (b : (bs ++ UN L y1))) ('COPR (a || UN 'COPR y2)))
-> (b ~> a)
-> Cocone (L (b : (bs ++ UN L y1))) ('COPR (a || UN 'COPR y2))
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 ~> a
l ((Ob y1, Ob y2) =>
 Cocone (L (b : (bs ++ UN L y1))) ('COPR (a || UN 'COPR y2)))
-> Cocone y1 y2
-> Cocone (L (b : (bs ++ UN L y1))) ('COPR (a || UN 'COPR y2))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: LIST k) (b :: COPROD k) r.
((Ob a, Ob b) => r) -> Cocone a b -> r
\\ Cocone y1 y2
rs

-- | A sink is a cocone, but with the apex type hidden by an existential.
data Sink (as :: [k]) where
  Cocone :: Cocone (L as) (COPR a) -> Sink as