{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Colimit.Pushout where

import Prelude (Bool, ($), (==))

import Proarrow.Category.Enriched.Thin (Thin)
import Proarrow.Category.Instance.Free (Eq2)
import Proarrow.Category.Instance.Opposite (OPPOSITE, Op (..))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit (Unit (..))
import Proarrow.Colimit.BinaryCoproduct (HasBinaryCoproducts (..), HasCoproducts)
import Proarrow.Core (CategoryOf (..), Hom, obj, (//))
import Proarrow.Limit.Pullback (HasPullbacks (..))
import Proarrow.Object (pattern Objs)

-- | 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 (CategoryOf k) => HasPushouts k where
  pushout :: forall (o :: k) a b r. o ~> a -> o ~> b -> (forall p. a ~> p -> b ~> p -> r) -> r

instance HasPushouts () where
  pushout :: forall (o :: ()) (a :: ()) (b :: ()) r.
(o ~> a)
-> (o ~> b) -> (forall (p :: ()). (a ~> p) -> (b ~> p) -> r) -> r
pushout o ~> a
Unit o a
Unit o ~> b
Unit '() b
Unit forall (p :: ()). (a ~> p) -> (b ~> p) -> r
k = (a ~> '()) -> (b ~> '()) -> r
forall (p :: ()). (a ~> p) -> (b ~> p) -> r
k a ~> '()
Unit '() '()
Unit b ~> '()
Unit '() '()
Unit

instance (HasPushouts k1, HasPushouts k2) => HasPushouts (k1, k2) where
  pushout :: forall (o :: (k1, k2)) (a :: (k1, k2)) (b :: (k1, k2)) r.
(o ~> a)
-> (o ~> b)
-> (forall (p :: (k1, k2)). (a ~> p) -> (b ~> p) -> r)
-> r
pushout (a1 ~> b1
l1 :**: a2 ~> b2
l2) (a1 ~> b1
r1 :**: a2 ~> b2
r2) forall (p :: (k1, k2)). (a ~> p) -> (b ~> p) -> r
k = (a1 ~> b1)
-> (a1 ~> b1)
-> (forall (p :: k1). (b1 ~> p) -> (b1 ~> p) -> r)
-> r
forall (o :: k1) (a :: k1) (b :: k1) r.
(o ~> a)
-> (o ~> b) -> (forall (p :: k1). (a ~> p) -> (b ~> p) -> r) -> r
forall k (o :: k) (a :: k) (b :: k) r.
HasPushouts k =>
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
pushout a1 ~> b1
l1 a1 ~> b1
a1 ~> b1
r1 \b1 ~> p
f1 b1 ~> p
g1 -> (a2 ~> b2)
-> (a2 ~> b2)
-> (forall (p :: k2). (b2 ~> p) -> (b2 ~> p) -> r)
-> r
forall (o :: k2) (a :: k2) (b :: k2) r.
(o ~> a)
-> (o ~> b) -> (forall (p :: k2). (a ~> p) -> (b ~> p) -> r) -> r
forall k (o :: k) (a :: k) (b :: k) r.
HasPushouts k =>
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
pushout a2 ~> b2
l2 a2 ~> b2
a2 ~> b2
r2 \b2 ~> p
f2 b2 ~> p
g2 -> (a ~> '(p, p)) -> (b ~> '(p, p)) -> r
forall (p :: (k1, k2)). (a ~> p) -> (b ~> p) -> r
k (b1 ~> p
f1 (b1 ~> p) -> (b2 ~> p) -> (:**:) (~>) (~>) '(b1, b2) '(p, p)
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)
:**: b2 ~> p
f2) (b1 ~> p
g1 (b1 ~> p) -> (b2 ~> p) -> (:**:) (~>) (~>) '(b1, b2) '(p, p)
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)
:**: b2 ~> p
g2)

-- | In a thin category, arrows don't carry information, so pushouts are just coproducts.
thinPushout
  :: forall {k} (o :: k) a b r. (Thin k, HasCoproducts k) => o ~> a -> o ~> b -> (forall p. a ~> p -> b ~> p -> r) -> r
thinPushout :: forall {k} (o :: k) (a :: k) (b :: k) r.
(Thin k, HasCoproducts k) =>
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
thinPushout o ~> a
l o ~> b
r forall (p :: k). (a ~> p) -> (b ~> p) -> r
k = o ~> a
l (o ~> a) -> ((Ob o, Ob a) => r) -> r
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// o ~> b
r (o ~> b) -> ((Ob o, Ob b) => r) -> r
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob 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 ((Ob (a || b) => r) -> r) -> (Ob (a || b) => r) -> r
forall a b. (a -> b) -> a -> b
$ (a ~> (a || b)) -> (b ~> (a || b)) -> r
forall (p :: k). (a ~> p) -> (b ~> p) -> r
k (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @b) (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @b)

coequalizerDefault
  :: forall {k} (a :: k) b r. (HasPushouts k, HasCoproducts k) => a ~> b -> a ~> b -> (forall c. b ~> c -> r) -> r
coequalizerDefault :: forall {k} (a :: k) (b :: k) r.
(HasPushouts k, HasCoproducts k) =>
(a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
coequalizerDefault f :: a ~> b
f@a ~> b
Objs a ~> b
g forall (c :: k). (b ~> c) -> r
k = ((b || a) ~> b)
-> ((b || a) ~> b)
-> (forall (p :: k). (b ~> p) -> (b ~> p) -> r)
-> r
forall (o :: k) (a :: k) (b :: k) r.
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
forall k (o :: k) (a :: k) (b :: k) r.
HasPushouts k =>
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
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) \b ~> p
_ -> (b ~> p) -> r
forall (c :: k). (b ~> c) -> r
k

cokernelPair :: (HasPushouts k) => (a :: k) ~> b -> (forall p. b ~> p -> b ~> p -> r) -> r
cokernelPair :: forall k (a :: k) (b :: k) r.
HasPushouts k =>
(a ~> b) -> (forall (p :: k). (b ~> p) -> (b ~> p) -> r) -> r
cokernelPair a ~> b
f = (a ~> b)
-> (a ~> b) -> (forall (p :: k). (b ~> p) -> (b ~> p) -> r) -> r
forall (o :: k) (a :: k) (b :: k) r.
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
forall k (o :: k) (a :: k) (b :: k) r.
HasPushouts k =>
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
pushout a ~> b
f a ~> b
f

isEpi :: (HasPushouts k, Eq2 (Hom k)) => (a :: k) ~> b -> Bool
isEpi :: forall k (a :: k) (b :: k).
(HasPushouts k, Eq2 (Hom k)) =>
(a ~> b) -> Bool
isEpi a ~> b
f = (a ~> b) -> (forall (p :: k). (b ~> p) -> (b ~> p) -> Bool) -> Bool
forall k (a :: k) (b :: k) r.
HasPushouts k =>
(a ~> b) -> (forall (p :: k). (b ~> p) -> (b ~> p) -> r) -> r
cokernelPair a ~> b
f (b ~> p) -> (b ~> p) -> Bool
forall (p :: k). (b ~> p) -> (b ~> p) -> Bool
forall a. Eq a => a -> a -> Bool
(==)

instance (HasPullbacks k) => HasPushouts (OPPOSITE k) where
  pushout :: forall (o :: OPPOSITE k) (a :: OPPOSITE k) (b :: OPPOSITE k) r.
(o ~> a)
-> (o ~> b)
-> (forall (p :: OPPOSITE k). (a ~> p) -> (b ~> p) -> r)
-> r
pushout (Op b1 ~> a1
l) (Op b1 ~> a1
r) forall (p :: OPPOSITE k). (a ~> p) -> (b ~> p) -> r
k = (b1 ~> a1)
-> (b1 ~> a1)
-> (forall (p :: k). (p ~> b1) -> (p ~> b1) -> r)
-> r
forall (o :: k) (a :: k) (b :: k) r.
(a ~> o)
-> (b ~> o) -> (forall (p :: k). (p ~> a) -> (p ~> b) -> r) -> r
forall k (o :: k) (a :: k) (b :: k) r.
HasPullbacks k =>
(a ~> o)
-> (b ~> o) -> (forall (p :: k). (p ~> a) -> (p ~> b) -> r) -> r
pullback b1 ~> a1
l b1 ~> a1
b1 ~> a1
r \p ~> b1
f p ~> b1
g -> (a ~> 'OP p) -> (b ~> 'OP p) -> r
forall (p :: OPPOSITE k). (a ~> p) -> (b ~> p) -> r
k ((p ~> b1) -> Op (~>) ('OP b1) ('OP p)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op p ~> b1
f) ((p ~> b1) -> Op (~>) ('OP b1) ('OP p)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op p ~> b1
g)

instance (HasPushouts k) => HasPullbacks (OPPOSITE k) where
  pullback :: forall (o :: OPPOSITE k) (a :: OPPOSITE k) (b :: OPPOSITE k) r.
(a ~> o)
-> (b ~> o)
-> (forall (p :: OPPOSITE k). (p ~> a) -> (p ~> b) -> r)
-> r
pullback (Op b1 ~> a1
l) (Op b1 ~> a1
r) forall (p :: OPPOSITE k). (p ~> a) -> (p ~> b) -> r
k = (b1 ~> a1)
-> (b1 ~> a1)
-> (forall (p :: k). (a1 ~> p) -> (a1 ~> p) -> r)
-> r
forall (o :: k) (a :: k) (b :: k) r.
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
forall k (o :: k) (a :: k) (b :: k) r.
HasPushouts k =>
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
pushout b1 ~> a1
l b1 ~> a1
b1 ~> a1
r \a1 ~> p
f a1 ~> p
g -> ('OP p ~> a) -> ('OP p ~> b) -> r
forall (p :: OPPOSITE k). (p ~> a) -> (p ~> b) -> r
k ((a1 ~> p) -> Op (~>) ('OP p) ('OP a1)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op a1 ~> p
f) ((a1 ~> p) -> Op (~>) ('OP p) ('OP a1)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op a1 ~> p
g)