{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Colimit where

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

import Proarrow.Category.Instance.Coproduct (COPRODUCT (..), IsLR (..))
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.Colimit.BinaryCoproduct (HasBinaryCoproducts (..), lft, rgt)
import Proarrow.Colimit.Copower (Copowered (..))
import Proarrow.Colimit.Initial (HasInitialObject (..), initiate)
import Proarrow.Core (CAT, CategoryOf (..), Kind, Profunctor (..), Promonad (..), lmap, (//), (:~>), type (+->))
import Proarrow.Functor (Functor (..), FunctorForRep (..))
import Proarrow.Profunctor.Corepresentable (Corep (..), Corepresentable (..), corepUniv, withObCorep)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Constant (Constant)
import Proarrow.Profunctor.Instance.Costar (Costar, pattern Costar)
import Proarrow.Profunctor.Instance.HaskValue (HaskValue (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Instance.Terminal (TerminalProfunctor (..))
import Proarrow.Profunctor.Representable (Rep (..), Representable (..))

type Unweighted = TerminalProfunctor

class (Corepresentable (Colimit j d)) => IsCorepColimit j d
instance (Corepresentable (Colimit j d)) => IsCorepColimit j d

-- | profunctor-weighted colimits
type HasColimits :: forall {i} {a}. a +-> i -> Kind -> Constraint
class (Profunctor j, forall (d :: k +-> i). (Corepresentable d) => IsCorepColimit j d) => HasColimits (j :: a +-> i) k where
  type Colimit (j :: a +-> i) (d :: k +-> i) :: k +-> a
  colimit :: (Corepresentable (d :: k +-> i)) => j :.: Colimit j d :~> d
  colimitUniv :: (Corepresentable (d :: k +-> i), Profunctor p) => (j :.: p :~> d) -> p :~> Colimit j d

mapColimit
  :: forall {i} j k p q
   . (HasColimits j k, Corepresentable p, Corepresentable q) => (p :: k +-> i) ~> q -> Colimit j p ~> Colimit j q
mapColimit :: forall {a} {i} (j :: a +-> i) k (p :: k +-> i) (q :: k +-> i).
(HasColimits j k, Corepresentable p, Corepresentable q) =>
(p ~> q) -> Colimit j p ~> Colimit j q
mapColimit (Prof p :~> q
n) = (Colimit j p :~> Colimit j q) -> Prof (Colimit j p) (Colimit j q)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof (forall {i} {a} (j :: a +-> i) k (d :: k +-> i) (p :: k +-> a).
(HasColimits j k, Corepresentable d, Profunctor p) =>
((j :.: p) :~> d) -> p :~> Colimit j d
forall (j :: a +-> i) k (d :: k +-> i) (p :: k +-> a).
(HasColimits j k, Corepresentable d, Profunctor p) =>
((j :.: p) :~> d) -> p :~> Colimit j d
colimitUniv @j (p a b -> q a b
p :~> q
n (p a b -> q a b)
-> ((:.:) j (Colimit j p) a b -> p a b)
-> (:.:) j (Colimit j p) 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 {i} {a} (j :: a +-> i) k (d :: k +-> i).
(HasColimits j k, Corepresentable d) =>
(j :.: Colimit j d) :~> d
forall (j :: a +-> i) k (d :: k +-> i).
(HasColimits j k, Corepresentable d) =>
(j :.: Colimit j d) :~> d
colimit @j))

instance (HasInitialObject k) => HasColimits (Unweighted :: () +-> VOID) k where
  type Colimit Unweighted d = Corep (Constant InitialObject)
  colimit :: forall (d :: k +-> VOID).
Corepresentable d =>
(Unweighted :.: Colimit Unweighted d) :~> d
colimit (Unweighted a b
t :.: Colimit Unweighted d b b
_) = case Unweighted a b
t of {}
  colimitUniv :: forall (d :: k +-> VOID) (p :: k +-> ()).
(Corepresentable d, Profunctor p) =>
((Unweighted :.: p) :~> d) -> p :~> Colimit Unweighted d
colimitUniv (Unweighted :.: p) :~> d
_ p a b
p = p a b
p p a b
-> ((Ob a, Ob b) => Corep (Constant InitialObject) a b)
-> Corep (Constant InitialObject) a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// ((Constant InitialObject @ a) ~> b)
-> Corep (Constant InitialObject) a b
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep (Constant InitialObject @ a) ~> b
InitialObject ~> b
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate

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

data family CoproductColimit :: k +-> COPRODUCT () () -> () +-> k
instance (HasBinaryCoproducts k, Corepresentable d) => FunctorForRep (CoproductColimit d :: () +-> k) where
  type CoproductColimit d @ '() = At1 d || At2 d
  fmap :: forall (a :: ()) (b :: ()).
(a ~> b) -> (CoproductColimit d @ a) ~> (CoproductColimit d @ b)
fmap a ~> b
Unit a b
Unit = forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: k +-> COPRODUCT () ()) (a :: COPRODUCT () ()) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withObCorep @d @O1 ((Ob (d %% O1) =>
  (CoproductColimit d @ a) ~> (CoproductColimit d @ b))
 -> (CoproductColimit d @ a) ~> (CoproductColimit d @ b))
-> (Ob (d %% O1) =>
    (CoproductColimit d @ a) ~> (CoproductColimit d @ b))
-> (CoproductColimit d @ a) ~> (CoproductColimit d @ b)
forall a b. (a -> b) -> a -> b
$ forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: k +-> COPRODUCT () ()) (a :: COPRODUCT () ()) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withObCorep @d @O2 ((Ob (d %% O2) =>
  (CoproductColimit d @ a) ~> (CoproductColimit d @ b))
 -> (CoproductColimit d @ a) ~> (CoproductColimit d @ b))
-> (Ob (d %% O2) =>
    (CoproductColimit d @ a) ~> (CoproductColimit d @ b))
-> (CoproductColimit d @ a) ~> (CoproductColimit d @ b)
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @(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 (HasBinaryCoproducts k) => HasColimits (Unweighted :: () +-> COPRODUCT () ()) k where
  type Colimit Unweighted d = Corep (CoproductColimit d)
  colimit :: forall (d :: k +-> COPRODUCT () ()).
Corepresentable d =>
(Unweighted :.: Colimit Unweighted d) :~> d
colimit @d (TerminalProfunctor @o :.: Corep (CoproductColimit d @ '()) ~> b
f) =
    forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: k +-> COPRODUCT () ()) (a :: COPRODUCT () ()) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withObCorep @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 {k1} {k2} (p :: k1 +-> k2) (a :: k2) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: k +-> COPRODUCT () ()) (a :: COPRODUCT () ()) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withObCorep @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
          (((d %% a) ~> b) -> d a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
forall (a :: COPRODUCT () ()) (b :: k).
Ob a =>
((d %% a) ~> b) -> d a b
cotabulate ((CoproductColimit d @ '()) ~> b
((d %% O1) || (d %% O2)) ~> b
f (((d %% O1) || (d %% O2)) ~> b)
-> ((d %% O1) ~> ((d %% O1) || (d %% O2))) -> (d %% O1) ~> 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
. forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @(At1 d) @(At2 d)))
          (((d %% a) ~> b) -> d a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
forall (a :: COPRODUCT () ()) (b :: k).
Ob a =>
((d %% a) ~> b) -> d a b
cotabulate ((CoproductColimit d @ '()) ~> b
((d %% O1) || (d %% O2)) ~> b
f (((d %% O1) || (d %% O2)) ~> b)
-> ((d %% O2) ~> ((d %% O1) || (d %% O2))) -> (d %% O2) ~> 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
. forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @(At1 d) @(At2 d)))
  colimitUniv :: forall (d :: k +-> COPRODUCT () ()) (p :: k +-> ()).
(Corepresentable d, Profunctor p) =>
((Unweighted :.: p) :~> d) -> p :~> Colimit Unweighted d
colimitUniv (Unweighted :.: p) :~> d
n p a b
p =
    p a b
p p a b
-> ((Ob a, Ob b) => Corep (CoproductColimit d) a b)
-> Corep (CoproductColimit 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 O1 b
l = (:.:) Unweighted p O1 b -> d O1 b
(Unweighted :.: p) :~> d
n (forall {j} {k} (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
forall (a :: COPRODUCT () ()) (b :: ()).
(CategoryOf (COPRODUCT () ()), CategoryOf (), Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor @O1 TerminalProfunctor O1 a -> p a b -> (:.:) Unweighted p O1 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
:.: p a b
p)
          r :: d O2 b
r = (:.:) Unweighted p O2 b -> d O2 b
(Unweighted :.: p) :~> d
n (forall {j} {k} (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
forall (a :: COPRODUCT () ()) (b :: ()).
(CategoryOf (COPRODUCT () ()), CategoryOf (), Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor @O2 TerminalProfunctor O2 a -> p a b -> (:.:) Unweighted p O2 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
:.: p a b
p)
      in ((CoproductColimit d @ a) ~> b) -> Corep (CoproductColimit d) a b
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep (((CoproductColimit d @ a) ~> b) -> Corep (CoproductColimit d) a b)
-> ((CoproductColimit d @ a) ~> b)
-> Corep (CoproductColimit d) a b
forall a b. (a -> b) -> a -> b
$ d O1 b -> (d %% O1) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
forall (a :: COPRODUCT () ()) (b :: k). d a b -> (d %% a) ~> b
coindex d O1 b
l ((d %% O1) ~> b)
-> ((d %% O2) ~> b) -> ((d %% O1) || (d %% O2)) ~> b
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| d O2 b -> (d %% O2) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
forall (a :: COPRODUCT () ()) (b :: k). d a b -> (d %% a) ~> b
coindex d O2 b
r

data family CopowerLimit :: Type -> k +-> () -> () +-> k
instance (Corepresentable d, Copowered Type k) => FunctorForRep (CopowerLimit n d :: () +-> k) where
  type CopowerLimit n d @ '() = n *. (d %% '())
  fmap :: forall (a :: ()) (b :: ()).
(a ~> b) -> (CopowerLimit n d @ a) ~> (CopowerLimit n d @ b)
fmap a ~> b
Unit a b
Unit = forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: k +-> ()) (a :: ()) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withObCorep @d @'() ((Ob (d %% '()) =>
  (CopowerLimit n d @ a) ~> (CopowerLimit n d @ b))
 -> (CopowerLimit n d @ a) ~> (CopowerLimit n d @ b))
-> (Ob (d %% '()) =>
    (CopowerLimit n d @ a) ~> (CopowerLimit n d @ b))
-> (CopowerLimit n d @ a) ~> (CopowerLimit n d @ b)
forall a b. (a -> b) -> a -> b
$ forall v k (a :: k) (n :: v) r.
(Copowered v k, Ob a, Ob n) =>
(Ob (n *. a) => r) -> r
withObCopower @Type @k @(d %% '()) @n (n *. (d %% '())) ~> (n *. (d %% '()))
Ob (n *. (d %% '())) => (n *. (d %% '())) ~> (n *. (d %% '()))
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
instance (Copowered Type k) => HasColimits (HaskValue n :: () +-> ()) k where
  type Colimit (HaskValue n) d = Corep (CopowerLimit n d)
  colimit :: forall (d :: k +-> ()).
Corepresentable d =>
(HaskValue n :.: Colimit (HaskValue n) d) :~> d
colimit @d (HaskValue n
n :.: Corep (CopowerLimit n d @ '()) ~> b
f) = forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: k +-> ()) (a :: ()) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withObCorep @d @'() ((Ob (d %% '()) => d a b) -> d a b)
-> (Ob (d %% '()) => d a b) -> d a b
forall a b. (a -> b) -> a -> b
$ ((d %% a) ~> b) -> d a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
forall (a :: ()) (b :: k). Ob a => ((d %% a) ~> b) -> d a b
cotabulate (((d %% a) ~> b) -> d a b) -> ((d %% a) ~> b) -> d a b
forall a b. (a -> b) -> a -> b
$ ((n *. (d %% '())) ~> b) -> n ~> HomObj Type (d %% '()) b
forall (a :: k) n (b :: k).
(Ob a, Ob n) =>
((n *. a) ~> b) -> n ~> HomObj Type a b
forall v k (a :: k) (n :: v) (b :: k).
(Copowered v k, Ob a, Ob n) =>
((n *. a) ~> b) -> n ~> HomObj v a b
uncopower (CopowerLimit n d @ '()) ~> b
(n *. (d %% '())) ~> b
f n
n
  colimitUniv :: forall (d :: k +-> ()) (p :: k +-> ()).
(Corepresentable d, Profunctor p) =>
((HaskValue n :.: p) :~> d) -> p :~> Colimit (HaskValue n) d
colimitUniv @d (HaskValue n :.: p) :~> d
m p a b
p = forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: k +-> ()) (a :: ()) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withObCorep @d @'() ((Ob (d %% '()) => Colimit (HaskValue n) d a b)
 -> Colimit (HaskValue n) d a b)
-> (Ob (d %% '()) => Colimit (HaskValue n) d a b)
-> Colimit (HaskValue n) d a b
forall a b. (a -> b) -> a -> b
$ ((CopowerLimit n d @ a) ~> b) -> Corep (CopowerLimit n d) a b
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep ((n ~> HomObj Type (d %% '()) b) -> (n *. (d %% '())) ~> b
forall (a :: k) (b :: k) n.
(Ob a, Ob b) =>
(n ~> HomObj Type a b) -> (n *. a) ~> b
forall v k (a :: k) (b :: k) (n :: v).
(Copowered v k, Ob a, Ob b) =>
(n ~> HomObj v a b) -> (n *. a) ~> b
copower \n
n -> d '() b -> (d %% '()) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
forall (a :: ()) (b :: k). d a b -> (d %% a) ~> b
coindex ((:.:) (HaskValue n) p '() b -> d '() b
(HaskValue n :.: p) :~> d
m (n -> HaskValue n '() a
forall {k} {j} (a :: k) (b :: j) c.
(Ob a, Ob b) =>
c -> HaskValue c a b
HaskValue n
n HaskValue n '() a -> p a b -> (:.:) (HaskValue n) p '() 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
:.: p a b
p))) ((Ob a, Ob b) => Corep (CopowerLimit n d) a b)
-> p a b -> Corep (CopowerLimit n d) a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: ()) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

data Coend d where
  Coend :: a ~> b -> d %% '(OP b, a) -> Coend d

data family CoendLimit :: Type +-> (OPPOSITE k, k) -> () +-> Type
instance (Corepresentable d) => FunctorForRep (CoendLimit (d :: Type +-> (OPPOSITE k, k))) where
  type CoendLimit d @ '() = Coend d
  fmap :: forall (a :: ()) (b :: ()).
(a ~> b) -> (CoendLimit d @ a) ~> (CoendLimit d @ b)
fmap a ~> b
Unit a b
Unit = (CoendLimit d @ a) ~> (CoendLimit d @ b)
Coend d -> Coend 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 b, a) '()
instance (CategoryOf k) => Profunctor (Hom :: () +-> (OPPOSITE k, k)) where
  dimap :: forall (c :: (OPPOSITE k, k)) (a :: (OPPOSITE k, k)) (b :: ())
       (d :: ()).
(c ~> a) -> (b ~> d) -> Hom a b -> Hom c d
dimap (Op b1 ~> a1
l :**: a2 ~> b2
r) b ~> d
Unit b d
Unit (Hom a ~> b
f) = (a2 ~> a1) -> Hom '( 'OP a1, a2) '()
forall {k} (b :: k) (b :: k). (b ~> b) -> Hom '( 'OP b, b) '()
Hom (b1 ~> a1
l (b1 ~> a1) -> (a2 ~> b1) -> a2 ~> a1
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
. b2 ~> b1
a ~> b
f (b2 ~> b1) -> (a2 ~> b2) -> a2 ~> b1
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
. a2 ~> b2
r) ((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 :: (OPPOSITE k, k)) (b :: ()) 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) => HasColimits (Hom :: () +-> (OPPOSITE k, k)) Type where
  type Colimit Hom d = Corep (CoendLimit d)
  colimit :: forall (d :: Type +-> (OPPOSITE k, k)).
Corepresentable d =>
(Hom :.: Colimit Hom d) :~> d
colimit (Hom a ~> b
f :.: Corep (CoendLimit d @ '()) ~> b
g) = a ~> b
f (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
// ((d %% a) ~> b) -> d a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
forall (a :: (OPPOSITE k, k)) b. Ob a => ((d %% a) ~> b) -> d a b
cotabulate (\d %% '( 'OP b, a)
d -> (CoendLimit d @ '()) ~> b
Coend d -> b
g ((a ~> b) -> (d %% '( 'OP b, a)) -> Coend d
forall {k} (b :: k) (b :: k) (d :: Type +-> (OPPOSITE k, k)).
(b ~> b) -> (d %% '( 'OP b, b)) -> Coend d
Coend a ~> b
f d %% '( 'OP b, a)
d))
  colimitUniv :: forall (d :: Type +-> (OPPOSITE k, k)) (p :: Type +-> ()).
(Corepresentable d, Profunctor p) =>
((Hom :.: p) :~> d) -> p :~> Colimit Hom d
colimitUniv (Hom :.: p) :~> d
n p a b
p = p a b
p p a b
-> ((Ob a, Ob b) => Corep (CoendLimit d) a b)
-> Corep (CoendLimit 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
// ((CoendLimit d @ a) ~> b) -> Corep (CoendLimit d) a b
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep \(Coend a ~> b
f d %% '( 'OP b, a)
d) -> d '( 'OP b, a) b -> (d %% '( 'OP b, a)) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
forall (a :: (OPPOSITE k, k)) b. d a b -> (d %% a) ~> b
coindex ((:.:) Hom p '( 'OP b, a) b -> d '( 'OP b, a) b
(Hom :.: p) :~> d
n ((a ~> b) -> Hom '( 'OP b, a) '()
forall {k} (b :: k) (b :: k). (b ~> b) -> Hom '( 'OP b, b) '()
Hom a ~> b
f Hom '( 'OP b, a) '() -> p '() b -> (:.:) Hom p '( 'OP b, 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
:.: p a b
p '() b
p)) d %% '( 'OP b, a)
d

