module Proarrow.Limit.Pullback where

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

import Proarrow.Category.Enriched.Thin (Thin)
import Proarrow.Category.Instance.Free (Eq2)
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit (Unit (..))
import Proarrow.Core (CategoryOf (..), Hom, obj, (//))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..), HasProducts)
import Proarrow.Object (pattern Objs)

-- | Pullbacks 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 arrows and the type, which we hide behind an existential.
class (CategoryOf k) => HasPullbacks k where
  pullback :: forall (o :: k) a b r. a ~> o -> b ~> o -> (forall p. p ~> a -> p ~> b -> r) -> r

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

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

-- | In a thin category, arrows don't carry information, so pullbacks are just products.
thinPullback
  :: forall {k} (o :: k) a b r. (Thin k, HasProducts k) => a ~> o -> b ~> o -> (forall p. p ~> a -> p ~> b -> r) -> r
thinPullback :: forall {k} (o :: k) (a :: k) (b :: k) r.
(Thin k, HasProducts k) =>
(a ~> o)
-> (b ~> o) -> (forall (p :: k). (p ~> a) -> (p ~> b) -> r) -> r
thinPullback a ~> o
l b ~> o
r forall (p :: k). (p ~> a) -> (p ~> b) -> r
k = a ~> o
l (a ~> o) -> ((Ob a, Ob o) => r) -> r
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// b ~> o
r (b ~> o) -> ((Ob b, Ob o) => 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.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @a @b ((Ob (a && b) => r) -> r) -> (Ob (a && b) => r) -> r
forall a b. (a -> b) -> a -> b
$ ((a && b) ~> a) -> ((a && b) ~> 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) (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @a @b)

equalizerDefault
  :: forall {k} (a :: k) b r. (HasPullbacks k, HasProducts k) => a ~> b -> a ~> b -> (forall e. e ~> a -> r) -> r
equalizerDefault :: forall {k} (a :: k) (b :: k) r.
(HasPullbacks k, HasProducts k) =>
(a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
equalizerDefault f :: a ~> b
f@a ~> b
Objs a ~> b
g forall (e :: k). (e ~> a) -> r
k = (a ~> (a && b))
-> (a ~> (a && b))
-> (forall (p :: k). (p ~> a) -> (p ~> a) -> 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 (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (a ~> b) -> a ~> (a && b)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> b
f) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (a ~> b) -> a ~> (a && b)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> b
g) \p ~> a
_ -> (p ~> a) -> r
forall (e :: k). (e ~> a) -> r
k

kernelPair :: (HasPullbacks k) => (a :: k) ~> b -> (forall p. p ~> a -> p ~> a -> r) -> r
kernelPair :: forall k (a :: k) (b :: k) r.
HasPullbacks k =>
(a ~> b) -> (forall (p :: k). (p ~> a) -> (p ~> a) -> r) -> r
kernelPair a ~> b
f = (a ~> b)
-> (a ~> b) -> (forall (p :: k). (p ~> a) -> (p ~> a) -> 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 a ~> b
f a ~> b
f

isMono :: (HasPullbacks k, Eq2 (Hom k)) => (a :: k) ~> b -> Bool
isMono :: forall k (a :: k) (b :: k).
(HasPullbacks k, Eq2 (Hom k)) =>
(a ~> b) -> Bool
isMono a ~> b
f = (a ~> b) -> (forall (p :: k). (p ~> a) -> (p ~> a) -> Bool) -> Bool
forall k (a :: k) (b :: k) r.
HasPullbacks k =>
(a ~> b) -> (forall (p :: k). (p ~> a) -> (p ~> a) -> r) -> r
kernelPair a ~> b
f (p ~> a) -> (p ~> a) -> Bool
forall (p :: k). (p ~> a) -> (p ~> a) -> Bool
forall a. Eq a => a -> a -> Bool
(==)