{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Limit where

import Data.Function (($))
import Data.Kind (Constraint, Type)

import Proarrow.Category.Instance.Coproduct (COPRODUCT, IsLR (..), L, R)
import Proarrow.Category.Instance.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Unit (Unit (..))
import Proarrow.Category.Instance.Zero (VOID)
import Proarrow.Core (CAT, CategoryOf (..), Kind, Profunctor (..), Promonad (..), rmap, (//), (:~>), type (+->))
import Proarrow.Functor (Functor (..), FunctorForRep (..))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..), fst, snd)
import Proarrow.Limit.Power (Powered (..))
import Proarrow.Limit.Terminal (HasTerminalObject (..), terminate)
import Proarrow.Profunctor.Corepresentable (Corep (..), corepUniv)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Constant (Constant)
import Proarrow.Profunctor.Instance.HaskValue (HaskValue (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Instance.Star (Star, pattern Star)
import Proarrow.Profunctor.Instance.Terminal (TerminalProfunctor (..))
import Proarrow.Profunctor.Representable (Rep (..), Representable (..), repUniv, withObRep)

class (Representable (Limit j d)) => IsRepresentableLimit j d
instance (Representable (Limit j d)) => IsRepresentableLimit j d

-- | profunctor-weighted limits
type HasLimits :: forall {a} {i}. i +-> a -> Kind -> Constraint
class (Profunctor j, forall (d :: i +-> k). (Representable d) => IsRepresentableLimit j d) => HasLimits (j :: i +-> a) k where
  type Limit (j :: i +-> a) (d :: i +-> k) :: a +-> k
  limit :: (Representable (d :: i +-> k)) => Limit j d :.: j :~> d
  limitUniv :: (Representable (d :: i +-> k), Profunctor p) => p :.: j :~> d -> p :~> Limit j d

mapLimit
  :: forall {i} j k p q. (HasLimits j k, Representable p, Representable q) => (p :: i +-> k) ~> q -> Limit j p ~> Limit j q
mapLimit :: forall {a} {i} (j :: i +-> a) k (p :: i +-> k) (q :: i +-> k).
(HasLimits j k, Representable p, Representable q) =>
(p ~> q) -> Limit j p ~> Limit j q
mapLimit (Prof p :~> q
n) = (Limit j p :~> Limit j q) -> Prof (Limit j p) (Limit j q)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof (forall {a} {i} (j :: i +-> a) k (d :: i +-> k) (p :: a +-> k).
(HasLimits j k, Representable d, Profunctor p) =>
((p :.: j) :~> d) -> p :~> Limit j d
forall (j :: i +-> a) k (d :: i +-> k) (p :: a +-> k).
(HasLimits j k, Representable d, Profunctor p) =>
((p :.: j) :~> d) -> p :~> Limit j d
limitUniv @j (p a b -> q a b
p :~> q
n (p a b -> q a b)
-> ((:.:) (Limit j p) j a b -> p a b)
-> (:.:) (Limit j p) j a b
-> q a b
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
. forall {a} {i} (j :: i +-> a) k (d :: i +-> k).
(HasLimits j k, Representable d) =>
(Limit j d :.: j) :~> d
forall (j :: i +-> a) k (d :: i +-> k).
(HasLimits j k, Representable d) =>
(Limit j d :.: j) :~> d
limit @j))

type Unweighted = TerminalProfunctor

instance (HasTerminalObject k) => HasLimits (Unweighted :: VOID +-> ()) k where
  type Limit Unweighted d = Rep (Constant TerminalObject)
  limit :: forall (d :: VOID +-> k).
Representable d =>
(Limit Unweighted d :.: Unweighted) :~> d
limit (Limit Unweighted d a b
_ :.: Unweighted b b
t) = case Unweighted b b
t of {}
  limitUniv :: forall (d :: VOID +-> k) (p :: () +-> k).
(Representable d, Profunctor p) =>
((p :.: Unweighted) :~> d) -> p :~> Limit Unweighted d
limitUniv (p :.: Unweighted) :~> d
_ p a b
p = p a b
p p a b
-> ((Ob a, Ob b) => Rep (Constant TerminalObject) a b)
-> Rep (Constant TerminalObject) a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (a ~> (Constant TerminalObject @ b))
-> Rep (Constant TerminalObject) a b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep a ~> (Constant TerminalObject @ b)
a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate

type O1 = L '()
type O2 = R '()
type At1 d = d % O1
type At2 d = d % O2

data family ProductLimit :: COPRODUCT () () +-> k -> () +-> k
instance (HasBinaryProducts k, Representable d) => FunctorForRep (ProductLimit d :: () +-> k) where
  type ProductLimit d @ '() = At1 d && At2 d
  fmap :: forall (a :: ()) (b :: ()).
(a ~> b) -> (ProductLimit d @ a) ~> (ProductLimit d @ b)
fmap a ~> b
Unit a b
Unit = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: COPRODUCT () () +-> k) (a :: COPRODUCT () ()) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @d @O1 ((Ob (d % O1) => (ProductLimit d @ a) ~> (ProductLimit d @ b))
 -> (ProductLimit d @ a) ~> (ProductLimit d @ b))
-> (Ob (d % O1) => (ProductLimit d @ a) ~> (ProductLimit d @ b))
-> (ProductLimit d @ a) ~> (ProductLimit d @ b)
forall a b. (a -> b) -> a -> b
$ forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: COPRODUCT () () +-> k) (a :: COPRODUCT () ()) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @d @O2 ((Ob (d % O2) => (ProductLimit d @ a) ~> (ProductLimit d @ b))
 -> (ProductLimit d @ a) ~> (ProductLimit d @ b))
-> (Ob (d % O2) => (ProductLimit d @ a) ~> (ProductLimit d @ b))
-> (ProductLimit d @ a) ~> (ProductLimit d @ b)
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @(At1 d) @(At2 d) ((d % O1) && (d % O2)) ~> ((d % O1) && (d % O2))
Ob ((d % O1) && (d % O2)) =>
((d % O1) && (d % O2)) ~> ((d % O1) && (d % O2))
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

instance (HasBinaryProducts k) => HasLimits (Unweighted :: COPRODUCT () () +-> ()) k where
  type Limit Unweighted d = Rep (ProductLimit d)
  limit :: forall (d :: COPRODUCT () () +-> k).
Representable d =>
(Limit Unweighted d :.: Unweighted) :~> d
limit @d (Rep a ~> (ProductLimit d @ b)
f :.: TerminalProfunctor @_ @o) =
    forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: COPRODUCT () () +-> k) (a :: COPRODUCT () ()) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @d @O1 ((Ob (d % O1) => d a b) -> d a b)
