{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Colimit.Coequalizer where

import Proarrow.Category.Enriched.Thin (Thin)
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.Colimit.Initial (HasZeroObject (..))
import Proarrow.Core (CategoryOf (..), Hom, Promonad (..))
import Proarrow.Limit.Equalizer (HasEqualizers (..))
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Object (pattern Objs)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))

-- | Coequalizers 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 arrow and the type, which we hide behind an existential.
class (CategoryOf k) => HasCoequalizers k where
  coequalize :: forall (a :: k) b r. a ~> b -> a ~> b -> (forall c. b ~> c -> r) -> r
  default coequalize :: forall (a :: k) b r. (HasTerminalObject k) => a ~> b -> a ~> b -> (forall c. b ~> c -> r) -> r
  coequalize l :: a ~> b
l@a ~> b
Objs a ~> b
r forall (c :: k). (b ~> c) -> r
k = case (a ~> b)
-> (a ~> b)
-> (b ~> TerminalObject)
-> (:.:) (~>) (~>) b TerminalObject
forall (a :: k) (b :: k) (c :: k).
(a ~> b) -> (a ~> b) -> (b ~> c) -> (:.:) (~>) (~>) b c
forall k (a :: k) (b :: k) (c :: k).
HasCoequalizers k =>
(a ~> b) -> (a ~> b) -> (b ~> c) -> (:.:) (~>) (~>) b c
factorCoequalizer a ~> b
l a ~> b
r b ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate of f :: Hom k b b
f@Hom k b b
Objs :.: Hom k b TerminalObject
_ -> Hom k b b -> r
forall (c :: k). (b ~> c) -> r
k Hom k b b
f
  factorCoequalizer :: forall (a :: k) b c. a ~> b -> a ~> b -> b ~> c -> (Hom k :.: Hom k) b c

instance HasCoequalizers () where
  factorCoequalizer :: forall (a :: ()) (b :: ()) (c :: ()).
(a ~> b) -> (a ~> b) -> (b ~> c) -> (:.:) (Hom ()) (Hom ()) b c
factorCoequalizer a ~> b
Unit a b
Unit a ~> b
Unit '() '()
Unit b ~> c
Unit '() c
Unit = Unit b '()
Unit '() '()
Unit Unit b '() -> Unit '() c -> (:.:) Unit Unit b c
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
:.: Unit '() c
Unit '() '()
Unit

instance (HasCoequalizers k1, HasCoequalizers k2) => HasCoequalizers (k1, k2) where
  coequalize :: forall (a :: (k1, k2)) (b :: (k1, k2)) r.
