{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | Coequalizers: 'HasCoequalizers' with 'coequalize' in continuation-passing style (the apex type
-- depends on the given arrows, so it is hidden behind an existential) and 'factorCoequalizer' for the
-- universal property.
module Proarrow.Colimit.Coequalizer where

import Proarrow.Category.Enriched.Thin (Thin)
import Proarrow.Category.Instance.Bool (BOOL (..), Booleans (..))
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 (..), Promonad (..))
import Proarrow.Limit.BinaryProduct (PROD, Prod (..))
import Proarrow.Limit.Equalizer (HasEqualizers (..))
import Proarrow.Object (pattern Objs)
import Prelude qualified as P

-- | 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

  -- | @factorCoequalizer q h@ requires @q@ to be epi and @h@ to be constant on @q@'s fibers; @q@ is
  -- typically (though not necessarily) the coequalizer arrow produced by 'coequalize'.
  factorCoequalizer :: forall (c :: k) x c'. x ~> c -> x ~> c' -> c ~> c'

instance HasCoequalizers () where
  coequalize :: forall (a :: ()) (b :: ()) r.
(a ~> b) -> (a ~> b) -> (forall (c :: ()). (b ~> c) -> r) -> r
coequalize a ~> b
Unit a b
Unit a ~> b
Unit '() '()
Unit forall (c :: ()). (b ~> c) -> r
k = (b ~> '()) -> r
forall (c :: ()). (b ~> c) -> r
k b ~> '()
Unit '() '()
Unit
  factorCoequalizer :: forall (c :: ()) (x :: ()) (c' :: ()).
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer x ~> c
Unit x c
Unit x ~> c'
Unit '() c'
Unit = c ~> c'
Unit '() '()
Unit

-- | Dual to the 'Proarrow.Limit.Equalizer.HasEqualizers' instance for 'BOOL'.
instance HasCoequalizers BOOL where
  coequalize :: forall (a :: BOOL) (b :: BOOL) r.
(a ~> b) -> (a ~> b) -> (forall (c :: BOOL). (b ~> c) -> r) -> r
coequalize = (a ~> b) -> (a ~> b) -> (forall (c :: BOOL). (b ~> c) -> r) -> r
forall {k} (a :: k) (b :: k) r.
Thin k =>
(a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
thinCoequalize
  factorCoequalizer :: forall (c :: BOOL) (x :: BOOL) (c' :: BOOL).
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer x ~> c
Booleans x c
Fls x ~> c'
Booleans 'FLS c'
Fls = c ~> c'
Booleans 'FLS 'FLS
Fls
  factorCoequalizer x ~> c
Booleans x c
Fls x ~> c'
Booleans 'FLS c'
F2T = c ~> c'
Booleans 'FLS 'TRU
F2T
  factorCoequalizer x ~> c
Booleans x c
F2T x ~> c'
Booleans 'FLS c'
F2T = c ~> c'
Booleans 'TRU 'TRU
Tru
  factorCoequalizer x ~> c
Booleans x c
Tru x ~> c'
Booleans 'TRU c'
Tru = c ~> c'
Booleans 'TRU 'TRU
Tru
  factorCoequalizer x ~> c
Booleans x c
F2T x ~> c'
Booleans 'FLS c'
Fls = [Char] -> Booleans 'TRU 'FLS
forall a. HasCallStack => [Char] -> a
P.error [Char]
"factorCoequalizer: h must be constant on q's fibers"

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 (c :: (k1, k2)) (x :: (k1, k2)) (c' :: (k1, k2)).
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer (a1 ~> b1
q1 :**: a2 ~> b2
q2) (a1 ~> b1
h1 :**: a2 ~> b2
h2) = (a1 ~> b1) -> (a1 ~> b1) -> b1 ~> b1
forall (c :: k1) (x :: k1) (c' :: k1).
(x ~> c) -> (x ~> c') -> c ~> c'
forall k (c :: k) (x :: k) (c' :: k).
HasCoequalizers k =>
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer a1 ~> b1
q1 a1 ~> b1
a1 ~> b1
h1 (b1 ~> b1) -> (b2 ~> b2) -> (:**:) (~>) (~>) '(b1, b2) '(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)
:**: (a2 ~> b2) -> (a2 ~> b2) -> b2 ~> b2
forall (c :: k2) (x :: k2) (c' :: k2).
(x ~> c) -> (x ~> c') -> c ~> c'
forall k (c :: k) (x :: k) (c' :: k).
HasCoequalizers k =>
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer a2 ~> b2
q2 a2 ~> b2
a2 ~> b2
h2

-- | Coequalizers are unchanged by making the tensor the product.
instance (HasCoequalizers k) => HasCoequalizers (PROD k) where
  coequalize :: forall (a :: PROD k) (b :: PROD k) r.
(a ~> b) -> (a ~> b) -> (forall (c :: PROD k). (b ~> c) -> r) -> r
coequalize (Prod a1 ~> b1
f) (Prod a1 ~> b1
g) forall (c :: PROD k). (b ~> c) -> r
k = (a1 ~> b1) -> (a1 ~> b1) -> (forall (c :: k). (b1 ~> 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 a1 ~> b1
f a1 ~> b1
a1 ~> b1
g \b1 ~> c
c -> (b ~> PR c) -> r
forall (c :: PROD k). (b ~> c) -> r
k ((b1 ~> c) -> Prod (~>) (PR b1) (PR c)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod b1 ~> c
c)
  factorCoequalizer :: forall (c :: PROD k) (x :: PROD k) (c' :: PROD k).
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer (Prod a1 ~> b1
proj) (Prod a1 ~> b1
h) = (b1 ~> b1) -> Prod (~>) (PR b1) (PR b1)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod ((a1 ~> b1) -> (a1 ~> b1) -> b1 ~> b1
forall (c :: k) (x :: k) (c' :: k).
(x ~> c) -> (x ~> c') -> c ~> c'
forall k (c :: k) (x :: k) (c' :: k).
HasCoequalizers k =>
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer a1 ~> b1
proj a1 ~> b1
a1 ~> b1
h)

-- | 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 :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id

-- | Standalone helper (not a class method) usable as the @default@ implementation of
-- 'Proarrow.Colimit.Pushout.pushout' wherever @(HasCoequalizers k, HasCoproducts k)@ happen to hold.
-- Not every 'Proarrow.Colimit.Pushout.HasPushouts' instance needs it or is required to have it.
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 :: CAT 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 :: CAT 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 :: CAT 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 :: CAT 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)

-- | Given a pushout's own legs @p1, p2@ and a compatible cocone @k1, k2@ out of some @q@ (with
-- @k1 . f == k2 . g@ for whichever cospan @p1, p2@ are a pushout of), produces the unique @p ~> q@
-- through which the cocone factors. Standalone helper (not a class method), usable as the
-- @default@ implementation of 'Proarrow.Colimit.Pushout.factorPushout', dual to
-- 'Proarrow.Limit.Equalizer.factorPullbackDefault'.
factorPushoutDefault
  :: forall {k} (a :: k) b p q
   . (HasCoequalizers k, HasCoproducts k)
  => a ~> p -> b ~> p -> a ~> q -> b ~> q -> p ~> q
factorPushoutDefault :: forall {k} (a :: k) (b :: k) (p :: k) (q :: k).
(HasCoequalizers k, HasCoproducts k) =>
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
factorPushoutDefault p1 :: a ~> p
p1@a ~> p
Objs p2 :: b ~> p
p2@b ~> p
Objs a ~> q
k1 b ~> q
k2 = ((a || b) ~> p) -> ((a || b) ~> q) -> p ~> q
forall (c :: k) (x :: k) (c' :: k).
(x ~> c) -> (x ~> c') -> c ~> c'
forall k (c :: k) (x :: k) (c' :: k).
HasCoequalizers k =>
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer (a ~> p
p1 (a ~> p) -> (b ~> p) -> (a || b) ~> p
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
||| b ~> p
p2) (a ~> q
k1 (a ~> q) -> (b ~> q) -> (a || b) ~> q
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
||| b ~> q
k2)

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 :: CAT 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 (c :: OPPOSITE k) (x :: OPPOSITE k) (c' :: OPPOSITE k).
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer (Op b1 ~> a1
x1) (Op b1 ~> a1
x2) = (b1 ~> b1) -> Op (~>) (OP b1) (OP b1)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p (OP a1) (OP b1)
Op ((b1 ~> a1) -> (b1 ~> a1) -> b1 ~> b1
forall (e :: k) (x :: k) (e' :: k).
(e ~> x) -> (e' ~> x) -> e' ~> e
forall k (e :: k) (x :: k) (e' :: k).
HasEqualizers k =>
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer b1 ~> a1
x1 b1 ~> a1
b1 ~> a1
x2)

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 :: CAT 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 (e :: OPPOSITE k) (x :: OPPOSITE k) (e' :: OPPOSITE k).
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer (Op b1 ~> a1
x1) (Op b1 ~> a1
x2) = (a1 ~> a1) -> Op (~>) (OP a1) (OP a1)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p (OP a1) (OP b1)
Op ((b1 ~> a1) -> (b1 ~> a1) -> a1 ~> a1
forall (c :: k) (x :: k) (c' :: k).
(x ~> c) -> (x ~> c') -> c ~> c'
forall k (c :: k) (x :: k) (c' :: k).
HasCoequalizers k =>
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer b1 ~> a1
x1 b1 ~> a1
b1 ~> a1
x2)