-> (Ob (d % O1) => d a b) -> d a b
forall a b. (a -> b) -> a -> b
$
      forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: COPRODUCT () () +-> k) (a :: COPRODUCT () ()) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @d @O2 ((Ob (d % O2) => d a b) -> d a b)
-> (Ob (d % O2) => d a b) -> d a b
forall a b. (a -> b) -> a -> b
$
        forall {j} {k} (a :: COPRODUCT j k) r.
IsLR a =>
(forall (b :: j). (a ~ L b, Ob b) => r)
-> (forall (b :: k). (a ~ R b, Ob b) => r) -> r
forall (a :: COPRODUCT () ()) r.
IsLR a =>
(forall (b :: ()). (a ~ L b, Ob b) => r)
-> (forall (b :: ()). (a ~ R b, Ob b) => r) -> r
lrCase @o
          ((a ~> (d % b)) -> d a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (b :: COPRODUCT () ()) (a :: k).
Ob b =>
(a ~> (d % b)) -> d a b
tabulate (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @(At1 d) @(At2 d) (((d % O1) && (d % O2)) ~> (d % O1))
-> (a ~> ((d % O1) && (d % O2))) -> a ~> (d % O1)
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
. a ~> (ProductLimit d @ b)
a ~> ((d % O1) && (d % O2))
f))
          ((a ~> (d % b)) -> d a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (b :: COPRODUCT () ()) (a :: k).
Ob b =>
(a ~> (d % b)) -> d a b
tabulate (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @(At1 d) @(At2 d) (((d % O1) && (d % O2)) ~> (d % O2))
-> (a ~> ((d % O1) && (d % O2))) -> a ~> (d % O2)
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
. a ~> (ProductLimit d @ b)
a ~> ((d % O1) && (d % O2))
f))
  limitUniv :: forall (d :: COPRODUCT () () +-> k) (p :: () +-> k).
