{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Object.Pushout where

import Proarrow.Category.Opposite (OPPOSITE, Op (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), obj, type (+->), rmap, UN)
import Proarrow.Object (pattern Objs)
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..), HasCoproducts, COPROD (..), Coprod (..))
import Proarrow.Object.Initial (HasZeroObject (..))
import Proarrow.Object.Pullback (Cone (..), Cosink (..), HasPullbacks (..))
import Proarrow.Profunctor.List (LIST (..), List (..))
import Proarrow.Category.Monoidal (MonoidalProfunctor (..))
import Proarrow.Profunctor.Identity (Id(..))

-- | 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} (a :: k). Ob a => Cocone (L '[]) ('COPR a)
Coapex ((Ob ('COPR a), Ob d) => Cocone c d)
-> Coprod Id ('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 Id a b -> r
\\ b ~> d
Coprod Id ('COPR a) d
r
  dimap (Cons a ~> b
l List (~>) (L as1) (L bs1)
ls) r :: b ~> d
r@(Coprod (Id 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} (a :: k) (a :: k) (bs :: [k]).
(a ~> a)
-> Cocone (L bs) ('COPR a) -> Cocone (L (a : 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
  par0 :: Cocone Unit Unit
par0 = Cocone Unit Unit
Cocone (L '[]) ('COPR InitialObject)
forall {k} (a :: k). Ob a => Cocone (L '[]) ('COPR a)
Coapex
  Coapex @l par :: forall (x1 :: LIST k) (x2 :: COPROD k) (y1 :: LIST k)
       (y2 :: COPROD k).
Cocone x1 x2 -> Cocone y1 y2 -> Cocone (x1 ** y1) (x2 ** y2)
`par` 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
rmap (Id (UN 'COPR y2) (a || UN 'COPR y2)
-> Coprod Id ('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 ((UN 'COPR y2 ~> (a || UN 'COPR y2))
-> Id (UN 'COPR y2) (a || UN 'COPR y2)
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (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 `par` (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} (a :: k) (a :: k) (bs :: [k]).
(a ~> a)
-> Cocone (L bs) ('COPR a) -> Cocone (L (a : 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)
`par` 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

-- | Pushouts are an inherently dependently typed concept:
-- The type of the apex object depends on the values of the given arrows.
-- But at runtime we can still calculate the arrows and the type, which we hide behind an existential.
class (HasCoproducts k) => HasPushouts k where
  pushout :: forall (o :: k) a b. o ~> a -> o ~> b -> Sink [a, b]

coequalizer :: forall {k} (a :: k) b. (HasPushouts k) => a ~> b -> a ~> b -> Sink '[b]
coequalizer :: forall {k} (a :: k) (b :: k).
HasPushouts k =>
(a ~> b) -> (a ~> b) -> Sink '[b]
coequalizer f :: a ~> b
f@a ~> b
Objs a ~> b
g = case ((b || a) ~> b) -> ((b || a) ~> b) -> Sink '[b, b]
forall (o :: k) (a :: k) (b :: k).
(o ~> a) -> (o ~> b) -> Sink '[a, b]
forall k (o :: k) (a :: k) (b :: k).
HasPushouts k =>
(o ~> a) -> (o ~> b) -> Sink '[a, b]
pushout (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b Obj b -> (a ~> b) -> (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
||| a ~> b
f) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b Obj b -> (a ~> b) -> (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
||| a ~> b
g) of
  Cocone (Coleg b ~> a
_ Cocone (L bs) ('COPR a)
cocone) -> Cocone (L '[b]) ('COPR a) -> Sink '[b]
forall {k} (as :: [k]) (a :: k). Cocone (L as) ('COPR a) -> Sink as
Cocone Cocone (L bs) ('COPR a)
Cocone (L '[b]) ('COPR a)
cocone

cokernel :: (HasPushouts k, HasZeroObject k) => (a :: k) ~> b -> Sink '[b]
cokernel :: forall k (a :: k) (b :: k).
(HasPushouts k, HasZeroObject k) =>
(a ~> b) -> Sink '[b]
cokernel f :: a ~> b
f@a ~> b
Objs = (a ~> b) -> (a ~> b) -> Sink '[b]
forall {k} (a :: k) (b :: k).
HasPushouts k =>
(a ~> b) -> (a ~> b) -> Sink '[b]
coequalizer a ~> b
forall (a :: k) (b :: k). (Ob a, Ob b) => a ~> b
forall k (a :: k) (b :: k). (HasZeroObject k, Ob a, Ob b) => a ~> b
zero a ~> b
f

instance (HasPullbacks k) => HasPushouts (OPPOSITE k) where
  pushout :: forall (o :: OPPOSITE k) (a :: OPPOSITE k) (b :: OPPOSITE k).
(o ~> a) -> (o ~> b) -> Sink '[a, b]
pushout (Op b1 ~> a1
l) (Op b1 ~> a1
r) = case (b1 ~> a1) -> (b1 ~> a1) -> Cosink '[b1, b1]
forall (o :: k) (a :: k) (b :: k).
(a ~> o) -> (b ~> o) -> Cosink '[a, b]
forall k (o :: k) (a :: k) (b :: k).
HasPullbacks k =>
(a ~> o) -> (b ~> o) -> Cosink '[a, b]
pullback b1 ~> a1
l b1 ~> a1
b1 ~> a1
r of Cone (Leg a1 ~> b
f (Leg a1 ~> b
g Cone ('PR a1) (L bs1)
Apex)) -> Cocone (L '[a, b]) ('COPR ('OP a)) -> Sink '[a, b]
forall {k} (as :: [k]) (a :: k). Cocone (L as) ('COPR a) -> Sink as
Cocone ((a ~> 'OP a)
-> Cocone (L '[b]) ('COPR ('OP a))
-> Cocone (L '[a, b]) ('COPR ('OP a))
forall {k} (a :: k) (a :: k) (bs :: [k]).
(a ~> a)
-> Cocone (L bs) ('COPR a) -> Cocone (L (a : bs)) ('COPR a)
Coleg ((a ~> b1) -> Op (~>) ('OP b1) ('OP a)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op a ~> b1
a1 ~> b
f) ((b ~> 'OP a)
-> Cocone (L '[]) ('COPR ('OP a))
-> Cocone (L '[b]) ('COPR ('OP a))
forall {k} (a :: k) (a :: k) (bs :: [k]).
(a ~> a)
-> Cocone (L bs) ('COPR a) -> Cocone (L (a : bs)) ('COPR a)
Coleg ((a ~> b1) -> Op (~>) ('OP b1) ('OP a)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op a ~> b1
a1 ~> b
g) Cocone (L '[]) ('COPR ('OP a))
forall {k} (a :: k). Ob a => Cocone (L '[]) ('COPR a)
Coapex))

instance (HasPushouts k) => HasPullbacks (OPPOSITE k) where
  pullback :: forall (o :: OPPOSITE k) (a :: OPPOSITE k) (b :: OPPOSITE k).
(a ~> o) -> (b ~> o) -> Cosink '[a, b]
pullback (Op b1 ~> a1
l) (Op b1 ~> a1
r) = case (b1 ~> a1) -> (b1 ~> a1) -> Sink '[a1, a1]
forall (o :: k) (a :: k) (b :: k).
(o ~> a) -> (o ~> b) -> Sink '[a, b]
forall k (o :: k) (a :: k) (b :: k).
HasPushouts k =>
(o ~> a) -> (o ~> b) -> Sink '[a, b]
pushout b1 ~> a1
l b1 ~> a1
b1 ~> a1
r of Cocone (Coleg b ~> a
f (Coleg b ~> a
g Cocone (L bs) ('COPR a)
Coapex)) -> Cone ('PR ('OP a)) (L '[a, b]) -> Cosink '[a, b]
forall {k} (a :: k) (as :: [k]). Cone ('PR a) (L as) -> Cosink as
Cone (('OP a ~> a)
-> Cone ('PR ('OP a)) (L '[b]) -> Cone ('PR ('OP a)) (L '[a, b])
forall {k} (a1 :: k) (b :: k) (bs1 :: [k]).
(a1 ~> b) -> Cone ('PR a1) (L bs1) -> Cone ('PR a1) (L (b : bs1))
Leg ((a1 ~> a) -> Op (~>) ('OP a) ('OP a1)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op a1 ~> a
b ~> a
f) (('OP a ~> b)
-> Cone ('PR ('OP a)) (L '[]) -> Cone ('PR ('OP a)) (L '[b])
forall {k} (a1 :: k) (b :: k) (bs1 :: [k]).
(a1 ~> b) -> Cone ('PR a1) (L bs1) -> Cone ('PR a1) (L (b : bs1))
Leg ((a1 ~> a) -> Op (~>) ('OP a) ('OP a1)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op a1 ~> a
b ~> a
g) Cone ('PR ('OP a)) (L '[])
forall {k} (a1 :: k). Ob a1 => Cone ('PR a1) (L '[])
Apex))