{-# 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 (CategoryOf (..), Kind, Profunctor (..), Promonad (..), lmap, (//), (:~>), type (+->))
import Proarrow.Object (Obj)
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..), fst, snd)
import Proarrow.Object.Terminal (HasTerminalObject (..), terminate)
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Representable (Representable (..), dimapRep, withRepObj)
import Proarrow.Profunctor.Terminal (TerminalProfunctor (TerminalProfunctor'))

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), Representable 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 :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// case forall {j} {k} (p :: PRO k j) (q :: PRO j k) (a :: j).
(Adjunction p q, Ob a) =>
(:.:) q p a a
forall (p :: PRO k k') (q :: PRO 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, Representable p) =>
((p :.: j) :~> d) -> p :~> Limit j d
forall (j :: i +-> a) k (d :: i +-> k) (p :: a +-> k).
(HasLimits j k, Representable d, Representable 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 :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap ((:.:) f g a b -> a ~> b
(f :.: g) :~> (~>)
forall {j} {k} (p :: PRO k j) (q :: PRO j k).
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, Representable p) =>
((p :.: j) :~> d) -> p :~> Limit j d
forall (j :: i +-> a) k (d :: i +-> k) (p :: a +-> k).
(HasLimits j k, Representable d, Representable 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

type TerminalLimit :: VOID +-> k -> () +-> k
data TerminalLimit d a b where
  TerminalLimit :: forall d a. a ~> TerminalObject -> TerminalLimit d a '()

instance (HasTerminalObject k) => Profunctor (TerminalLimit (d :: VOID +-> k)) where
  dimap :: forall (c :: k) (a :: k) (b :: ()) (d :: ()).
(c ~> a) -> (b ~> d) -> TerminalLimit d a b -> TerminalLimit d c d
dimap = (c ~> a) -> (b ~> d) -> TerminalLimit d a b -> TerminalLimit d c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: ()) r.
((Ob a, Ob b) => r) -> TerminalLimit d a b -> r
\\ TerminalLimit a ~> TerminalObject
f = r
(Ob a, Ob TerminalObject) => r
(Ob a, Ob b) => r
r ((Ob a, Ob TerminalObject) => r) -> (a ~> TerminalObject) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> TerminalObject
f
instance (HasTerminalObject k) => Representable (TerminalLimit (d :: VOID +-> k)) where
  type TerminalLimit d % '() = TerminalObject
  index :: forall (a :: k) (b :: ()).
TerminalLimit d a b -> a ~> (TerminalLimit d % b)
index (TerminalLimit a ~> TerminalObject
f) = a ~> (TerminalLimit d % b)
a ~> TerminalObject
f
  tabulate :: forall (b :: ()) (a :: k).
Ob b =>
(a ~> (TerminalLimit d % b)) -> TerminalLimit d a b
tabulate = (a ~> (TerminalLimit d % b)) -> TerminalLimit d a b
(a ~> TerminalObject) -> TerminalLimit d a '()
forall {k} (d :: VOID +-> k) (a :: k).
(a ~> TerminalObject) -> TerminalLimit d a '()
TerminalLimit
  repMap :: forall (a :: ()) (b :: ()).
(a ~> b) -> (TerminalLimit d % a) ~> (TerminalLimit d % b)
repMap a ~> b
Unit a b
Unit = (TerminalLimit d % a) ~> (TerminalLimit d % b)
TerminalObject ~> TerminalObject
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id

instance (HasTerminalObject k) => HasLimits (Unweighted :: VOID +-> ()) k where
  type Limit Unweighted d = 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, Representable 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) => TerminalLimit d a b) -> TerminalLimit d a b
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (a ~> TerminalObject) -> TerminalLimit d a '()
forall {k} (d :: VOID +-> k) (a :: k).
(a ~> TerminalObject) -> TerminalLimit d a '()
TerminalLimit a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate

type ProductLimit :: COPRODUCT () () +-> k -> () +-> k
data ProductLimit d a b where
  ProductLimit :: forall d a. a ~> ProductLimit d % '() -> ProductLimit d a '()

instance (HasBinaryProducts k, Representable d) => Profunctor (ProductLimit d :: () +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: ()) (d :: ()).
(c ~> a) -> (b ~> d) -> ProductLimit d a b -> ProductLimit d c d
dimap = (c ~> a) -> (b ~> d) -> ProductLimit d a b -> ProductLimit d c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: ()) r.
((Ob a, Ob b) => r) -> ProductLimit d a b -> r
\\ (ProductLimit a ~> (ProductLimit d % '())
f) = r
(Ob a, Ob ((d % L '()) && (d % R '()))) => r
(Ob a, Ob b) => r
r ((Ob a, Ob ((d % L '()) && (d % R '()))) => r)
-> (a ~> ((d % L '()) && (d % R '()))) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> (ProductLimit d % '())
a ~> ((d % L '()) && (d % R '()))
f
instance (HasBinaryProducts k, Representable d) => Representable (ProductLimit d :: () +-> k) where
  type ProductLimit d % '() = (d % L '()) && (d % R '())
  index :: forall (a :: k) (b :: ()).
ProductLimit d a b -> a ~> (ProductLimit d % b)
index (ProductLimit a ~> (ProductLimit d % '())
f) = a ~> (ProductLimit d % b)
a ~> (ProductLimit d % '())
f
  tabulate :: forall (b :: ()) (a :: k).
Ob b =>
(a ~> (ProductLimit d % b)) -> ProductLimit d a b
tabulate = (a ~> (ProductLimit d % b)) -> ProductLimit d a b
(a ~> (ProductLimit d % '())) -> ProductLimit d a '()
forall {k} (d :: COPRODUCT () () +-> k) (a :: k).
(a ~> (ProductLimit d % '())) -> ProductLimit d a '()
ProductLimit
  repMap :: forall (a :: ()) (b :: ()).
(a ~> b) -> (ProductLimit d % a) ~> (ProductLimit d % b)
repMap 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 (('() ~> '()) -> (:++:) (~>) (~>) (L '()) (L '())
forall {k} {j} (a' :: COLLAGE InitialProfunctor)
       (b' :: COLLAGE InitialProfunctor) (a :: k) (b :: k).
(a' ~ L a, b' ~ L b) =>
(a ~> b) -> (:++:) (~>) (~>) a' b'
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 (('() ~> '()) -> (:++:) (~>) (~>) (R '()) (R '())
forall {k} {j} (a' :: COLLAGE InitialProfunctor)
       (b' :: COLLAGE InitialProfunctor) (a :: j) (b :: j).
(a' ~ R a, b' ~ R b) =>
(a ~> b) -> (:++:) (~>) (~>) a' b'
InjR '() ~> '()
Unit '() '()
Unit))

instance (HasBinaryProducts k) => HasLimits (Unweighted :: COPRODUCT () () +-> ()) k where
  type Limit Unweighted d = ProductLimit d
  limit :: forall (d :: COPRODUCT () () +-> k).
Representable d =>
(Limit Unweighted d :.: Unweighted) :~> d
limit (ProductLimit @d a ~> (ProductLimit d % '())
f :.: TerminalProfunctor' Obj b
_ Obj b
o) = Obj b
Collage b b
o Collage b b -> ((Ob b, Ob b) => d a b) -> d a b
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) 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 :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (ProductLimit d % '())
a ~> ((d % L '()) && (d % R '()))
f
  limitUniv :: forall (d :: COPRODUCT () () +-> k) (p :: () +-> k).
(Representable d, Representable 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) => ProductLimit d a b) -> ProductLimit d a b
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) 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 (('() ~> '()) -> (:++:) (~>) (~>) (L '()) (L '())
forall {k} {j} (a' :: COLLAGE InitialProfunctor)
       (b' :: COLLAGE InitialProfunctor) (a :: k) (b :: k).
(a' ~ L a, b' ~ L b) =>
(a ~> b) -> (:++:) (~>) (~>) a' b'
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 (('() ~> '()) -> (:++:) (~>) (~>) (R '()) (R '())
forall {k} {j} (a' :: COLLAGE InitialProfunctor)
       (b' :: COLLAGE InitialProfunctor) (a :: j) (b :: j).
(a' ~ R a, b' ~ R b) =>
(a ~> b) -> (:++:) (~>) (~>) a' b'
InjR '() ~> '()
Unit '() '()
Unit))
         in (a ~> (ProductLimit d % '())) -> ProductLimit d a '()
forall {k} (d :: COPRODUCT () () +-> k) (a :: k).
(a ~> (ProductLimit d % '())) -> ProductLimit d a '()
ProductLimit ((a ~> (ProductLimit d % '())) -> ProductLimit d a '())
-> (a ~> (ProductLimit d % '())) -> ProductLimit d a '()
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
withRepObj @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
withRepObj @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 a ~> b
Unit b b
Unit) -> forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @(d % L '()) @(d % R '())
  (InjR a ~> b
Unit b b
Unit) -> forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @(d % L '()) @(d % R '())

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

type EndLimit :: (OPPOSITE k, k) +-> Type -> () +-> Type
data EndLimit d a b where
  EndLimit :: forall d a. (a -> End d) -> EndLimit d a '()

instance (Representable d) => Profunctor (EndLimit (d :: (OPPOSITE k, k) +-> Type)) where
  dimap :: forall c a (b :: ()) (d :: ()).
(c ~> a) -> (b ~> d) -> EndLimit d a b -> EndLimit d c d
dimap = (c ~> a) -> (b ~> d) -> EndLimit d a b -> EndLimit d c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall a (b :: ()) r. ((Ob a, Ob b) => r) -> EndLimit d a b -> r
\\ EndLimit a -> End d
f = r
(Ob a, Ob (End d)) => r
(Ob a, Ob b) => r
r ((Ob a, Ob (End d)) => r) -> (a -> End d) -> r
forall a b r. ((Ob a, Ob b) => r) -> (a -> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a -> End d
f
instance (Representable d) => Representable (EndLimit (d :: (OPPOSITE k, k) +-> Type)) where
  type EndLimit d % '() = End d
  index :: forall a (b :: ()). EndLimit d a b -> a ~> (EndLimit d % b)
index (EndLimit a -> End d
f) = a ~> (EndLimit d % b)
a -> End d
f
  tabulate :: forall (b :: ()) a.
Ob b =>
(a ~> (EndLimit d % b)) -> EndLimit d a b
tabulate = (a ~> (EndLimit d % b)) -> EndLimit d a b
(a -> End d) -> EndLimit d a '()
forall {k} (d :: (OPPOSITE k, k) +-> Type) a.
(a -> End d) -> EndLimit d a '()
EndLimit
  repMap :: forall (a :: ()) (b :: ()).
(a ~> b) -> (EndLimit d % a) ~> (EndLimit d % b)
repMap 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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO j k) (a :: j) (b :: k) 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 :: PRO j k) (a :: j) (b :: k) 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 :: PRO j k) (a :: j) (b :: k) 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 = EndLimit d
  limit :: forall (d :: (OPPOSITE k, k) +-> Type).
Representable d =>
(Limit Hom d :.: Hom) :~> d
limit (EndLimit a -> End d
f :.: Hom a ~> b
k) = a ~> b
k (a ~> b) -> ((Ob a, Ob b) => d a b) -> d a b
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) 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 -> End d
f a
a) a ~> b
k)
  limitUniv :: forall (d :: (OPPOSITE k, k) +-> Type) (p :: () +-> Type).
(Representable d, Representable 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) => EndLimit d a b) -> EndLimit d a b
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (a -> End d) -> EndLimit d a '()
forall {k} (d :: (OPPOSITE k, k) +-> Type) a.
(a -> End d) -> EndLimit d a '()
EndLimit \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