(Representable d, Profunctor p) =>
((p :.: Unweighted) :~> d) -> p :~> Limit Unweighted d
limitUniv (p :.: Unweighted) :~> d
n p a b
p = p a b
p p a b
-> ((Ob a, Ob b) => Rep (ProductLimit d) a b)
-> Rep (ProductLimit d) a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (a ~> (ProductLimit d @ b)) -> Rep (ProductLimit d) a b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (d a O1 -> a ~> (d % O1)
forall (a :: k) (b :: COPRODUCT () ()). d a b -> a ~> (d % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index ((:.:) p Unweighted a O1 -> d a O1
(p :.: Unweighted) :~> d
n (p a b
p p a b -> Unweighted b O1 -> (:.:) p Unweighted a O1
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
:.: forall {j} {k} (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
forall (a :: ()) (b :: COPRODUCT () ()).
(CategoryOf (), CategoryOf (COPRODUCT () ()), Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor @'() @O1)) (a ~> (d % O1)) -> (a ~> (d % O2)) -> a ~> ((d % O1) && (d % O2))
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)
&&& d a O2 -> a ~> (d % O2)
forall (a :: k) (b :: COPRODUCT () ()). d a b -> a ~> (d % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index ((:.:) p Unweighted a O2 -> d a O2
(p :.: Unweighted) :~> d
n (p a b
p p a b -> Unweighted b O2 -> (:.:) p Unweighted a O2
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
:.: forall {j} {k} (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
forall (a :: ()) (b :: COPRODUCT () ()).
(CategoryOf (), CategoryOf (COPRODUCT () ()), Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor @'() @O2)))

data family PowerLimit :: v -> () +-> k -> () +-> k
instance (Representable d, Powered v k, Ob n) => FunctorForRep (PowerLimit (n :: v) d :: () +-> k) where
  type PowerLimit n d @ '() = (d % '()) ^ n
  fmap :: forall (a :: ()) (b :: ()).
(a ~> b) -> (PowerLimit n d @ a) ~> (PowerLimit n d @ b)
fmap a ~> b
Unit a b
Unit = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: () +-> k) (a :: ()) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @d @'() ((Ob (d % '()) => (PowerLimit n d @ a) ~> (PowerLimit n d @ b))
 -> (PowerLimit n d @ a) ~> (PowerLimit n d @ b))
-> (Ob (d % '()) => (PowerLimit n d @ a) ~> (PowerLimit n d @ b))
-> (PowerLimit n d @ a) ~> (PowerLimit n d @ b)
forall a b. (a -> b) -> a -> b
$ forall v k (a :: k) (n :: v) r.
(Powered v k, Ob a, Ob n) =>
(Ob (a ^ n) => r) -> r
withObPower @v @k @(d % '()) @n ((d % '()) ^ n) ~> ((d % '()) ^ n)
Ob ((d % '()) ^ n) => ((d % '()) ^ n) ~> ((d % '()) ^ n)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
instance (Powered Type k) => HasLimits (HaskValue n :: () +-> ()) k where
  type Limit (HaskValue n) d = Rep (PowerLimit n d)
  limit :: forall (d :: () +-> k).
Representable d =>
(Limit (HaskValue n) d :.: HaskValue n) :~> d
limit @d (Rep a ~> (PowerLimit n d @ b)
f :.: HaskValue n
n) = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: () +-> k) (a :: ()) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @d @'() ((Ob (d % '()) => d a b) -> d a b)
-> (Ob (d % '()) => d a b) -> d a b
forall a b. (a -> b) -> a -> b
$ (a ~> (d % b)) -> d a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (b :: ()) (a :: k). Ob b => (a ~> (d % b)) -> d a b
tabulate ((a ~> ((d % '()) ^ n)) -> n ~> ProObj Type (~>) a (d % '())
forall (b :: k) n (a :: k).
(Ob b, Ob n) =>
(a ~> (b ^ n)) -> n ~> HomObj Type a b
forall v k (b :: k) (n :: v) (a :: k).
(Powered v k, Ob b, Ob n) =>
(a ~> (b ^ n)) -> n ~> HomObj v a b
unpower a ~> (PowerLimit n d @ b)
a ~> ((d % '()) ^ n)
f n
n)
  limitUniv :: forall (d :: () +-> k) (p :: () +-> k).
(Representable d, Profunctor p) =>
((p :.: HaskValue n) :~> d) -> p :~> Limit (HaskValue n) d
limitUniv @d (p :.: HaskValue n) :~> d
m p a b
p = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: () +-> k) (a :: ()) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @d @'() ((Ob (d % '()) => Limit (HaskValue n) d a b)
 -> Limit (HaskValue n) d a b)
-> (Ob (d % '()) => Limit (HaskValue n) d a b)
-> Limit (HaskValue n) d a b
forall a b. (a -> b) -> a -> b
$ (a ~> (PowerLimit n d @ b)) -> Rep (PowerLimit n d) a b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep ((n ~> HomObj Type a (d % '())) -> a ~> ((d % '()) ^ n)
forall (a :: k) (b :: k) n.
(Ob a, Ob b) =>
(n ~> HomObj Type a b) -> a ~> (b ^ n)
forall v k (a :: k) (b :: k) (n :: v).
(Powered v k, Ob a, Ob b) =>
(n ~> HomObj v a b) -> a ~> (b ^ n)
power \n
n -> d a '() -> a ~> (d % '())
forall (a :: k) (b :: ()). d a b -> a ~> (d % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index ((:.:) p (HaskValue n) a '() -> d a '()
(p :.: HaskValue n) :~> d
m (p a b
p p a b -> HaskValue n b '() -> (:.:) p (HaskValue n) 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
:.: n -> HaskValue n b '()
forall {k} {j} (a :: k) (b :: j) c.
(Ob a, Ob b) =>
c -> HaskValue c a b
HaskValue n
n))) ((Ob a, Ob b) => Rep (PowerLimit n d) a b)
-> p a b -> Rep (PowerLimit n d) a b
forall (a :: k) (b :: ()) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

newtype End d = End {forall {k} (d :: (OPPOSITE k, k) +-> Type).
End d -> forall (a :: k) (b :: k). (a ~> b) -> d % '( 'OP a, b)
unEnd :: forall a b. a ~> b -> d % '(OP a, b)}

data family EndLimit :: (OPPOSITE k, k) +-> Type -> () +-> Type
instance (Representable d) => FunctorForRep (EndLimit (d :: (OPPOSITE k, k) +-> Type)) where
  type EndLimit d @ '() = End d
  fmap :: forall (a :: ()) (b :: ()).
(a ~> b) -> (EndLimit d @ a) ~> (EndLimit d @ b)
fmap a ~> b
Unit a b
Unit = (EndLimit d @ a) ~> (EndLimit d @ b)
End d -> End d
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

type Hom :: (OPPOSITE k, k) +-> ()
data Hom a b where
  Hom :: a ~> b -> Hom '() '(OP a, b)
instance (CategoryOf k) => Profunctor (Hom :: (OPPOSITE k, k) +-> ()) where
  dimap :: forall (c :: ()) (a :: ()) (b :: (OPPOSITE k, k))
       (d :: (OPPOSITE k, k)).
(c ~> a) -> (b ~> d) -> Hom a b -> Hom c d
dimap c ~> a
Unit c a
Unit (Op b1 ~> a1
l :**: a2 ~> b2
r) (Hom a ~> b
f) = (b1 ~> b2) -> Hom '() '( 'OP b1, b2)
forall {k} (a :: k) (b :: k). (a ~> b) -> Hom '() '( 'OP a, b)
Hom (a2 ~> b2
r (a2 ~> b2) -> (b1 ~> a2) -> b1 ~> b2
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
. a1 ~> a2
a ~> b
f (a1 ~> a2) -> (b1 ~> a1) -> b1 ~> a2
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
. b1 ~> a1
l) ((Ob b1, Ob a1) => Hom c d) -> (b1 ~> a1) -> Hom c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b1 ~> a1
l ((Ob a2, Ob b2) => Hom c d) -> (a2 ~> b2) -> Hom c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a2 ~> b2
r
  (Ob a, Ob b) => r
r \\ :: forall (a :: ()) (b :: (OPPOSITE k, k)) r.
((Ob a, Ob b) => r) -> Hom a b -> r
\\ Hom a ~> b
f = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f

instance (CategoryOf k) => HasLimits (Hom :: (OPPOSITE k, k) +-> ()) Type where
  type Limit Hom d = Rep (EndLimit d)
  limit :: forall (d :: (OPPOSITE k, k) +-> Type).
Representable d =>
(Limit Hom d :.: Hom) :~> d
limit (Rep a ~> (EndLimit d @ b)
f :.: Hom a ~> b
k) = a ~> b
k (a ~> b) -> ((Ob a, Ob b) => d a b) -> d a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (a ~> (d % b)) -> d a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (b :: (OPPOSITE k, k)) a. Ob b => (a ~> (d % b)) -> d a b
tabulate (\a
a -> End d -> forall (a :: k) (b :: k). (a ~> b) -> d % '( 'OP a, b)
forall {k} (d :: (OPPOSITE k, k) +-> Type).
End d -> forall (a :: k) (b :: k). (a ~> b) -> d % '( 'OP a, b)
unEnd (a ~> (EndLimit d @ b)
a -> End d
f a
a) a ~> b
k)
  limitUniv :: forall (d :: (OPPOSITE k, k) +-> Type) (p :: () +-> Type).
(Representable d, Profunctor p) =>
((p :.: Hom) :~> d) -> p :~> Limit Hom d
limitUniv (p :.: Hom) :~> d
n p a b
p = p a b
p p a b
-> ((Ob a, Ob b) => Rep (EndLimit d) a b) -> Rep (EndLimit d) a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (a ~> (EndLimit d @ b)) -> Rep (EndLimit d) a b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep \a
a -> (forall (a :: k) (b :: k). (a ~> b) -> d % '( 'OP a, b)) -> End d
forall {k} (d :: (OPPOSITE k, k) +-> Type).
(forall (a :: k) (b :: k). (a ~> b) -> d % '( 'OP a, b)) -> End d
End \a ~> b
x -> d a '( 'OP a, b) -> a ~> (d % '( 'OP a, b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall a (b :: (OPPOSITE k, k)). d a b -> a ~> (d % b)
index ((:.:) p Hom a '( 'OP a, b) -> d a '( 'OP a, b)
(p :.: Hom) :~> d
n (p a b
p p a b -> Hom b '( 'OP a, b) -> (:.:) p Hom a '( 'OP a, b)
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
:.: (a ~> b) -> Hom '() '( 'OP a, b)
forall {k} (a :: k) (b :: k). (a ~> b) -> Hom '() '( 'OP a, b)
Hom a ~> b
x)) a
a

instance (CategoryOf j) => HasLimits (Id :: CAT j) k where
  type Limit Id d = d
  limit :: forall (d :: j +-> k). Representable d => (Limit Id d :.: Id) :~> d
limit (Limit Id d a b
d :.: Id b ~> b
f) = (b ~> b) -> d a b -> d a b
forall (b :: j) (d :: j) (a :: k). (b ~> d) -> d a b -> d a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> b
f d a b
Limit Id d a b
d
  limitUniv :: forall (d :: j +-> k) (p :: j +-> k).
(Representable d, Profunctor p) =>
((p :.: Id) :~> d) -> p :~> Limit Id d
limitUniv (p :.: Id) :~> d
n p a b
p = (:.:) p Id a b -> d a b
(p :.: Id) :~> d
n (p a b
p p a b -> Id b b -> (:.:) p Id a b
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 ~> b) -> Id b b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id b ~> b
forall (a :: j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id) ((Ob a, Ob b) => d a b) -> p a b -> d a b
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

instance (Representable j1, HasLimits j1 k, HasLimits j2 k) => HasLimits (j1 :.: j2) k where
  type Limit (j1 :.: j2) d = Limit j1 (Limit j2 d)
  limit :: forall (d :: i +-> k).
Representable d =>
(Limit (j1 :.: j2) d :.: (j1 :.: j2)) :~> d
limit @d (Limit (j1 :.: j2) d a b
l :.: (j1 b b
j1 :.: j2 b b
j2)) = forall {a} {i} (j :: i +-> a) k (d :: i +-> k).
(HasLimits j k, Representable d) =>
(Limit j d :.: j) :~> d
forall (j :: i +-> j) k (d :: i +-> k).
(HasLimits j k, Representable d) =>
(Limit j d :.: j) :~> d
limit @j2 @k @d (forall {a} {i} (j :: i +-> a) k (d :: i +-> k).
(HasLimits j k, Representable d) =>
(Limit j d :.: j) :~> d
forall (j :: j +-> a) k (d :: j +-> k).
(HasLimits j k, Representable d) =>
(Limit j d :.: j) :~> d
limit @j1 @k @(Limit j2 d) (Limit j1 (Limit j2 d) a b
Limit (j1 :.: j2) d a b
l Limit j1 (Limit j2 d) a b
-> j1 b b -> (:.:) (Limit j1 (Limit j2 d)) j1 a b
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
:.: j1 b b
j1) Limit j2 d a b -> j2 b b -> (:.:) (Limit j2 d) j2 a b
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
:.: j2 b b
j2)
  limitUniv :: forall (d :: i +-> k) (p :: a +-> k).
(Representable d, Profunctor p) =>
((p :.: (j1 :.: j2)) :~> d) -> p :~> Limit (j1 :.: j2) d
limitUniv @d (p :.: (j1 :.: j2)) :~> d
n = forall {a} {i} (j :: i +-> a) k (d :: i +-> k) (p :: a +-> k).
(HasLimits j k, Representable d, Profunctor p) =>
((p :.: j) :~> d) -> p :~> Limit j d
forall (j :: j +-> a) k (d :: j +-> k) (p :: a +-> k).
(HasLimits j k, Representable d, Profunctor p) =>
((p :.: j) :~> d) -> p :~> Limit j d
limitUniv @j1 @k @(Limit j2 d) (forall {a} {i} (j :: i +-> a) k (d :: i +-> k) (p :: a +-> k).
(HasLimits j k, Representable d, Profunctor p) =>
((p :.: j) :~> d) -> p :~> Limit j d
forall (j :: i +-> j) k (d :: i +-> k) (p :: j +-> k).
(HasLimits j k, Representable d, Profunctor p) =>
((p :.: j) :~> d) -> p :~> Limit j d
limitUniv @j2 @k @d (\((p a b
p' :.: j1 b b
j1) :.: j2 b b
j2) -> (:.:) p (j1 :.: j2) a b -> d a b
(p :.: (j1 :.: j2)) :~> d
n (p a b
p' p a b -> (:.:) j1 j2 b b -> (:.:) p (j1 :.: j2) a b
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
:.: (j1 b b
j1 j1 b b -> j2 b b -> (:.:) j1 j2 b b
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
:.: j2 b b
j2))))

instance (FunctorForRep f) => HasLimits (Corep f) k where
  type Limit (Corep f) d = d :.: Rep f
  limit :: forall (d :: i +-> k).
Representable d =>
(Limit (Corep f) d :.: Corep f) :~> d
limit ((d a b
d :.: Rep b ~> (f @ b)
f) :.: Corep (f @ b) ~> b
g) = (b ~> b) -> d a b -> d a b
forall (b :: i) (d :: i) (a :: k). (b ~> d) -> d a b -> d a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap ((f @ b) ~> b
g ((f @ b) ~> b) -> (b ~> (f @ b)) -> b ~> b
forall (b :: i) (c :: i) (a :: i). (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
. b ~> (f @ b)
f) d a b
d
  limitUniv :: forall (d :: i +-> k) (p :: a +-> k).
(Representable d, Profunctor p) =>
((p :.: Corep f) :~> d) -> p :~> Limit (Corep f) d
limitUniv (p :.: Corep f) :~> d
n p a b
p = p a b
p p a b
-> ((Ob a, Ob b) => (:.:) d (Rep f) a b) -> (:.:) d (Rep f) a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (:.:) p (Corep f) a (f @ b) -> d a (f @ b)
(p :.: Corep f) :~> d
n (p a b
p p a b -> Corep f b (f @ b) -> (:.:) p (Corep f) a (f @ b)
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
:.: Corep f b (f @ b)
Corep f b (Corep f %% b)
forall (a :: a). Ob a => Corep f a (Corep f %% a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv) d a (f @ b) -> Rep f (f @ b) b -> (:.:) d (Rep f) a b
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
:.: Rep f (f @ b) b
Rep f (Rep f % b) b
forall (a :: a). Ob a => Rep f (Rep f % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
repUniv

newtype AnyLimit j a b = AnyLimit (j a b)
  deriving newtype (CategoryOf k
CategoryOf j
(CategoryOf j, CategoryOf k) =>
(forall (c :: k) (a :: k) (b :: j) (d :: j).
 (c ~> a) -> (b ~> d) -> AnyLimit j a b -> AnyLimit j c d)
-> (forall (c :: k) (a :: k) (b :: j).
    (c ~> a) -> AnyLimit j a b -> AnyLimit j c b)
-> (forall (b :: j) (d :: j) (a :: k).
    (b ~> d) -> AnyLimit j a b -> AnyLimit j a d)
-> (forall (a :: k) (b :: j) r.
    ((Ob a, Ob b) => r) -> AnyLimit j a b -> r)
-> Profunctor (AnyLimit j)
forall (c :: k) (a :: k) (b :: j).
(c ~> a) -> AnyLimit j a b -> AnyLimit j c b
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> AnyLimit j a b -> AnyLimit j c d
forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> AnyLimit j a b -> r
forall (b :: j) (d :: j) (a :: k).
(b ~> d) -> AnyLimit j a b -> AnyLimit j a d
forall k j (j :: k -> j -> Type). Profunctor j => CategoryOf k
forall k j (j :: k -> j -> Type). Profunctor j => CategoryOf j
forall k j (j :: k -> j -> Type) (c :: k) (a :: k) (b :: j).
Profunctor j =>
(c ~> a) -> AnyLimit j a b -> AnyLimit j c b
forall k j (j :: k -> j -> Type) (c :: k) (a :: k) (b :: j)
       (d :: j).
Profunctor j =>
(c ~> a) -> (b ~> d) -> AnyLimit j a b -> AnyLimit j c d
forall k j (j :: k -> j -> Type) (a :: k) (b :: j) r.
Profunctor j =>
((Ob a, Ob b) => r) -> AnyLimit j a b -> r
forall k j (j :: k -> j -> Type) (b :: j) (d :: j) (a :: k).
Profunctor j =>
(b ~> d) -> AnyLimit j a b -> AnyLimit j a d
forall {j} {k} (p :: j +-> k).
(CategoryOf j, CategoryOf k) =>
(forall (c :: k) (a :: k) (b :: j) (d :: j).
 (c ~> a) -> (b ~> d) -> p a b -> p c d)
-> (forall (c :: k) (a :: k) (b :: j). (c ~> a) -> p a b -> p c b)
-> (forall (b :: j) (d :: j) (a :: k). (b ~> d) -> p a b -> p a d)
-> (forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r)
-> Profunctor p
$cdimap :: forall k j (j :: k -> j -> Type) (c :: k) (a :: k) (b :: j)
       (d :: j).
Profunctor j =>
(c ~> a) -> (b ~> d) -> AnyLimit j a b -> AnyLimit j c d
dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> AnyLimit j a b -> AnyLimit j c d
$clmap :: forall k j (j :: k -> j -> Type) (c :: k) (a :: k) (b :: j).
Profunctor j =>
(c ~> a) -> AnyLimit j a b -> AnyLimit j c b
lmap :: forall (c :: k) (a :: k) (b :: j).
(c ~> a) -> AnyLimit j a b -> AnyLimit j c b
$crmap :: forall k j (j :: k -> j -> Type) (b :: j) (d :: j) (a :: k).
Profunctor j =>
(b ~> d) -> AnyLimit j a b -> AnyLimit j a d
rmap :: forall (b :: j) (d :: j) (a :: k).
(b ~> d) -> AnyLimit j a b -> AnyLimit j a d
$c\\ :: forall k j (j :: k -> j -> Type) (a :: k) (b :: j) r.
Profunctor j =>
((Ob a, Ob b) => r) -> AnyLimit j a b -> r
\\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> AnyLimit j a b -> r
Profunctor)
type Ran :: (i +-> a) -> (i +-> Type) -> a -> Type
newtype Ran j d a = Ran {forall i a (j :: i +-> a) (d :: i +-> Type) (a :: a).
Ran j d a -> forall (b :: i). j a b -> d % b
runRan :: forall b. j a b -> d % b}
instance (Profunctor j, Representable d) => Functor (Ran j d) where
  map :: forall (a :: k1) (b :: k1). (a ~> b) -> Ran j d a ~> Ran j d b
map a ~> b
f (Ran forall (b :: i). j a b -> d % b
g) = (forall (b :: i). j b b -> d % b) -> Ran j d b
forall i a (j :: i +-> a) (d :: i +-> Type) (a :: a).
(forall (b :: i). j a b -> d % b) -> Ran j d a
Ran \j b b
j -> j a b -> d % b
forall (b :: i). j a b -> d % b
g ((a ~> b) -> j b b -> j a b
forall (c :: k1) (a :: k1) (b :: i). (c ~> a) -> j a b -> j c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> b
f j b b
j)
instance (Profunctor j) => HasLimits (AnyLimit j) Type where
  type Limit (AnyLimit j) d = Star (Ran j d)
  limit :: forall (d :: i +-> Type).
Representable d =>
(Limit (AnyLimit j) d :.: AnyLimit j) :~> d
limit (Star a ~> Ran j d b
f :.: AnyLimit j b b
j) = (a ~> (d % b)) -> d a b
forall (b :: i) a. Ob b => (a ~> (d % b)) -> d a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (\a
a -> Ran j d b -> forall (b :: i). j b b -> d % b
forall i a (j :: i +-> a) (d :: i +-> Type) (a :: a).
Ran j d a -> forall (b :: i). j a b -> d % b
runRan (a ~> Ran j d b
a -> Ran j d b
f a
a) j b b
j) ((Ob b, Ob b) => d a b) -> j b b -> d a b
forall (a :: a) (b :: i) r. ((Ob a, Ob b) => r) -> j a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ j b b
j
  limitUniv :: forall (d :: i +-> Type) (p :: a +-> Type).
(Representable d, Profunctor p) =>
((p :.: AnyLimit j) :~> d) -> p :~> Limit (AnyLimit j) d
limitUniv (p :.: AnyLimit j) :~> d
n p a b
p = p a b
p p a b
-> ((Ob a, Ob b) => Star' ('NT (Ran j d)) a b)
-> Star' ('NT (Ran j d)) a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (a ~> Ran j d b) -> Star' ('NT (Ran j d)) a b
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (\a
a -> (forall (b :: i). j b b -> d % b) -> Ran j d b
forall i a (j :: i +-> a) (d :: i +-> Type) (a :: a).
(forall (b :: i). j a b -> d % b) -> Ran j d a
Ran \j b b
j -> d a b -> a ~> (d % b)
forall a (b :: i). d a b -> a ~> (d % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index ((:.:) p (AnyLimit j) a b -> d a b
(p :.: AnyLimit j) :~> d
n (p a b
p p a b -> AnyLimit j b b -> (:.:) p (AnyLimit j) a b
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
:.: j b b -> AnyLimit j b b
forall {k} {k} (j :: k -> k -> Type) (a :: k) (b :: k).
j a b -> AnyLimit j a b
AnyLimit j b b
j)) a
a)