{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Colimit where

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

import Proarrow.Adjunction (Adjunction (..))
import Proarrow.Category.Instance.Coproduct (COPRODUCT (..), type (:++:) (..))
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, src)
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..), lft, rgt)
import Proarrow.Object.Copower (Copowered (..))
import Proarrow.Object.Initial (HasInitialObject (..), initiate)
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), corepObj, dimapCorep, withCorepOb)
import Proarrow.Profunctor.HaskValue (HaskValue (..))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Terminal (TerminalProfunctor (TerminalProfunctor'))
import Proarrow.Profunctor.Wrapped (Wrapped (..))
import Proarrow.Profunctor.Representable

type Unweighted = TerminalProfunctor

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

-- | profunctor-weighted colimits
type HasColimits :: forall {i} {a}. a +-> i -> Kind -> Constraint
class
  (Profunctor j, forall (d :: k +-> i). (Corepresentable d) => IsCorepresentableColimit 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

leftAdjointPreservesColimits
  :: forall {k} {k'} {i} {a} (f :: k' +-> k) g (d :: k +-> i) (j :: a +-> i)
   . (Adjunction f g, Corepresentable d, Corepresentable f, HasColimits j k, HasColimits j k')
  => Colimit j (d :.: f) :~> Colimit j d :.: f
leftAdjointPreservesColimits :: forall {k} {k'} {i} {a} (f :: k' +-> k) (g :: k +-> k')
       (d :: k +-> i) (j :: a +-> i).
(Adjunction f g, Corepresentable d, Corepresentable f,
 HasColimits j k, HasColimits j k') =>
Colimit j (d :.: f) :~> (Colimit j d :.: f)
leftAdjointPreservesColimits Colimit j (d :.: f) a b
colim =
  Colimit j (d :.: f) a b
colim Colimit j (d :.: f) a b
-> ((Ob a, Ob b) => (:.:) (Colimit j d) f a b)
-> (:.:) (Colimit j d) f a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// 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 b b
g :.: f b b
f ->
      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 @k @d
        (\(j a b
j :.: (Colimit j (d :.: f) b b
colim' :.: g b b
g')) -> case 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 @k' @(d :.: f) (j a b
j j a b
-> Colimit j (d :.: f) b b -> (:.:) j (Colimit j (d :.: f)) 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
:.: Colimit j (d :.: f) b b
colim') of d a b
d :.: f 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 ((:.:) f g b b -> b ~> b
(f :.: g) :~> (~>)
forall {j} {k} (p :: j +-> k) (q :: k +-> j).
Adjunction p q =>
(p :.: q) :~> (~>)
counit (f b b
f' f b b -> g b b -> (:.:) f g 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
:.: g b b
g')) d a b
d)
        (Colimit j (d :.: f) a b
colim Colimit j (d :.: f) a b
-> g b b -> (:.:) (Colimit j (d :.: 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)
        Colimit j d a b -> f b b -> (:.:) (Colimit j d) f 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
:.: f b b
f

leftAdjointPreservesColimitsInv
  :: forall {k} {k'} {i} {a} (f :: k' +-> k) (d :: k +-> i) (j :: a +-> i)
   . (Corepresentable d, Corepresentable f, HasColimits j k, HasColimits j k')
  => Colimit j d :.: f :~> Colimit j (d :.: f)
leftAdjointPreservesColimitsInv :: forall {k} {k'} {i} {a} (f :: k' +-> k) (d :: k +-> i)
       (j :: a +-> i).
(Corepresentable d, Corepresentable f, HasColimits j k,
 HasColimits j k') =>
(Colimit j d :.: f) :~> Colimit j (d :.: f)
leftAdjointPreservesColimitsInv = 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 @k' @(d :.: f) (\(j a b
j :.: (Colimit j d b b
colim :.: f b b
f)) -> (:.:) j (Colimit j d) a b -> d a b
(j :.: Colimit j d) :~> d
forall {i} {a} (j :: a +-> i) k (d :: k +-> i).
(HasColimits j k, Corepresentable d) =>
(j :.: Colimit j d) :~> d
forall (d :: k +-> i).
Corepresentable d =>
(j :.: Colimit j d) :~> d
colimit (j a b
j j a b -> Colimit j d b b -> (:.:) j (Colimit 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
:.: Colimit j d b b
colim) d a b -> f b b -> (:.:) d f 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
:.: f b b
f)

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

instance (HasInitialObject k) => Profunctor (InitialLimit (d :: k +-> VOID)) where
  dimap :: forall (c :: ()) (a :: ()) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> InitialLimit d a b -> InitialLimit d c d
dimap = (c ~> a) -> (b ~> d) -> InitialLimit d a b -> InitialLimit d c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Corepresentable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapCorep
  (Ob a, Ob b) => r
r \\ :: forall (a :: ()) (b :: k) r.
((Ob a, Ob b) => r) -> InitialLimit d a b -> r
\\ InitialLimit InitialObject ~> b
f = r
(Ob InitialObject, Ob b) => r
(Ob a, Ob b) => r
r ((Ob InitialObject, Ob b) => r) -> (InitialObject ~> 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
\\ InitialObject ~> b
f
instance (HasInitialObject k) => Corepresentable (InitialLimit (d :: k +-> VOID)) where
  type InitialLimit d %% '() = InitialObject
  coindex :: forall (a :: ()) (b :: k).
InitialLimit d a b -> (InitialLimit d %% a) ~> b
coindex (InitialLimit InitialObject ~> b
f) = (InitialLimit d %% a) ~> b
InitialObject ~> b
f
  cotabulate :: forall (a :: ()) (b :: k).
Ob a =>
((InitialLimit d %% a) ~> b) -> InitialLimit d a b
cotabulate = ((InitialLimit d %% a) ~> b) -> InitialLimit d a b
(InitialObject ~> b) -> InitialLimit d '() b
forall {k} (d :: k +-> VOID) (a :: k).
(InitialObject ~> a) -> InitialLimit d '() a
InitialLimit
  corepMap :: forall (a :: ()) (b :: ()).
(a ~> b) -> (InitialLimit d %% a) ~> (InitialLimit d %% b)
corepMap a ~> b
Unit a b
Unit = (InitialLimit d %% a) ~> (InitialLimit d %% b)
InitialObject ~> InitialObject
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
instance (HasInitialObject k) => HasColimits (Unweighted :: () +-> VOID) k where
  type Colimit Unweighted d = InitialLimit d
  colimit :: forall (d :: k +-> VOID).
Corepresentable d =>
(Unweighted :.: Colimit Unweighted d) :~> d
colimit = \case {}
  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) => InitialLimit d a b) -> InitialLimit 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
// (InitialObject ~> b) -> InitialLimit d '() b
forall {k} (d :: k +-> VOID) (a :: k).
(InitialObject ~> a) -> InitialLimit d '() a
InitialLimit InitialObject ~> b
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate

type CoproductColimit :: k +-> COPRODUCT () () -> k +-> ()
data CoproductColimit d a b where
  CoproductColimit :: forall d b. ((d %% L '()) || (d %% R '())) ~> b -> CoproductColimit d '() b

instance (CategoryOf k) => Profunctor (CoproductColimit d :: k +-> ()) where
  dimap :: forall (c :: ()) (a :: ()) (b :: k) (d :: k).
(c ~> a)
-> (b ~> d) -> CoproductColimit d a b -> CoproductColimit d c d
dimap c ~> a
Unit c a
Unit b ~> d
r (CoproductColimit ((d %% L '()) || (d %% R '())) ~> b
f) = (((d %% L '()) || (d %% R '())) ~> d) -> CoproductColimit d '() d
forall {k} (d :: k +-> COPRODUCT () ()) (b :: k).
(((d %% L '()) || (d %% R '())) ~> b) -> CoproductColimit d '() b
CoproductColimit (b ~> d
r (b ~> d)
-> (((d %% L '()) || (d %% R '())) ~> b)
-> ((d %% L '()) || (d %% R '())) ~> d
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
. ((d %% L '()) || (d %% R '())) ~> b
f) ((Ob b, Ob d) => CoproductColimit d c d)
-> (b ~> d) -> CoproductColimit d 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
\\ b ~> d
r
  (Ob a, Ob b) => r
r \\ :: forall (a :: ()) (b :: k) r.
((Ob a, Ob b) => r) -> CoproductColimit d a b -> r
\\ (CoproductColimit ((d %% L '()) || (d %% R '())) ~> b
f) = r
(Ob ((d %% L '()) || (d %% R '())), Ob b) => r
(Ob a, Ob b) => r
r ((Ob ((d %% L '()) || (d %% R '())), Ob b) => r)
-> (((d %% L '()) || (d %% R '())) ~> 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
\\ ((d %% L '()) || (d %% R '())) ~> b
f

instance (HasBinaryCoproducts k, Corepresentable d) => Corepresentable (CoproductColimit d :: k +-> ()) where
  type CoproductColimit d %% '() = (d %% L '()) || (d %% R '())
  coindex :: forall (a :: ()) (b :: k).
CoproductColimit d a b -> (CoproductColimit d %% a) ~> b
coindex (CoproductColimit ((d %% L '()) || (d %% R '())) ~> b
f) = (CoproductColimit d %% a) ~> b
((d %% L '()) || (d %% R '())) ~> b
f
  cotabulate :: forall (a :: ()) (b :: k).
Ob a =>
((CoproductColimit d %% a) ~> b) -> CoproductColimit d a b
cotabulate = ((CoproductColimit d %% a) ~> b) -> CoproductColimit d a b
(((d %% L '()) || (d %% R '())) ~> b) -> CoproductColimit d '() b
forall {k} (d :: k +-> COPRODUCT () ()) (b :: k).
(((d %% L '()) || (d %% R '())) ~> b) -> CoproductColimit d '() b
CoproductColimit
  corepMap :: forall (a :: ()) (b :: ()).
(a ~> b) -> (CoproductColimit d %% a) ~> (CoproductColimit d %% b)
corepMap a ~> b
Unit a b
Unit = forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryCoproducts k =>
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
(+++) @_ @(d %% L '()) @(d %% R '()) (forall {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: k +-> COPRODUCT () ()) (a :: COPRODUCT () ())
       (b :: COPRODUCT () ()).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @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 :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: k +-> COPRODUCT () ()) (a :: COPRODUCT () ())
       (b :: COPRODUCT () ()).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @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 (HasBinaryCoproducts k) => HasColimits (Unweighted :: () +-> COPRODUCT () ()) k where
  type Colimit Unweighted d = CoproductColimit d
  colimit :: forall (d :: k +-> COPRODUCT () ()).
Corepresentable d =>
(Unweighted :.: Colimit Unweighted d) :~> d
colimit (TerminalProfunctor' Obj a
o Obj b
_ :.: CoproductColimit @d ((d %% L '()) || (d %% R '())) ~> b
f) = Obj a
(:++:) Unit Unit a a
o (:++:) Unit Unit a a -> ((Ob a, Ob a) => 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 :: COPRODUCT () ()) (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
$ ((d %% L '()) || (d %% R '())) ~> b
f (((d %% L '()) || (d %% R '())) ~> b)
-> ((d %% a) ~> ((d %% L '()) || (d %% R '()))) -> (d %% a) ~> 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 (d :: k +-> COPRODUCT () ()) (b :: COPRODUCT () ()).
(HasBinaryCoproducts k, Corepresentable d) =>
Obj b -> (d %% b) ~> ((d %% L '()) || (d %% R '()))
cochoose @_ @d Obj a
o
  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) => CoproductColimit d a b)
-> 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 (L '()) b
l = (:.:) Unweighted p (L '()) b -> d (L '()) b
(Unweighted :.: p) :~> d
n ((L '() ~> L '()) -> Obj a -> TerminalProfunctor (L '()) a
forall k (a :: k) j (b :: j).
Obj a -> Obj b -> TerminalProfunctor a b
TerminalProfunctor' (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) Obj a
Unit '() '()
Unit TerminalProfunctor (L '()) a
-> p a b -> (:.:) Unweighted p (L '()) 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
:.: p a b
p)
          r :: d (R '()) b
r = (:.:) Unweighted p (R '()) b -> d (R '()) b
(Unweighted :.: p) :~> d
n ((R '() ~> R '()) -> Obj a -> TerminalProfunctor (R '()) a
forall k (a :: k) j (b :: j).
Obj a -> Obj b -> TerminalProfunctor a b
TerminalProfunctor' (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) Obj a
Unit '() '()
Unit TerminalProfunctor (R '()) a
-> p a b -> (:.:) Unweighted p (R '()) 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
:.: p a b
p)
      in (((d %% L '()) || (d %% R '())) ~> b) -> CoproductColimit d '() b
forall {k} (d :: k +-> COPRODUCT () ()) (b :: k).
(((d %% L '()) || (d %% R '())) ~> b) -> CoproductColimit d '() b
CoproductColimit ((((d %% L '()) || (d %% R '())) ~> b) -> CoproductColimit d '() b)
-> (((d %% L '()) || (d %% R '())) ~> b)
-> CoproductColimit d '() b
forall a b. (a -> b) -> a -> b
$ d (L '()) b -> (d %% L '()) ~> 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 (L '()) b
l ((d %% L '()) ~> b)
-> ((d %% R '()) ~> b) -> ((d %% L '()) || (d %% R '())) ~> 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 (R '()) b -> (d %% R '()) ~> 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 (R '()) b
r

cochoose
  :: forall k (d :: k +-> COPRODUCT () ()) b
   . (HasBinaryCoproducts k, Corepresentable d)
  => Obj b
  -> (d %% b) ~> ((d %% L '()) || (d %% R '()))
cochoose :: forall k (d :: k +-> COPRODUCT () ()) (b :: COPRODUCT () ()).
(HasBinaryCoproducts k, Corepresentable d) =>
Obj b -> (d %% b) ~> ((d %% L '()) || (d %% R '()))
cochoose Obj b
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
withCorepOb @d @(L '()) ((Ob (d %% L '()) => (d %% b) ~> ((d %% L '()) || (d %% R '())))
 -> (d %% b) ~> ((d %% L '()) || (d %% R '())))
-> (Ob (d %% L '()) => (d %% b) ~> ((d %% L '()) || (d %% R '())))
-> (d %% b) ~> ((d %% L '()) || (d %% R '()))
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
withCorepOb @d @(R '()) ((Ob (d %% R '()) => (d %% b) ~> ((d %% L '()) || (d %% R '())))
 -> (d %% b) ~> ((d %% L '()) || (d %% R '())))
-> (Ob (d %% R '()) => (d %% b) ~> ((d %% L '()) || (d %% R '())))
-> (d %% b) ~> ((d %% L '()) || (d %% R '()))
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).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @(d %% L '()) @(d %% R '())
  (InjR Unit a1 b1
Unit b1 b1
Unit) -> forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @(d %% L '()) @(d %% R '())

type CopowerLimit :: Type -> k +-> () -> k +-> ()
data CopowerLimit n d a b where
  CopowerLimit :: forall n d b. (Ob n) => (CopowerLimit n d %% '() ~> b) -> CopowerLimit n d '() b
instance (Corepresentable d, Copowered Type k) => Profunctor (CopowerLimit n d :: k +-> ()) where
  dimap :: forall (c :: ()) (a :: ()) (b :: k) (d :: k).
(c ~> a)
-> (b ~> d) -> CopowerLimit n d a b -> CopowerLimit n d c d
dimap = (c ~> a)
-> (b ~> d) -> CopowerLimit n d a b -> CopowerLimit n d c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Corepresentable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapCorep
  (Ob a, Ob b) => r
r \\ :: forall (a :: ()) (b :: k) r.
((Ob a, Ob b) => r) -> CopowerLimit n d a b -> r
\\ CopowerLimit (CopowerLimit n d %% '()) ~> b
f = r
(Ob (n *. (d %% '())), Ob b) => r
(Ob a, Ob b) => r
r ((Ob (n *. (d %% '())), Ob b) => r)
-> ((n *. (d %% '())) ~> 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
\\ (CopowerLimit n d %% '()) ~> b
(n *. (d %% '())) ~> b
f
instance (Corepresentable d, Copowered Type k) => Corepresentable (CopowerLimit n d :: k +-> ()) where
  type CopowerLimit n d %% '() = n *. (d %% '())
  coindex :: forall (a :: ()) (b :: k).
CopowerLimit n d a b -> (CopowerLimit n d %% a) ~> b
coindex (CopowerLimit (CopowerLimit n d %% '()) ~> b
f) = (CopowerLimit n d %% a) ~> b
(CopowerLimit n d %% '()) ~> b
f
  cotabulate :: forall (a :: ()) (b :: k).
Ob a =>
((CopowerLimit n d %% a) ~> b) -> CopowerLimit n d a b
cotabulate = ((CopowerLimit n d %% a) ~> b) -> CopowerLimit n d a b
((CopowerLimit n d %% '()) ~> b) -> CopowerLimit n d '() b
forall {k} n (d :: k +-> ()) (b :: k).
Ob n =>
((CopowerLimit n d %% '()) ~> b) -> CopowerLimit n d '() b
CopowerLimit
  corepMap :: forall (a :: ()) (b :: ()).
(a ~> b) -> (CopowerLimit n d %% a) ~> (CopowerLimit n d %% b)
corepMap a ~> b
Unit a b
Unit = 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 ((Ob (d %% '()), Ob (d %% '())) =>
 (n *. (d %% '())) ~> (n *. (d %% '())))
-> ((d %% '()) ~> (d %% '()))
-> (n *. (d %% '())) ~> (n *. (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
\\ forall {k1} {k2} (p :: k1 +-> k2) (a :: k2).
(Corepresentable p, Ob a) =>
Obj (p %% a)
forall (p :: k +-> ()) (a :: ()).
(Corepresentable p, Ob a) =>
Obj (p %% a)
corepObj @d @'()
instance (Copowered Type k) => HasColimits (HaskValue n :: () +-> ()) k where
  type Colimit (HaskValue n) d = CopowerLimit n d
  colimit :: forall (d :: k +-> ()).
Corepresentable d =>
(HaskValue n :.: Colimit (HaskValue n) d) :~> d
colimit @d (HaskValue n
n :.: CopowerLimit (CopowerLimit n d %% '()) ~> b
f) = ((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 (((n *. (d %% '())) ~> b) -> n ~> ProObj 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) ((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 {k1} {k2} (p :: k1 +-> k2) (a :: k2).
(Corepresentable p, Ob a) =>
Obj (p %% a)
forall (p :: k +-> ()) (a :: ()).
(Corepresentable p, Ob a) =>
Obj (p %% a)
corepObj @d @'()
  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 = ((CopowerLimit n d %% '()) ~> b) -> CopowerLimit n d '() b
forall {k} n (d :: k +-> ()) (b :: k).
Ob n =>
((CopowerLimit n d %% '()) ~> b) -> CopowerLimit n d '() b
CopowerLimit ((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} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p a b
p))) ((Ob a, Ob b) => CopowerLimit n d a b)
-> p a b -> 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 ((Ob (d %% '()), Ob (d %% '())) => CopowerLimit n d a b)
-> ((d %% '()) ~> (d %% '())) -> CopowerLimit 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 {k1} {k2} (p :: k1 +-> k2) (a :: k2).
(Corepresentable p, Ob a) =>
Obj (p %% a)
forall (p :: k +-> ()) (a :: ()).
(Corepresentable p, Ob a) =>
Obj (p %% a)
corepObj @d @'()

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

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

instance (Corepresentable d) => Profunctor (CoendLimit (d :: Type +-> (OPPOSITE k, k))) where
  dimap :: forall (c :: ()) (a :: ()) b d.
(c ~> a) -> (b ~> d) -> CoendLimit d a b -> CoendLimit d c d
dimap = (c ~> a) -> (b ~> d) -> CoendLimit d a b -> CoendLimit d c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Corepresentable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapCorep
  (Ob a, Ob b) => r
r \\ :: forall (a :: ()) b r. ((Ob a, Ob b) => r) -> CoendLimit d a b -> r
\\ CoendLimit Coend d -> b
f = r
(Ob (Coend d), Ob b) => r
(Ob a, Ob b) => r
r ((Ob (Coend d), Ob b) => r) -> (Coend d -> b) -> r
forall a b 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
\\ Coend d -> b
f
instance (Corepresentable d) => Corepresentable (CoendLimit (d :: Type +-> (OPPOSITE k, k))) where
  type CoendLimit d %% '() = Coend d
  coindex :: forall (a :: ()) b. CoendLimit d a b -> (CoendLimit d %% a) ~> b
coindex (CoendLimit Coend d -> b
f) = (CoendLimit d %% a) ~> b
Coend d -> b
f
  cotabulate :: forall (a :: ()) b.
Ob a =>
((CoendLimit d %% a) ~> b) -> CoendLimit d a b
cotabulate = ((CoendLimit d %% a) ~> b) -> CoendLimit d a b
(Coend d -> b) -> CoendLimit d '() b
forall {k} (d :: Type +-> (OPPOSITE k, k)) b.
(Coend d -> b) -> CoendLimit d '() b
CoendLimit
  corepMap :: forall (a :: ()) (b :: ()).
(a ~> b) -> (CoendLimit d %% a) ~> (CoendLimit d %% b)
corepMap 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} (a :: k) (b :: k). (a ~> b) -> Hom '( 'OP b, a) '()
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 = CoendLimit d
  colimit :: forall (d :: Type +-> (OPPOSITE k, k)).
Corepresentable d =>
(Hom :.: Colimit Hom d) :~> d
colimit (Hom a ~> b
f :.: CoendLimit Coend 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 -> Coend d -> b
g ((a ~> b) -> (d %% '( 'OP b, a)) -> Coend d
forall {k} (a :: k) (b :: k) (d :: Type +-> (OPPOSITE k, k)).
(a ~> b) -> (d %% '( 'OP b, a)) -> 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) => CoendLimit d a b) -> 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
// (Coend d -> b) -> CoendLimit d '() b
forall {k} (d :: Type +-> (OPPOSITE k, k)) b.
(Coend d -> b) -> CoendLimit d '() b
CoendLimit \(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} (a :: k) (b :: k). (a ~> b) -> Hom '( 'OP b, a) '()
Hom a ~> b
f Hom '( 'OP b, a) '() -> p '() b -> (:.:) Hom p '( 'OP b, 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
:.: 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 {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} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
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} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
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} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
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} (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) (:.:) j1 j2 a b -> p b b -> (:.:) (j1 :.: j2) p 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
:.: p b b
p')))

instance (Representable j) => HasColimits (Wrapped j) k where
  type Colimit (Wrapped j) d = RepCostar j :.: d
  colimit :: forall (d :: k +-> i).
Corepresentable d =>
(Wrapped j :.: Colimit (Wrapped j) d) :~> d
colimit (Wrapped j a b
j :.: (RepCostar (j % 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 ((j % b) ~> b
g ((j % b) ~> b) -> (a ~> (j % 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
. Wrapped j a b -> a ~> (Wrapped j % b)
forall (a :: i) (b :: a). Wrapped j a b -> a ~> (Wrapped j % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index Wrapped j a b
j) d b b
d
  colimitUniv :: forall (d :: k +-> i) (p :: k +-> a).
(Corepresentable d, Profunctor p) =>
((Wrapped j :.: p) :~> d) -> p :~> Colimit (Wrapped j) d
colimitUniv (Wrapped j :.: p) :~> d
n p a b
p = p a b
p p a b
-> ((Ob a, Ob b) => (:.:) (RepCostar j) d a b)
-> (:.:) (RepCostar 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
// ((j % a) ~> (j % a)) -> RepCostar j a (j % a)
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: a +-> i) (a :: a) (b :: a).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @j (p a b -> a ~> a
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src p a b
p)) RepCostar j a (j % a) -> d (j % a) b -> (:.:) (RepCostar 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
:.: (:.:) (Wrapped j) p (j % a) b -> d (j % a) b
(Wrapped j :.: p) :~> d
n (Wrapped j (j % a) a
Wrapped j (Wrapped j % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
trivialRep Wrapped j (j % a) a -> p a b -> (:.:) (Wrapped j) p (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
:.: p a b
p)