{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Category.Limit where

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

import Proarrow.Category.Instance.Coproduct (COPRODUCT(..), (:++:)(..))
import Proarrow.Category.Instance.Unit (UNIT(..), Unit(..))
import Proarrow.Category.Instance.Zero (VOID)
import Proarrow.Core (PRO, (:~>), CategoryOf (..), Promonad(..), Profunctor(..), (//), CategoryOf, Kind, UN)
import Proarrow.Profunctor.Terminal (TerminalProfunctor(TerminalProfunctor'))
import Proarrow.Profunctor.Representable (Representable (..), withRepCod, dimapRep)
import Proarrow.Profunctor.Rift (type (<|), Rift (..))
import Proarrow.Object (Obj)
import Proarrow.Object.Terminal (HasTerminalObject(..), terminate)
import Proarrow.Object.BinaryProduct (HasBinaryProducts(..), fst, snd)
import Proarrow.Category.Opposite (OPPOSITE(..), Op(..))
import Proarrow.Category.Instance.Product ((:**:)(..), Fst, Snd)

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

-- profunctor-weighted limits
type HasLimits :: PRO a i -> Kind -> Constraint
class (forall (d :: PRO k i). Representable d => IsRepresentableLimit j d) => HasLimits (j :: PRO a i) k where
  type Limit (j :: PRO a i) (d :: PRO k i) :: PRO k a
  limit :: Representable (d :: PRO k i) => Limit j d :~> d <| j
  limitInv :: Representable (d :: PRO k i) => d <| j :~> Limit j d

type Unweighted = TerminalProfunctor


type TerminalLimit :: PRO k VOID -> PRO k UNIT
data TerminalLimit d a b where
  TerminalLimit :: forall d a. a ~> TerminalObject -> TerminalLimit d a U

instance HasTerminalObject k => Profunctor (TerminalLimit (d :: PRO k VOID)) where
  dimap :: forall (c :: k) (a :: k) (b :: UNIT) (d :: UNIT).
(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 :: PRO j k) (a :: j) (b :: k) (c :: j) (d :: k).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: UNIT) 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 :: PRO k VOID)) where
  type TerminalLimit d % U = TerminalObject
  index :: forall (a :: k) (b :: UNIT).
TerminalLimit d a b -> a ~> (TerminalLimit d % b)
index (TerminalLimit a ~> TerminalObject
f) = a ~> (TerminalLimit d % b)
a ~> TerminalObject
f
  tabulate :: forall (b :: UNIT) (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 U
forall {k} (d :: PRO k VOID) (a :: k).
(a ~> TerminalObject) -> TerminalLimit d a U
TerminalLimit
  repMap :: forall (a :: UNIT) (b :: UNIT).
(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 :: PRO UNIT VOID) k where
  type Limit Unweighted d = TerminalLimit d
  limit :: forall (d :: PRO k VOID).
Representable d =>
Limit Unweighted d :~> (d <| Unweighted)
limit (TerminalLimit @d a ~> TerminalObject
f) = a ~> TerminalObject
f (a ~> TerminalObject)
-> ((Ob a, Ob TerminalObject) => (<|) d Unweighted a b)
-> (<|) d Unweighted 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
// (forall (x :: VOID). Ob x => Unweighted b x -> d a x)
-> (<|) d Unweighted a b
forall {j} {k} {i} (a :: j) (b :: k) (j2 :: PRO k i)
       (p :: PRO j i).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j2 b x -> p a x) -> Rift ('OP j2) p a b
Rift \(TerminalProfunctor' Obj b
_ Obj x
o) -> (a ~> (d % x)) -> d a x
forall {j} {k} (p :: PRO j k) (b :: k) (a :: j).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (b :: VOID) (a :: k). Ob b => (a ~> (d % b)) -> d a b
tabulate (case Obj x
o of (TerminalObject ~> (d % x))
-> (a ~> TerminalObject) -> a ~> (d % x)
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 ~> TerminalObject
f)
  limitInv :: forall (d :: PRO k VOID).
Representable d =>
(d <| Unweighted) :~> Limit Unweighted d
limitInv Rift{} = (a ~> TerminalObject) -> TerminalLimit d a U
forall {k} (d :: PRO k VOID) (a :: k).
(a ~> TerminalObject) -> TerminalLimit d a U
TerminalLimit a ~> TerminalObject
forall {k} (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate


type ProductLimit :: PRO k (COPRODUCT UNIT UNIT) -> PRO k UNIT
data ProductLimit d a b where
  ProductLimit :: forall d a. a ~> ProductLimit d % U -> ProductLimit d a U

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

instance HasBinaryProducts k => HasLimits (Unweighted :: PRO UNIT (COPRODUCT UNIT UNIT)) k where
  type Limit Unweighted d = ProductLimit d
  limit :: forall (d :: PRO k (COPRODUCT UNIT UNIT)).
Representable d =>
Limit Unweighted d :~> (d <| Unweighted)
limit (ProductLimit @d a ~> (ProductLimit d % U)
f) = a ~> (ProductLimit d % U)
a ~> ((d % 'L U) && (d % 'R U))
f (a ~> ((d % 'L U) && (d % 'R U)))
-> ((Ob a, Ob ((d % 'L U) && (d % 'R U))) => (<|) d Unweighted a b)
-> (<|) d Unweighted 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
// (forall (x :: COPRODUCT UNIT UNIT).
 Ob x =>
 Unweighted b x -> d a x)
-> (<|) d Unweighted a b
forall {j} {k} {i} (a :: j) (b :: k) (j2 :: PRO k i)
       (p :: PRO j i).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j2 b x -> p a x) -> Rift ('OP j2) p a b
Rift \(TerminalProfunctor' Obj b
_ Obj x
o) -> (a ~> (d % x)) -> d a x
forall {j} {k} (p :: PRO j k) (b :: k) (a :: j).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (b :: COPRODUCT UNIT UNIT) (a :: k).
Ob b =>
(a ~> (d % b)) -> d a b
tabulate ((a ~> (d % x)) -> d a x) -> (a ~> (d % x)) -> d a x
forall a b. (a -> b) -> a -> b
$ forall k (d :: PRO k (COPRODUCT UNIT UNIT))
       (b :: COPRODUCT UNIT UNIT).
(HasBinaryProducts k, Representable d) =>
Obj b -> ((d % 'L U) && (d % 'R U)) ~> (d % b)
choose @_ @d Obj x
o (((d % 'L U) && (d % 'R U)) ~> (d % x))
-> (a ~> ((d % 'L U) && (d % 'R U))) -> a ~> (d % x)
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 % U)
a ~> ((d % 'L U) && (d % 'R U))
f
  limitInv :: forall (d :: PRO k (COPRODUCT UNIT UNIT)).
Representable d =>
(d <| Unweighted) :~> Limit Unweighted d
limitInv (Rift forall (x :: COPRODUCT UNIT UNIT). Ob x => j2 b x -> d a x
k) =
    let l :: d a ('L U)
l = j2 b ('L U) -> d a ('L U)
forall (x :: COPRODUCT UNIT UNIT). Ob x => j2 b x -> d a x
k (Obj b -> ('L U ~> 'L U) -> TerminalProfunctor b ('L U)
forall j k (a :: j) (b :: k).
(CategoryOf j, CategoryOf k) =>
Obj a -> Obj b -> TerminalProfunctor a b
TerminalProfunctor' Obj b
Unit U U
Unit (Unit U U -> (:++:) Unit Unit ('L U) ('L U)
forall {j} {k} (c :: CAT j) (a1 :: j) (b1 :: j) (d :: CAT k).
c a1 b1 -> (:++:) c d ('L a1) ('L b1)
InjL Unit U U
Unit))
        r :: d a ('R U)
r = j2 b ('R U) -> d a ('R U)
forall (x :: COPRODUCT UNIT UNIT). Ob x => j2 b x -> d a x
k (Obj b -> ('R U ~> 'R U) -> TerminalProfunctor b ('R U)
forall j k (a :: j) (b :: k).
(CategoryOf j, CategoryOf k) =>
Obj a -> Obj b -> TerminalProfunctor a b
TerminalProfunctor' Obj b
Unit U U
Unit (Unit U U -> (:++:) Unit Unit ('R U) ('R U)
forall {k} {j} (d :: CAT k) (a1 :: k) (b1 :: k) (c :: CAT j).
d a1 b1 -> (:++:) c d ('R a1) ('R b1)
InjR Unit U U
Unit))
    in (a ~> (ProductLimit d % U)) -> ProductLimit d a U
forall {j} (d :: PRO j (COPRODUCT UNIT UNIT)) (a :: j).
(a ~> (ProductLimit d % U)) -> ProductLimit d a U
ProductLimit ((a ~> (ProductLimit d % U)) -> ProductLimit d a U)
-> (a ~> (ProductLimit d % U)) -> ProductLimit d a U
forall a b. (a -> b) -> a -> b
$ d a ('L U) -> a ~> (d % 'L U)
forall (a :: k) (b :: COPRODUCT UNIT UNIT). d a b -> a ~> (d % b)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
Representable p =>
p a b -> a ~> (p % b)
index d a ('L U)
l (a ~> (d % 'L U))
-> (a ~> (d % 'R U)) -> a ~> ((d % 'L U) && (d % 'R U))
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 U) -> a ~> (d % 'R U)
forall (a :: k) (b :: COPRODUCT UNIT UNIT). d a b -> a ~> (d % b)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
Representable p =>
p a b -> a ~> (p % b)
index d a ('R U)
r

choose
  :: forall k (d :: PRO k (COPRODUCT UNIT UNIT)) b
  .  (HasBinaryProducts k, Representable d)
  => Obj b -> ((d % L U) && (d % R U)) ~> (d % b)
choose :: forall k (d :: PRO k (COPRODUCT UNIT UNIT))
       (b :: COPRODUCT UNIT UNIT).
(HasBinaryProducts k, Representable d) =>
Obj b -> ((d % 'L U) && (d % 'R U)) ~> (d % b)
choose Obj b
b = forall {k1} {k2} (p :: PRO k1 k2) (a :: k2) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: PRO k (COPRODUCT UNIT UNIT))
       (a :: COPRODUCT UNIT UNIT) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withRepCod @d @(L U) ((Ob (d % 'L U) => ((d % 'L U) && (d % 'R U)) ~> (d % b))
 -> ((d % 'L U) && (d % 'R U)) ~> (d % b))
-> (Ob (d % 'L U) => ((d % 'L U) && (d % 'R U)) ~> (d % b))
-> ((d % 'L U) && (d % 'R U)) ~> (d % b)
forall a b. (a -> b) -> a -> b
$ forall {k1} {k2} (p :: PRO k1 k2) (a :: k2) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: PRO k (COPRODUCT UNIT UNIT))
       (a :: COPRODUCT UNIT UNIT) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withRepCod @d @(R U) ((Ob (d % 'R U) => ((d % 'L U) && (d % 'R U)) ~> (d % b))
 -> ((d % 'L U) && (d % 'R U)) ~> (d % b))
-> (Ob (d % 'R U) => ((d % 'L U) && (d % 'R U)) ~> (d % b))
-> ((d % 'L U) && (d % 'R U)) ~> (d % b)
forall a b. (a -> b) -> a -> b
$ case Obj b
b of
  (InjL Unit a1 b1
Unit b1 b1
Unit) -> forall (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @(d % L U) @(d % R U)
  (InjR Unit a1 b1
Unit b1 b1
Unit) -> forall (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @(d % L U) @(d % R U)



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

type EndLimit :: PRO Type (OPPOSITE k, k) -> PRO Type UNIT
data EndLimit d a b where
  EndLimit :: forall d a. (a -> End d) -> EndLimit d a U

instance Representable d => Profunctor (EndLimit (d :: PRO Type (OPPOSITE k, k))) where
  dimap :: forall c a (b :: UNIT) (d :: UNIT).
(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 :: PRO j k) (a :: j) (b :: k) (c :: j) (d :: k).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall a (b :: UNIT) 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 :: PRO Type (OPPOSITE k, k))) where
  type EndLimit d % U = End d
  index :: forall a (b :: UNIT). 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 :: UNIT) 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 U
forall {k} (d :: PRO Type (OPPOSITE k, k)) a.
(a -> End d) -> EndLimit d a U
EndLimit
  repMap :: forall (a :: UNIT) (b :: UNIT).
(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 :: PRO UNIT (OPPOSITE k, k)
data Hom a b where
  Hom :: Ob ab => UN OP (Fst ab) ~> Snd ab -> Hom U ab
instance CategoryOf k => Profunctor (Hom :: PRO UNIT (OPPOSITE k, k)) where
  dimap :: forall (c :: UNIT) (a :: UNIT) (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 UN 'OP (Fst b) ~> Snd b
f) = (UN 'OP (Fst d) ~> Snd d) -> Hom U d
forall {b} (ab :: (OPPOSITE b, b)).
Ob ab =>
(UN 'OP (Fst ab) ~> Snd ab) -> Hom U ab
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
UN 'OP (Fst b) ~> Snd 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 :: UNIT) (b :: (OPPOSITE k, k)) r.
((Ob a, Ob b) => r) -> Hom a b -> r
\\ Hom UN 'OP (Fst b) ~> Snd b
f = r
(Ob (UN 'OP (Fst b)), Ob (Snd b)) => r
(Ob a, Ob b) => r
r ((Ob (UN 'OP (Fst b)), Ob (Snd b)) => r)
-> (UN 'OP (Fst b) ~> Snd 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
\\ UN 'OP (Fst b) ~> Snd b
f

instance CategoryOf k => HasLimits (Hom :: PRO UNIT (OPPOSITE k, k)) Type where
  type Limit Hom d = EndLimit d
  limit :: forall (d :: PRO Type (OPPOSITE k, k)).
Representable d =>
Limit Hom d :~> (d <| Hom)
limit (EndLimit @d a -> End d
f) = a -> End d
f (a -> End d)
-> ((Ob a, Ob (End d)) => (<|) d Hom a b) -> (<|) d Hom 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
// (forall (x :: (OPPOSITE k, k)). Ob x => Hom b x -> d a x)
-> (<|) d Hom a b
forall {j} {k} {i} (a :: j) (b :: k) (j2 :: PRO k i)
       (p :: PRO j i).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j2 b x -> p a x) -> Rift ('OP j2) p a b
Rift \(Hom UN 'OP (Fst x) ~> Snd x
k) -> forall {j} {k} (p :: PRO j k) (b :: k) (a :: j).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: PRO Type (OPPOSITE k, k)) (b :: (OPPOSITE k, k)) a.
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @d (\a
a -> End d -> forall (a :: k) (b :: k). (a ~> b) -> d % '( 'OP a, b)
forall {k} (d :: PRO Type (OPPOSITE k, k)).
End d -> forall (a :: k) (b :: k). (a ~> b) -> d % '( 'OP a, b)
getEnd (a -> End d
f a
a) UN 'OP (Fst x) ~> Snd x
k)
  limitInv :: forall (d :: PRO Type (OPPOSITE k, k)).
Representable d =>
(d <| Hom) :~> Limit Hom d
limitInv (Rift forall (x :: (OPPOSITE k, k)). Ob x => j2 b x -> d a x
n) = (a -> End d) -> EndLimit d a U
forall {k} (d :: PRO Type (OPPOSITE k, k)) a.
(a -> End d) -> EndLimit d a U
EndLimit \a
a -> (forall (a :: k) (b :: k). (a ~> b) -> d % '( 'OP a, b)) -> End d
forall {k} (d :: PRO Type (OPPOSITE k, k)).
(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 :: PRO j k) (a :: j) (b :: k).
Representable p =>
p a b -> a ~> (p % b)
forall a (b :: (OPPOSITE k, k)). d a b -> a ~> (d % b)
index (j2 b '( 'OP a, b) -> d a '( 'OP a, b)
forall (x :: (OPPOSITE k, k)). Ob x => j2 b x -> d a x
n ((UN 'OP (Fst '( 'OP a, b)) ~> Snd '( 'OP a, b))
-> Hom U '( 'OP a, b)
forall {b} (ab :: (OPPOSITE b, b)).
Ob ab =>
(UN 'OP (Fst ab) ~> Snd ab) -> Hom U ab
Hom a ~> b
UN 'OP (Fst '( 'OP a, b)) ~> Snd '( 'OP a, b)
x)) a
a ((Ob a, Ob b) => d % '( 'OP a, b)) -> (a ~> b) -> d % '( 'OP a, b)
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
x