{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Limit where

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

import Proarrow.Adjunction (Adjunction (..))
import Proarrow.Category.Instance.Coproduct (COPRODUCT, L, R, pattern InjL, pattern InjR)
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit (Unit (..))
import Proarrow.Category.Instance.Zero (VOID)
import Proarrow.Category.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Core (CAT, CategoryOf (..), Kind, Profunctor (..), Promonad (..), lmap, rmap, (//), (:~>), type (+->))
import Proarrow.Object (Obj, tgt)
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..), fst, snd)
import Proarrow.Object.Power (Powered (..))
import Proarrow.Object.Terminal (HasTerminalObject (..), terminate)
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.HaskValue (HaskValue (..))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Representable (Representable (..), repObj, withRepOb, CorepStar (..), FunctorForRep (..), Rep (..))
import Proarrow.Profunctor.Terminal (TerminalProfunctor (TerminalProfunctor'))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), trivialCorep)
import Proarrow.Profunctor.Wrapped (Wrapped)

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

rightAdjointPreservesLimits
  :: forall {k} {k'} {i} {a} (f :: k' +-> k) (g :: k +-> k') (d :: i +-> k) (j :: i +-> a)
   . (Adjunction f g, Representable d, Representable f, Representable g, HasLimits j k, HasLimits j k')
  => Limit j (g :.: d) :~> g :.: Limit j d
rightAdjointPreservesLimits :: forall {k} {k'} {i} {a} (f :: k' +-> k) (g :: k +-> k')
       (d :: i +-> k) (j :: i +-> a).
(Adjunction f g, Representable d, Representable f, Representable g,
 HasLimits j k, HasLimits j k') =>
Limit j (g :.: d) :~> (g :.: Limit j d)
rightAdjointPreservesLimits Limit j (g :.: d) a b
lim =
  Limit j (g :.: d) a b
lim Limit j (g :.: d) a b
-> ((Ob a, Ob b) => (:.:) g (Limit j d) a b)
-> (:.:) g (Limit 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
// case forall {j} {k} (p :: j +-> k) (q :: k +-> j) (a :: j).
(Adjunction p q, Ob a) =>
(:.:) q p a a
forall (p :: k' +-> k) (q :: k +-> k') (a :: k').
(Adjunction p q, Ob a) =>
(:.:) q p a a
unit @f @g of
    g a b
g :.: f b a
f ->
      g a b
g
        g a b -> Limit j d b b -> (:.:) g (Limit j d) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: 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 @k @d
          (\((f a b
f' :.: Limit j (g :.: d) b b
lim') :.: j b b
j) -> case 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 @k' @(g :.: d) (Limit j (g :.: d) b b
lim' Limit j (g :.: d) b b -> j b b -> (:.:) (Limit j (g :.: d)) j b b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: j b b
j) of g b b
g' :.: d b b
d -> (a ~> b) -> d b b -> d a b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap ((:.:) f g a b -> a ~> b
(f :.: g) :~> (~>)
forall {j} {k} (p :: j +-> k) (q :: k +-> j).
Adjunction p q =>
(p :.: q) :~> (~>)
counit (f a b
f' f a b -> g b b -> (:.:) f g a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: g b b
g')) d b b
d)
          (f b a
f f b a -> Limit j (g :.: d) a b -> (:.:) f (Limit j (g :.: d)) b b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: Limit j (g :.: d) a b
lim)

rightAdjointPreservesLimitsInv
  :: forall {k} {k'} {i} {a} (g :: k +-> k') (d :: i +-> k) (j :: i +-> a)
   . (Representable d, Representable g, HasLimits j k, HasLimits j k')
  => g :.: Limit j d :~> Limit j (g :.: d)
rightAdjointPreservesLimitsInv :: forall {k} {k'} {i} {a} (g :: k +-> k') (d :: i +-> k)
       (j :: i +-> a).
(Representable d, Representable g, HasLimits j k,
 HasLimits j k') =>
(g :.: Limit j d) :~> Limit j (g :.: d)
rightAdjointPreservesLimitsInv = 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 @k' @(g :.: d) (\((g a b
g :.: Limit j d b b
lim) :.: j b b
j) -> g a b
g g a b -> d b b -> (:.:) g d a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (:.:) (Limit j d) j b b -> d b b
(Limit j d :.: j) :~> d
forall {a} {i} (j :: i +-> a) k (d :: i +-> k).
(HasLimits j k, Representable d) =>
(Limit j d :.: j) :~> d
forall (d :: i +-> k). Representable d => (Limit j d :.: j) :~> d
limit (Limit j d b b
lim Limit j d b b -> j b b -> (:.:) (Limit j d) j b b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: j b b
j))

type Unweighted = TerminalProfunctor

data family TerminalLimit :: VOID +-> k -> () +-> k
instance (HasTerminalObject k) => FunctorForRep (TerminalLimit d :: () +-> k) where
  type TerminalLimit d @ a = TerminalObject
  fmap :: forall (a :: ()) (b :: ()).
(a ~> b) -> (TerminalLimit d @ a) ~> (TerminalLimit d @ b)
fmap a ~> b
Unit a b
Unit = (TerminalLimit d @ a) ~> (TerminalLimit d @ b)
TerminalObject ~> TerminalObject
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

instance (HasTerminalObject k) => HasLimits (Unweighted :: VOID +-> ()) k where
  type Limit Unweighted d = Rep (TerminalLimit d)
  limit :: forall (d :: VOID +-> k).
Representable d =>
(Limit Unweighted d :.: Unweighted) :~> d
limit = \case {}
  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 (TerminalLimit d) a b)
-> Rep (TerminalLimit 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 ~> (TerminalLimit d @ b)) -> Rep (TerminalLimit d) a b
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep a ~> (TerminalLimit d @ b)
a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate

data family ProductLimit :: COPRODUCT () () +-> k -> () +-> k
instance (HasBinaryProducts k, Representable d) => FunctorForRep (ProductLimit d :: () +-> k) where
  type ProductLimit d @ '() = (d % L '()) && (d % R '())
  fmap :: forall (a :: ()) (b :: ()).
(a ~> b) -> (ProductLimit d @ a) ~> (ProductLimit d @ b)
fmap a ~> b
Unit a b
Unit = forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
(***) @_ @(d % L '()) @(d % R '()) (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: COPRODUCT () () +-> k) (a :: COPRODUCT () ())
       (b :: COPRODUCT () ()).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @d (Unit '() '() -> (:++:) Unit Unit (L '()) (L '())
forall {j1} {k1} {j2} {k2} (p :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (q :: j2 +-> k2).
p a1 b1 -> (:++:) p q (L a1) (L b1)
InjL Unit '() '()
Unit)) (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: COPRODUCT () () +-> k) (a :: COPRODUCT () ())
       (b :: COPRODUCT () ()).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @d (Unit '() '() -> (:++:) Unit Unit (R '()) (R '())
forall {j2} {k2} {j1} {k1} (q :: j2 +-> k2) (a1 :: k2) (b1 :: j2)
       (p :: j1 +-> k1).
q a1 b1 -> (:++:) p q (R a1) (R b1)
InjR Unit '() '()
Unit))

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 (Rep @(ProductLimit d) a ~> (ProductLimit d @ b)
f :.: TerminalProfunctor' Obj b
_ Obj b
o) = Obj b
(:++:) Unit Unit b b
o (:++:) Unit Unit b b -> ((Ob b, 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 :: COPRODUCT () ()) (a :: k).
Ob b =>
(a ~> (d % b)) -> d a b
tabulate ((a ~> (d % b)) -> d a b) -> (a ~> (d % b)) -> d a b
forall a b. (a -> b) -> a -> b
$ forall k (d :: COPRODUCT () () +-> k) (b :: COPRODUCT () ()).
(HasBinaryProducts k, Representable d) =>
Obj b -> ((d % L '()) && (d % R '())) ~> (d % b)
choose @_ @d Obj b
o (((d % L '()) && (d % R '())) ~> (d % b))
-> (a ~> ((d % L '()) && (d % R '()))) -> a ~> (d % 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
. a ~> (ProductLimit d @ b)
a ~> ((d % L '()) && (d % R '()))
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
//
      let l :: d a (L '())
l = (:.:) p Unweighted a (L '()) -> d a (L '())
(p :.: Unweighted) :~> d
n (p a b
p p a b -> Unweighted b (L '()) -> (:.:) p Unweighted a (L '())
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: Obj b -> (L '() ~> L '()) -> Unweighted b (L '())
forall k (a :: k) j (b :: j).
Obj a -> Obj b -> TerminalProfunctor a b
TerminalProfunctor' Obj b
Unit '() '()
Unit (Unit '() '() -> (:++:) Unit Unit (L '()) (L '())
forall {j1} {k1} {j2} {k2} (p :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (q :: j2 +-> k2).
p a1 b1 -> (:++:) p q (L a1) (L b1)
InjL Unit '() '()
Unit))
          r :: d a (R '())
r = (:.:) p Unweighted a (R '()) -> d a (R '())
(p :.: Unweighted) :~> d
n (p a b
p p a b -> Unweighted b (R '()) -> (:.:) p Unweighted a (R '())
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: Obj b -> (R '() ~> R '()) -> Unweighted b (R '())
forall k (a :: k) j (b :: j).
Obj a -> Obj b -> TerminalProfunctor a b
TerminalProfunctor' Obj b
Unit '() '()
Unit (Unit '() '() -> (:++:) Unit Unit (R '()) (R '())
forall {j2} {k2} {j1} {k1} (q :: j2 +-> k2) (a1 :: k2) (b1 :: j2)
       (p :: j1 +-> k1).
q a1 b1 -> (:++:) p q (R a1) (R b1)
InjR Unit '() '()
Unit))
      in (a ~> (ProductLimit d @ b)) -> Rep (ProductLimit d) a b
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep ((a ~> (ProductLimit d @ b)) -> Rep (ProductLimit d) a b)
-> (a ~> (ProductLimit d @ b)) -> Rep (ProductLimit d) a b
forall a b. (a -> b) -> a -> b
$ d a (L '()) -> a ~> (d % L '())
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 d a (L '())
l (a ~> (d % L '()))
-> (a ~> (d % R '())) -> a ~> ((d % L '()) && (d % R '()))
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 (R '()) -> a ~> (d % R '())
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 d a (R '())
r

choose
  :: forall k (d :: COPRODUCT () () +-> k) b
   . (HasBinaryProducts k, Representable d)
  => Obj b
  -> ((d % L '()) && (d % R '())) ~> (d % b)
choose :: forall k (d :: COPRODUCT () () +-> k) (b :: COPRODUCT () ()).
(HasBinaryProducts k, Representable d) =>
Obj b -> ((d % L '()) && (d % R '())) ~> (d % b)
choose Obj b
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
withRepOb @d @(L '()) ((Ob (d % L '()) => ((d % L '()) && (d % R '())) ~> (d % b))
 -> ((d % L '()) && (d % R '())) ~> (d % b))
-> (Ob (d % L '()) => ((d % L '()) && (d % R '())) ~> (d % b))
-> ((d % L '()) && (d % R '())) ~> (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
withRepOb @d @(R '()) ((Ob (d % R '()) => ((d % L '()) && (d % R '())) ~> (d % b))
 -> ((d % L '()) && (d % R '())) ~> (d % b))
-> (Ob (d % R '()) => ((d % L '()) && (d % R '())) ~> (d % b))
-> ((d % L '()) && (d % R '())) ~> (d % b)
forall a b. (a -> b) -> a -> b
$ case Obj b
b of
  (InjL Unit a1 b1
Unit b1 b1
Unit) -> forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @(d % L '()) @(d % R '())
  (InjR Unit a1 b1
Unit b1 b1
Unit) -> forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @(d % L '()) @(d % R '())

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 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 ((Ob (d % '()), Ob (d % '())) =>
 ((d % '()) ^ n) ~> ((d % '()) ^ n))
-> ((d % '()) ~> (d % '())) -> ((d % '()) ^ n) ~> ((d % '()) ^ n)
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
\\ forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
forall (p :: () +-> k) (a :: ()).
(Representable p, Ob a) =>
Obj (p % a)
repObj @d @'()
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) = (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) ((Ob (d % '()), Ob (d % '())) => d a b)
-> ((d % '()) ~> (d % '())) -> d a b
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
\\ forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
forall (p :: () +-> k) (a :: ()).
(Representable p, Ob a) =>
Obj (p % a)
repObj @d @'()
  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 = (a ~> (PowerLimit n d @ b)) -> Rep (PowerLimit n d) a b
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
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} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
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 ((Ob (d % '()), Ob (d % '())) => Rep (PowerLimit n d) a b)
-> ((d % '()) ~> (d % '())) -> Rep (PowerLimit n d) a b
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
\\ forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
forall (p :: () +-> k) (a :: ()).
(Representable p, Ob a) =>
Obj (p % a)
repObj @d @'()

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} (f :: j +-> k) (a :: k) (b :: j).
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} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
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 {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} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
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} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
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} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
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} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
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} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: j2 b b
j2))))

instance (Corepresentable j) => HasLimits (Wrapped j) k where
  type Limit (Wrapped j) d = d :.: CorepStar j
  limit :: forall (d :: i +-> k).
Representable d =>
(Limit (Wrapped j) d :.: Wrapped j) :~> d
limit ((d a b
d :.: CorepStar b ~> (j %% b)
f) :.: Wrapped j b b
g) = (b ~> b) -> d a b -> d a b
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap (Wrapped j b b -> (Wrapped j %% b) ~> b
forall (a :: a) (b :: i). Wrapped j a b -> (Wrapped j %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex Wrapped j b b
g ((j %% b) ~> b) -> (b ~> (j %% 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 ~> (j %% b)
f) d a b
d
  limitUniv :: forall (d :: i +-> k) (p :: a +-> k).
(Representable d, Profunctor p) =>
((p :.: Wrapped j) :~> d) -> p :~> Limit (Wrapped j) d
limitUniv (p :.: Wrapped j) :~> d
n p a b
p = p a b
p p a b
-> ((Ob a, Ob b) => (:.:) d (CorepStar j) a b)
-> (:.:) d (CorepStar j) 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 (Wrapped j) a (j %% b) -> d a (j %% b)
(p :.: Wrapped j) :~> d
n (p a b
p p a b -> Wrapped j b (j %% b) -> (:.:) p (Wrapped j) a (j %% b)
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: Wrapped j b (j %% b)
Wrapped j b (Wrapped j %% b)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
trivialCorep) d a (j %% b) -> CorepStar j (j %% b) b -> (:.:) d (CorepStar j) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: ((j %% b) ~> (j %% b)) -> CorepStar j (j %% b) b
forall {j} {k} (b :: j) (a :: k) (p :: k +-> j).
Ob b =>
(a ~> (p %% b)) -> CorepStar p a b
CorepStar (forall {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: i +-> a) (a :: a) (b :: a).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @j (p a b -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt p a b
p))