module Proarrow.Limit.Equalizer where

import Proarrow.Category.Enriched.Thin (Thin)
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit (Unit (..))
import Proarrow.Colimit.Initial (HasInitialObject (..), HasZeroObject (..))
import Proarrow.Core (CategoryOf (..), Hom, Promonad (..))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..), HasProducts)
import Proarrow.Object (pattern Objs)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))

-- | Equalizers are an inherently dependently typed concept:
-- The type of the base 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) => HasEqualizers k where
  equalize :: forall (a :: k) b r. a ~> b -> a ~> b -> (forall e. e ~> a -> r) -> r
  default equalize :: forall (a :: k) b r. (HasInitialObject k) => a ~> b -> a ~> b -> (forall e. e ~> a -> r) -> r
  equalize l :: a ~> b
l@a ~> b
Objs a ~> b
r forall (e :: k). (e ~> a) -> r
k = case (a ~> b)
-> (a ~> b)
-> (InitialObject ~> a)
-> (:.:) (~>) (~>) InitialObject a
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) -> (:.:) (~>) (~>) c a
factorEqualizer a ~> b
l a ~> b
r InitialObject ~> a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate of Hom k InitialObject b
_ :.: f :: Hom k b a
f@Hom k b a
Objs -> Hom k b a -> r
forall (e :: k). (e ~> a) -> r
k Hom k b a
f
  factorEqualizer :: forall (a :: k) b c. a ~> b -> a ~> b -> c ~> a -> (Hom k :.: Hom k) c a

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

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

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

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

pullbackDefault
  :: forall {k} (o :: k) a b r
   . (HasEqualizers k, HasProducts k) => a ~> o -> b ~> o -> (forall p. p ~> a -> p ~> b -> r) -> r
pullbackDefault :: forall {k} (o :: k) (a :: k) (b :: k) r.
(HasEqualizers k, HasProducts k) =>
(a ~> o)
-> (b ~> o) -> (forall (p :: k). (p ~> a) -> (p ~> b) -> r) -> r
pullbackDefault f :: a ~> o
f@a ~> o
Objs g :: b ~> o
g@b ~> o
Objs forall (p :: k). (p ~> a) -> (p ~> b) -> r
k = ((a && b) ~> o)
-> ((a && b) ~> o) -> (forall (e :: k). (e ~> (a && b)) -> 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 (a ~> o
f (a ~> o) -> ((a && b) ~> a) -> (a && b) ~> o
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).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @a @b) (b ~> o
g (b ~> o) -> ((a && b) ~> b) -> (a && b) ~> o
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).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @a @b) \e :: e ~> (a && b)
e@e ~> (a && b)
Objs -> (e ~> a) -> (e ~> b) -> r
forall (p :: k). (p ~> a) -> (p ~> b) -> r
k (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @a @b ((a && b) ~> a) -> (e ~> (a && b)) -> e ~> a
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
. e ~> (a && b)
e) (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @a @b ((a && b) ~> b) -> (e ~> (a && b)) -> e ~> 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
. e ~> (a && b)
e)

kernel :: (HasEqualizers k, HasZeroObject k) => (a :: k) ~> b -> (forall e. e ~> a -> r) -> r
kernel :: forall k (a :: k) (b :: k) r.
(HasEqualizers k, HasZeroObject k) =>
(a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
kernel f :: a ~> b
f@a ~> b
Objs = (a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> 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 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