instance (CategoryOf j) => HasColimits (Id :: CAT j) k where
  type Colimit Id d = d
  colimit :: forall (d :: k +-> j).
Corepresentable d =>
(Id :.: Colimit Id d) :~> d
colimit (Id a ~> b
f :.: Colimit Id d b b
d) = (a ~> b) -> d b b -> d a b
forall (c :: j) (a :: j) (b :: k). (c ~> a) -> d a b -> d 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 d b b
Colimit Id d b b
d
  colimitUniv :: forall (d :: k +-> j) (p :: k +-> j).
(Corepresentable d, Profunctor p) =>
((Id :.: p) :~> d) -> p :~> Colimit Id d
colimitUniv (Id :.: p) :~> d
n p a b
p = (:.:) Id p a b -> d a b
(Id :.: p) :~> d
n ((a ~> a) -> Id a a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a ~> a
forall (a :: j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id Id a a -> p a b -> (:.:) Id p 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
:.: p a b
p) ((Ob a, Ob b) => d a b) -> p a b -> d a b
forall (a :: j) (b :: k) 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 (Corepresentable j2, HasColimits j1 k, HasColimits j2 k) => HasColimits (j1 :.: j2) k where
  type Colimit (j1 :.: j2) d = Colimit j2 (Colimit j1 d)
  colimit :: forall (d :: k +-> i).
Corepresentable d =>
((j1 :.: j2) :.: Colimit (j1 :.: j2) d) :~> d
colimit @d ((j1 a b
j1 :.: j2 b b
j2) :.: Colimit (j1 :.: j2) d b b
c) = forall {i} {a} (j :: a +-> i) k (d :: k +-> i).
(HasColimits j k, Corepresentable d) =>
(j :.: Colimit j d) :~> d
forall (j :: j +-> i) k (d :: k +-> i).
(HasColimits j k, Corepresentable d) =>
(j :.: Colimit j d) :~> d
colimit @j1 @k @d (j1 a b
j1 j1 a b -> Colimit j1 d b b -> (:.:) j1 (Colimit j1 d) 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
:.: forall {i} {a} (j :: a +-> i) k (d :: k +-> i).
(HasColimits j k, Corepresentable d) =>
(j :.: Colimit j d) :~> d
forall (j :: a +-> j) k (d :: k +-> j).
(HasColimits j k, Corepresentable d) =>
(j :.: Colimit j d) :~> d
colimit @j2 @k @(Colimit j1 d) (j2 b b
j2 j2 b b
-> Colimit j2 (Colimit j1 d) b b
-> (:.:) j2 (Colimit j2 (Colimit j1 d)) 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
:.: Colimit j2 (Colimit j1 d) b b
Colimit (j1 :.: j2) d b b
c))
  colimitUniv :: forall (d :: k +-> i) (p :: k +-> a).
(Corepresentable d, Profunctor p) =>
(((j1 :.: j2) :.: p) :~> d) -> p :~> Colimit (j1 :.: j2) d
colimitUniv @d ((j1 :.: j2) :.: p) :~> d
n = forall {i} {a} (j :: a +-> i) k (d :: k +-> i) (p :: k +-> a).
(HasColimits j k, Corepresentable d, Profunctor p) =>
((j :.: p) :~> d) -> p :~> Colimit j d
forall (j :: a +-> j) k (d :: k +-> j) (p :: k +-> a).
(HasColimits j k, Corepresentable d, Profunctor p) =>
((j :.: p) :~> d) -> p :~> Colimit j d
colimitUniv @j2 @k @(Colimit j1 d) (forall {i} {a} (j :: a +-> i) k (d :: k +-> i) (p :: k +-> a).
(HasColimits j k, Corepresentable d, Profunctor p) =>
((j :.: p) :~> d) -> p :~> Colimit j d
forall (j :: j +-> i) k (d :: k +-> i) (p :: k +-> j).
(HasColimits j k, Corepresentable d, Profunctor p) =>
((j :.: p) :~> d) -> p :~> Colimit j d
colimitUniv @j1 @k @d (\(j1 a b
j1 :.: (j2 b b
j2 :.: p b b
p')) -> (:.:) (j1 :.: j2) p a b -> d a b
((j1 :.: j2) :.: p) :~> d
n ((j1 a b
j1 j1 a b -> j2 b b -> (:.:) 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
:.: j2 b b
j2) (:.:) j1 j2 a b -> p b b -> (:.:) (j1 :.: j2) p 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
:.: p b b
p')))

instance (FunctorForRep f) => HasColimits (Rep f) k where
  type Colimit (Rep f) d = Corep f :.: d
  colimit :: forall (d :: k +-> i).
Corepresentable d =>
(Rep f :.: Colimit (Rep f) d) :~> d
colimit (Rep a ~> (f @ b)
f :.: (Corep (f @ b) ~> b
g :.: d b b
d)) = (a ~> b) -> d b b -> d a b
forall (c :: i) (a :: i) (b :: k). (c ~> a) -> d a b -> d 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 ((f @ b) ~> b
g ((f @ b) ~> b) -> (a ~> (f @ b)) -> a ~> 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
. a ~> (f @ b)
f) d b b
d
  colimitUniv :: forall (d :: k +-> i) (p :: k +-> a).
(Corepresentable d, Profunctor p) =>
((Rep f :.: p) :~> d) -> p :~> Colimit (Rep f) d
colimitUniv (Rep f :.: p) :~> d
n p a b
p = p a b
p p a b
-> ((Ob a, Ob b) => (:.:) (Corep f) d a b) -> (:.:) (Corep f) 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
// Corep f a (f @ a)
Corep f a (Corep f %% a)
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 Corep f a (f @ a) -> d (f @ a) b -> (:.:) (Corep f) d 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) p (f @ a) b -> d (f @ a) b
(Rep f :.: p) :~> d
n (Rep f (f @ a) a
Rep f (Rep f % a) a
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 Rep f (f @ a) a -> p a b -> (:.:) (Rep f) p (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
:.: p a b
p)

newtype AnyColimit j a b = AnyColimit (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) -> AnyColimit j a b -> AnyColimit j c d)
-> (forall (c :: k) (a :: k) (b :: j).
    (c ~> a) -> AnyColimit j a b -> AnyColimit j c b)
-> (forall (b :: j) (d :: j) (a :: k).
    (b ~> d) -> AnyColimit j a b -> AnyColimit j a d)
-> (forall (a :: k) (b :: j) r.
    ((Ob a, Ob b) => r) -> AnyColimit j a b -> r)
-> Profunctor (AnyColimit j)
forall (c :: k) (a :: k) (b :: j).
(c ~> a) -> AnyColimit j a b -> AnyColimit j c b
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> AnyColimit j a b -> AnyColimit j c d
forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> AnyColimit j a b -> r
forall (b :: j) (d :: j) (a :: k).
(b ~> d) -> AnyColimit j a b -> AnyColimit 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) -> AnyColimit j a b -> AnyColimit j c b
forall k j (j :: k -> j -> Type) (c :: k) (a :: k) (b :: j)
       (d :: j).
Profunctor j =>
(c ~> a) -> (b ~> d) -> AnyColimit j a b -> AnyColimit j c d
forall k j (j :: k -> j -> Type) (a :: k) (b :: j) r.
Profunctor j =>
((Ob a, Ob b) => r) -> AnyColimit j a b -> r
forall k j (j :: k -> j -> Type) (b :: j) (d :: j) (a :: k).
Profunctor j =>
(b ~> d) -> AnyColimit j a b -> AnyColimit 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) -> AnyColimit j a b -> AnyColimit j c d
dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> AnyColimit j a b -> AnyColimit j c d
$clmap :: forall k j (j :: k -> j -> Type) (c :: k) (a :: k) (b :: j).
Profunctor j =>
(c ~> a) -> AnyColimit j a b -> AnyColimit j c b
lmap :: forall (c :: k) (a :: k) (b :: j).
(c ~> a) -> AnyColimit j a b -> AnyColimit j c b
$crmap :: forall k j (j :: k -> j -> Type) (b :: j) (d :: j) (a :: k).
Profunctor j =>
(b ~> d) -> AnyColimit j a b -> AnyColimit j a d
rmap :: forall (b :: j) (d :: j) (a :: k).
(b ~> d) -> AnyColimit j a b -> AnyColimit j a d
$c\\ :: forall k j (j :: k -> j -> Type) (a :: k) (b :: j) r.
Profunctor j =>
((Ob a, Ob b) => r) -> AnyColimit j a b -> r
\\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> AnyColimit j a b -> r
Profunctor)
type Lan :: (a +-> i) -> (Type +-> i) -> a -> Type
data Lan j d a where
  Lan :: j b a -> d %% b -> Lan j d a
instance (Profunctor j, Corepresentable d) => Functor (Lan j d) where
  map :: forall (a :: k1) (b :: k1). (a ~> b) -> Lan j d a ~> Lan j d b
map a ~> b
f (Lan j b a
j d %% b
d) = j b b -> (d %% b) -> Lan j d b
forall {a} {k} (j :: a +-> k) (b :: k) (a :: a) (d :: Type +-> k).
j b a -> (d %% b) -> Lan j d a
Lan ((a ~> b) -> j b a -> j b b
forall (b :: k1) (d :: k1) (a :: i). (b ~> d) -> j a b -> j 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 a ~> b
f j b a
j) d %% b
d
instance (Profunctor j) => HasColimits (AnyColimit j) Type where
  type Colimit (AnyColimit j) d = Costar (Lan j d)
  colimit :: forall (d :: Type +-> i).
Corepresentable d =>
(AnyColimit j :.: Colimit (AnyColimit j) d) :~> d
colimit (AnyColimit j a b
j :.: Costar Lan j d b ~> b
f) = ((d %% a) ~> b) -> d a b
forall (a :: i) b. Ob a => ((d %% a) ~> b) -> d a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate (\d %% a
db -> Lan j d b ~> b
Lan j d b -> b
f (j a b -> (d %% a) -> Lan j d b
forall {a} {k} (j :: a +-> k) (b :: k) (a :: a) (d :: Type +-> k).
j b a -> (d %% b) -> Lan j d a
Lan j a b
j d %% a
db)) ((Ob a, Ob b) => d a b) -> j a b -> d a b
forall (a :: i) (b :: a) 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 a b
j
  colimitUniv :: forall (d :: Type +-> i) (p :: Type +-> a).
(Corepresentable d, Profunctor p) =>
((AnyColimit j :.: p) :~> d) -> p :~> Colimit (AnyColimit j) d
colimitUniv (AnyColimit j :.: p) :~> d
n p a b
p = p a b
p p a b
-> ((Ob a, Ob b) => Costar' ('OP ('NT (Lan j d))) a b)
-> Costar' ('OP ('NT (Lan 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
// (Lan j d a ~> b) -> Costar' ('OP ('NT (Lan j d))) a b
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar (\(Lan j b a
j d %% b
db) -> d b b -> (d %% b) ~> b
forall (a :: i) b. d a b -> (d %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex ((:.:) (AnyColimit j) p b b -> d b b
(AnyColimit j :.: p) :~> d
n (j b a -> AnyColimit j b a
forall {k} {k} (j :: k -> k -> Type) (a :: k) (b :: k).
j a b -> AnyColimit j a b
AnyColimit j b a
j AnyColimit j b a -> p a b -> (:.:) (AnyColimit j) p 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
:.: p a b
p)) d %% b
db)