(a ~> b)
-> (a ~> b) -> (forall (c :: (k1, k2)). (b ~> c) -> r) -> r
coequalize (a1 ~> b1
l1 :**: a2 ~> b2
l2) (a1 ~> b1
r1 :**: a2 ~> b2
r2) forall (c :: (k1, k2)). (b ~> c) -> r
k = (a1 ~> b1) -> (a1 ~> b1) -> (forall (c :: k1). (b1 ~> c) -> r) -> r
forall (a :: k1) (b :: k1) r.
(a ~> b) -> (a ~> b) -> (forall (c :: k1). (b ~> c) -> r) -> r
forall k (a :: k) (b :: k) r.
HasCoequalizers k =>
(a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
coequalize a1 ~> b1
l1 a1 ~> b1
a1 ~> b1
r1 \b1 ~> c
f1 -> (a2 ~> b2) -> (a2 ~> b2) -> (forall (c :: k2). (b2 ~> c) -> r) -> r
forall (a :: k2) (b :: k2) r.
(a ~> b) -> (a ~> b) -> (forall (c :: k2). (b ~> c) -> r) -> r
forall k (a :: k) (b :: k) r.
HasCoequalizers k =>
(a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
coequalize a2 ~> b2
l2 a2 ~> b2
a2 ~> b2
r2 \b2 ~> c
f2 -> (b ~> '(c, c)) -> r
forall (c :: (k1, k2)). (b ~> c) -> r
k (b1 ~> c
f1 (b1 ~> c) -> (b2 ~> c) -> (:**:) (~>) (~>) '(b1, b2) '(c, c)
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 ~> c
f2)
  factorCoequalizer :: forall (a :: (k1, k2)) (b :: (k1, k2)) (c :: (k1, k2)).
(a ~> b)
-> (a ~> b) -> (b ~> c) -> (:.:) (Hom (k1, k2)) (Hom (k1, k2)) b c
factorCoequalizer (a1 ~> b1
l1 :**: a2 ~> b2
l2) (a1 ~> b1
r1 :**: a2 ~> b2
r2) (a1 ~> b1
f1 :**: a2 ~> b2
f2) = case ((a1 ~> b1) -> (a1 ~> b1) -> (b1 ~> b1) -> (:.:) (~>) (~>) b1 b1
forall (a :: k1) (b :: k1) (c :: k1).
(a ~> b) -> (a ~> b) -> (b ~> c) -> (:.:) (~>) (~>) b c
forall k (a :: k) (b :: k) (c :: k).
HasCoequalizers k =>
(a ~> b) -> (a ~> b) -> (b ~> c) -> (:.:) (~>) (~>) b c
factorCoequalizer a1 ~> b1
l1 a1 ~> b1
a1 ~> b1
r1 b1 ~> b1
a1 ~> b1
f1, (a2 ~> b2) -> (a2 ~> b2) -> (b2 ~> b2) -> (:.:) (~>) (~>) b2 b2
forall (a :: k2) (b :: k2) (c :: k2).
(a ~> b) -> (a ~> b) -> (b ~> c) -> (:.:) (~>) (~>) b c
forall k (a :: k) (b :: k) (c :: k).
HasCoequalizers k =>
(a ~> b) -> (a ~> b) -> (b ~> c) -> (:.:) (~>) (~>) b c
factorCoequalizer a2 ~> b2
l2 a2 ~> b2
a2 ~> b2
r2 b2 ~> b2
a2 ~> b2
f2) of
    (b1 ~> b
l :.: b ~> b1
r, b2 ~> b
f :.: b ~> b2
g) -> (b1 ~> b
l (b1 ~> b) -> (b2 ~> b) -> (:**:) (~>) (~>) '(b1, b2) '(b, 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)
:**: b2 ~> b
f) (:**:) (~>) (~>) b '(b, b)
-> (:**:) (~>) (~>) '(b, b) c
-> (:.:) ((~>) :**: (~>)) ((~>) :**: (~>)) b c
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
:.: (b ~> b1
r (b ~> b1) -> (b ~> b2) -> (:**:) (~>) (~>) '(b, b) '(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)
:**: b ~> b2
g)

-- | In a thin category, arrows don't carry information, so coequalizers are just coproducts.
thinCoequalize :: forall {k} (a :: k) b r. (Thin k) => a ~> b -> a ~> b -> (forall c. b ~> c -> r) -> r
thinCoequalize :: forall {k} (a :: k) (b :: k) r.
Thin k =>
(a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
thinCoequalize a ~> b
Objs a ~> b
_ forall (c :: k). (b ~> c) -> r
k = (b ~> b) -> r
forall (c :: k). (b ~> c) -> r
k b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

thinFactorCoequalizer :: forall {k} (a :: k) b c. (Thin k) => a ~> b -> a ~> b -> b ~> c -> (Hom k :.: Hom k) b c
thinFactorCoequalizer :: forall {k} (a :: k) (b :: k) (c :: k).
Thin k =>
(a ~> b) -> (a ~> b) -> (b ~> c) -> (:.:) (Hom k) (Hom k) b c
thinFactorCoequalizer a ~> b
_ a ~> b
_ f :: b ~> c
f@b ~> c
Objs = b ~> c
f (b ~> c) -> (c ~> c) -> (:.:) (~>) (~>) b c
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
:.: c ~> c
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

pushoutDefault
  :: forall {k} (o :: k) a b r
   . (HasCoequalizers k, HasCoproducts k) => o ~> a -> o ~> b -> (forall p. a ~> p -> b ~> p -> r) -> r
pushoutDefault :: forall {k} (o :: k) (a :: k) (b :: k) r.
(HasCoequalizers k, HasCoproducts k) =>
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
pushoutDefault f :: o ~> a
f@o ~> a
Objs g :: o ~> b
g@o ~> b
Objs forall (p :: k). (a ~> p) -> (b ~> p) -> r
k = (o ~> (a || b))
-> (o ~> (a || b)) -> (forall (c :: k). ((a || b) ~> c) -> r) -> r
forall (a :: k) (b :: k) r.
(a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
forall k (a :: k) (b :: k) r.
HasCoequalizers k =>
(a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
coequalize (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @b (a ~> (a || b)) -> (o ~> a) -> o ~> (a || b)
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
. o ~> a
f) (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @b (b ~> (a || b)) -> (o ~> b) -> o ~> (a || b)
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
. o ~> b
g) \c :: (a || b) ~> c
c@(a || b) ~> c
Objs ->
  (a ~> c) -> (b ~> c) -> r
forall (p :: k). (a ~> p) -> (b ~> p) -> r
k ((a || b) ~> c
c ((a || b) ~> c) -> (a ~> (a || b)) -> a ~> c
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
. forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @b) ((a || b) ~> c
c ((a || b) ~> c) -> (b ~> (a || b)) -> b ~> c
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
. forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @b)

cokernel :: (HasCoequalizers k, HasZeroObject k) => (a :: k) ~> b -> (forall c. b ~> c -> r) -> r
cokernel :: forall k (a :: k) (b :: k) r.
(HasCoequalizers k, HasZeroObject k) =>
(a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
cokernel f :: a ~> b
f@a ~> b
Objs = (a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
forall (a :: k) (b :: k) r.
(a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
forall k (a :: k) (b :: k) r.
HasCoequalizers k =>
(a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
coequalize 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 (HasEqualizers k) => HasCoequalizers (OPPOSITE k) where
  coequalize :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) r.
(a ~> b)
-> (a ~> b) -> (forall (c :: OPPOSITE k). (b ~> c) -> r) -> r
coequalize (Op b1 ~> a1
l) (Op b1 ~> a1
r) forall (c :: OPPOSITE k). (b ~> c) -> r
k = (b1 ~> a1) -> (b1 ~> a1) -> (forall (e :: k). (e ~> b1) -> r) -> r
forall (a :: k) (b :: k) r.
(a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
forall k (a :: k) (b :: k) r.
HasEqualizers k =>
(a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
equalize b1 ~> a1
l b1 ~> a1
b1 ~> a1
r ((b ~> 'OP e) -> r
Op (~>) ('OP b1) ('OP e) -> r
forall (c :: OPPOSITE k). (b ~> c) -> r
k (Op (~>) ('OP b1) ('OP e) -> r)
-> ((e ~> b1) -> Op (~>) ('OP b1) ('OP e)) -> (e ~> b1) -> r
forall b c a. (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
. (e ~> b1) -> Op (~>) ('OP b1) ('OP e)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op)
  factorCoequalizer :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (c :: OPPOSITE k).
(a ~> b)
-> (a ~> b)
-> (b ~> c)
-> (:.:) (Hom (OPPOSITE k)) (Hom (OPPOSITE k)) b c
factorCoequalizer (Op b1 ~> a1
l) (Op b1 ~> a1
r) (Op b1 ~> a1
f) = case (b1 ~> a1) -> (b1 ~> a1) -> (b1 ~> b1) -> (:.:) (~>) (~>) b1 b1
forall (a :: k) (b :: k) (c :: k).
(a ~> b) -> (a ~> b) -> (c ~> a) -> (:.:) (~>) (~>) c a
forall k (a :: k) (b :: k) (c :: k).
HasEqualizers k =>
(a ~> b) -> (a ~> b) -> (c ~> a) -> (:.:) (Hom k) (Hom k) c a
factorEqualizer b1 ~> a1
l b1 ~> a1
b1 ~> a1
r b1 ~> b1
b1 ~> a1
f of
    Hom k b1 b
l' :.: Hom k b b1
r' -> Hom k b b1 -> Op (~>) ('OP b1) ('OP b)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op Hom k b b1
r' Op (~>) b ('OP b)
-> Op (~>) ('OP b) c -> (:.:) (Op (~>)) (Op (~>)) b c
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
:.: Hom k b1 b -> Op (~>) ('OP b) ('OP b1)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op Hom k b1 b
l'

instance (HasCoequalizers k) => HasEqualizers (OPPOSITE k) where
  equalize :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) r.
(a ~> b)
-> (a ~> b) -> (forall (e :: OPPOSITE k). (e ~> a) -> r) -> r
equalize (Op b1 ~> a1
l) (Op b1 ~> a1
r) forall (e :: OPPOSITE k). (e ~> a) -> r
k = (b1 ~> a1) -> (b1 ~> a1) -> (forall (c :: k). (a1 ~> c) -> r) -> r
forall (a :: k) (b :: k) r.
(a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
forall k (a :: k) (b :: k) r.
HasCoequalizers k =>
(a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
coequalize b1 ~> a1
l b1 ~> a1
b1 ~> a1
r (('OP c ~> a) -> r
Op (~>) ('OP c) ('OP a1) -> r
forall (e :: OPPOSITE k). (e ~> a) -> r
k (Op (~>) ('OP c) ('OP a1) -> r)
-> ((a1 ~> c) -> Op (~>) ('OP c) ('OP a1)) -> (a1 ~> c) -> r
forall b c a. (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
. (a1 ~> c) -> Op (~>) ('OP c) ('OP a1)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op)
  factorEqualizer :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (c :: OPPOSITE k).
(a ~> b)
-> (a ~> b)
-> (c ~> a)
-> (:.:) (Hom (OPPOSITE k)) (Hom (OPPOSITE k)) c a
factorEqualizer (Op b1 ~> a1
l) (Op b1 ~> a1
r) (Op b1 ~> a1
f) = case (b1 ~> a1) -> (b1 ~> a1) -> (a1 ~> a1) -> (:.:) (~>) (~>) a1 a1
forall (a :: k) (b :: k) (c :: k).
(a ~> b) -> (a ~> b) -> (b ~> c) -> (:.:) (~>) (~>) b c
forall k (a :: k) (b :: k) (c :: k).
HasCoequalizers k =>
(a ~> b) -> (a ~> b) -> (b ~> c) -> (:.:) (~>) (~>) b c
factorCoequalizer b1 ~> a1
l b1 ~> a1
b1 ~> a1
r a1 ~> a1
b1 ~> a1
f of
    Hom k a1 b
l' :.: Hom k b a1
r' -> Hom k b a1 -> Op (~>) ('OP a1) ('OP b)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op Hom k b a1
r' Op (~>) c ('OP b)
-> Op (~>) ('OP b) a -> (:.:) (Op (~>)) (Op (~>)) c a
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
:.: Hom k a1 b -> Op (~>) ('OP b) ('OP a1)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op Hom k a1 b
l'