{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Colimit where

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

import Proarrow.Adjunction (Adjunction (..), unit')
import Proarrow.Category.Instance.Coproduct (COPRODUCT (..), (:++:) (..))
import Proarrow.Category.Instance.Unit (Unit (..))
import Proarrow.Category.Instance.Zero (VOID)
import Proarrow.Core (CategoryOf (..), Kind, Profunctor (..), Promonad (..), lmap, src, (//), (:~>), type (+->))
import Proarrow.Object (Obj)
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.HaskValue (HaskValue (..))
import Proarrow.Profunctor.Representable (Representable (..), dimapRep, withRepOb)
import Proarrow.Profunctor.Terminal (TerminalProfunctor (..))

type Unweighted = TerminalProfunctor

class (Representable (Colimit j d)) => IsRepresentableColimit j d
instance (Representable (Colimit j d)) => IsRepresentableColimit j d

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

  -- Note: can't simplify this to Colimit j d :~> d :.: j because j is not necessarily representable.
  colimitUniv :: (Representable (d :: i +-> k), Representable p) => (d :.: j :~> p) -> Colimit j d :~> p

leftAdjointPreservesColimits
  :: forall {k} {k'} {i} {a} (f :: k +-> k') g (d :: i +-> k) (j :: a +-> i)
   . (Adjunction f g, Representable d, Representable f, Representable g, HasColimits j k, HasColimits j k')
  => f :.: Colimit j d :~> Colimit j (f :.: d)
leftAdjointPreservesColimits :: forall {k} {k'} {i} {a} (f :: k +-> k') (g :: k' +-> k)
       (d :: i +-> k) (j :: a +-> i).
(Adjunction f g, Representable d, Representable f, Representable g,
 HasColimits j k, HasColimits j k') =>
(f :.: Colimit j d) :~> Colimit j (f :.: d)
leftAdjointPreservesColimits (f a b
f :.: Colimit j d b b
colim) =
  Colimit j d b b
colim Colimit j d b b
-> ((Ob b, Ob b) => Colimit j (f :.: d) a b)
-> Colimit j (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
// case forall {i} {a} (j :: a +-> i) k (d :: i +-> k) (p :: a +-> k).
(HasColimits j k, Representable d, Representable p) =>
((d :.: j) :~> p) -> Colimit j d :~> p
forall (j :: a +-> i) k (d :: i +-> k) (p :: a +-> k).
(HasColimits j k, Representable d, Representable p) =>
((d :.: j) :~> p) -> Colimit j d :~> p
colimitUniv @j @k @d @(g :.: Colimit j (f :.: d))
    (\(d a b
d :.: j b b
j) -> case forall {i} {j} (p :: i +-> j) (q :: j +-> i) (a :: i) (b :: i).
Adjunction p q =>
(a ~> b) -> (:.:) q p a b
forall (p :: k +-> k') (q :: k' +-> k) (a :: k) (b :: k).
Adjunction p q =>
(a ~> b) -> (:.:) q p a b
unit' @f @g (d a b -> a ~> a
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src d a b
d) of g a b
g :.: f b a
f' -> g a b
g g a b
-> Colimit j (f :.: d) b b -> (:.:) g (Colimit j (f :.: 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 :: i +-> k).
(HasColimits j k, Representable d) =>
(d :.: j) :~> Colimit j d
forall (j :: a +-> i) k (d :: i +-> k).
(HasColimits j k, Representable d) =>
(d :.: j) :~> Colimit j d
colimit @j @k' @(f :.: d) ((f b a
f' f b a -> d a b -> (:.:) f 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
:.: d a b
d) (:.:) f d b b -> j b b -> (:.:) (f :.: 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))
    Colimit j d b b
colim of
    g b b
g :.: Colimit j (f :.: d) b b
colim' -> (a ~> b) -> Colimit j (f :.: d) b b -> Colimit j (f :.: d) a b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap ((:.:) f g a b -> a ~> b
(f :.: g) :~> (~>)
forall {j} {k} (p :: j +-> k) (q :: k +-> j).
Adjunction p q =>
(p :.: q) :~> (~>)
counit (f a b
f f a b -> g b b -> (:.:) f g a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: g b b
g)) Colimit j (f :.: d) b b
colim'

leftAdjointPreservesColimitsInv
  :: forall {k} {k'} {i} {a} (f :: k +-> k') (d :: i +-> k) (j :: a +-> i)
   . (Representable d, Representable f, HasColimits j k, HasColimits j k')
  => Colimit j (f :.: d) :~> f :.: Colimit j d
leftAdjointPreservesColimitsInv :: forall {k} {k'} {i} {a} (f :: k +-> k') (d :: i +-> k)
       (j :: a +-> i).
(Representable d, Representable f, HasColimits j k,
 HasColimits j k') =>
Colimit j (f :.: d) :~> (f :.: Colimit j d)
leftAdjointPreservesColimitsInv = forall {i} {a} (j :: a +-> i) k (d :: i +-> k) (p :: a +-> k).
(HasColimits j k, Representable d, Representable p) =>
((d :.: j) :~> p) -> Colimit j d :~> p
forall (j :: a +-> i) k (d :: i +-> k) (p :: a +-> k).
(HasColimits j k, Representable d, Representable p) =>
((d :.: j) :~> p) -> Colimit j d :~> p
colimitUniv @j @k' @(f :.: d) (\((f a b
f :.: d b b
d) :.: j b b
j) -> f a b
f f a b -> Colimit j d b b -> (:.:) f (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
:.: (:.:) d j b b -> Colimit j d b b
(d :.: j) :~> Colimit j d
forall {i} {a} (j :: a +-> i) k (d :: i +-> k).
(HasColimits j k, Representable d) =>
(d :.: j) :~> Colimit j d
forall (d :: i +-> k). Representable d => (d :.: j) :~> Colimit j d
colimit (d b b
d d b b -> j b b -> (:.:) 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 InitialLimit :: VOID +-> k -> () +-> k
data InitialLimit d a b where
  InitialLimit :: forall {k} d a. a ~> InitialLimit d % '() -> InitialLimit (d :: VOID +-> k) a '()
instance (HasInitialObject k) => Profunctor (InitialLimit (d :: VOID +-> k)) where
  dimap :: forall (c :: k) (a :: k) (b :: ()) (d :: ()).
(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).
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) -> InitialLimit d a b -> r
\\ InitialLimit a ~> (InitialLimit d % '())
f = r
(Ob a, Ob InitialObject) => r
(Ob a, Ob b) => r
r ((Ob a, Ob InitialObject) => r) -> (a ~> InitialObject) -> 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 ~> (InitialLimit d % '())
a ~> InitialObject
f
instance (HasInitialObject k) => Representable (InitialLimit (d :: VOID +-> k)) where
  type InitialLimit d % '() = InitialObject
  index :: forall (a :: k) (b :: ()).
InitialLimit d a b -> a ~> (InitialLimit d % b)
index (InitialLimit a ~> (InitialLimit d % '())
f) = a ~> (InitialLimit d % b)
a ~> (InitialLimit d % '())
f
  tabulate :: forall (b :: ()) (a :: k).
Ob b =>
(a ~> (InitialLimit d % b)) -> InitialLimit d a b
tabulate = (a ~> (InitialLimit d % b)) -> InitialLimit d a b
(a ~> (InitialLimit d % '())) -> InitialLimit d a '()
forall {k} (d :: VOID +-> k) (a :: k).
(a ~> (InitialLimit d % '())) -> InitialLimit d a '()
InitialLimit
  repMap :: forall (a :: ()) (b :: ()).
(a ~> b) -> (InitialLimit d % a) ~> (InitialLimit d % b)
repMap 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 :: VOID +-> k).
Representable d =>
(d :.: Unweighted) :~> Colimit Unweighted d
colimit = \case {}
  colimitUniv :: forall (d :: VOID +-> k) (p :: () +-> k).
(Representable d, Representable p) =>
((d :.: Unweighted) :~> p) -> Colimit Unweighted d :~> p
colimitUniv @_ @p (d :.: Unweighted) :~> p
_ (InitialLimit a ~> (InitialLimit d % '())
f) = forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: () +-> k) (b :: ()) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @p (((p % '()) ~> (p % '())) -> InitialObject ~> (p % '())
forall {k} (a' :: k) (a :: k).
HasInitialObject k =>
(a' ~> a) -> InitialObject ~> a
initiate' (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: () +-> k) (a :: ()) (b :: ()).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p '() ~> '()
Unit '() '()
Unit) (InitialObject ~> (p % '()))
-> (a ~> InitialObject) -> a ~> (p % '())
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (InitialLimit d % '())
a ~> InitialObject
f)

type CoproductColimit :: COPRODUCT () () +-> k -> () +-> k
data CoproductColimit d a b where
  CoproductColimit :: forall d a. a ~> CoproductColimit d % '() -> CoproductColimit d a '()
instance (HasBinaryCoproducts k, Representable d) => Profunctor (CoproductColimit d :: () +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: ()) (d :: ()).
(c ~> a)
-> (b ~> d) -> CoproductColimit d a b -> CoproductColimit d c d
dimap = (c ~> a)
-> (b ~> d) -> CoproductColimit d a b -> CoproductColimit 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) -> CoproductColimit d a b -> r
\\ CoproductColimit a ~> (CoproductColimit 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 :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> (CoproductColimit d % '())
a ~> ((d % L '()) || (d % R '()))
f
instance (HasBinaryCoproducts k, Representable d) => Representable (CoproductColimit d :: () +-> k) where
  type CoproductColimit d % '() = (d % L '()) || (d % R '())
  index :: forall (a :: k) (b :: ()).
CoproductColimit d a b -> a ~> (CoproductColimit d % b)
index (CoproductColimit a ~> (CoproductColimit d % '())
f) = a ~> (CoproductColimit d % b)
a ~> (CoproductColimit d % '())
f
  tabulate :: forall (b :: ()) (a :: k).
Ob b =>
(a ~> (CoproductColimit d % b)) -> CoproductColimit d a b
tabulate = (a ~> (CoproductColimit d % b)) -> CoproductColimit d a b
(a ~> (CoproductColimit d % '())) -> CoproductColimit d a '()
forall {k} (d :: COPRODUCT () () +-> k) (a :: k).
(a ~> (CoproductColimit d % '())) -> CoproductColimit d a '()
CoproductColimit
  repMap :: forall (a :: ()) (b :: ()).
(a ~> b) -> (CoproductColimit d % a) ~> (CoproductColimit d % b)
repMap 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 :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: COPRODUCT () () +-> k) (a :: COPRODUCT () ())
       (b :: COPRODUCT () ()).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @d (Unit '() '() -> (:++:) Unit Unit (L '()) (L '())
forall {j1} {k1} {j2} {k2} (p :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (q :: j2 +-> k2).
p a1 b1 -> (:++:) p q (L a1) (L b1)
InjL Unit '() '()
Unit)) (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: COPRODUCT () () +-> k) (a :: COPRODUCT () ())
       (b :: COPRODUCT () ()).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @d (Unit '() '() -> (:++:) Unit Unit (R '()) (R '())
forall {j2} {k2} {j1} {k1} (q :: j2 +-> k2) (a1 :: k2) (b1 :: j2)
       (p :: j1 +-> k1).
q a1 b1 -> (:++:) p q (R a1) (R b1)
InjR Unit '() '()
Unit))

instance (HasBinaryCoproducts k) => HasColimits (Unweighted :: () +-> COPRODUCT () ()) k where
  type Colimit Unweighted d = CoproductColimit d
  colimit :: forall (d :: COPRODUCT () () +-> k).
Representable d =>
(d :.: Unweighted) :~> Colimit Unweighted d
colimit @d (d a b
d :.: TerminalProfunctor' Obj b
b Obj b
Unit b b
Unit) = (a ~> (CoproductColimit d % '())) -> CoproductColimit d a '()
forall {k} (d :: COPRODUCT () () +-> k) (a :: k).
(a ~> (CoproductColimit d % '())) -> CoproductColimit d a '()
CoproductColimit (forall k (d :: COPRODUCT () () +-> k) (b :: COPRODUCT () ()).
(HasBinaryCoproducts k, Representable d) =>
Obj b -> (d % b) ~> ((d % L '()) || (d % R '()))
cochoose @k @d Obj b
b ((d % b) ~> ((d % L '()) || (d % R '())))
-> (a ~> (d % b)) -> a ~> ((d % L '()) || (d % R '()))
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 a b -> a ~> (d % b)
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 b
d)
  colimitUniv :: forall (d :: COPRODUCT () () +-> k) (p :: () +-> k).
(Representable d, Representable p) =>
((d :.: Unweighted) :~> p) -> Colimit Unweighted d :~> p
colimitUniv @d @p (d :.: Unweighted) :~> p
n (CoproductColimit a ~> (CoproductColimit d % '())
f) =
    let l :: (d % L '()) ~> (p % '())
l = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: () +-> k) (a :: k) (b :: ()).
Representable p =>
p a b -> a ~> (p % b)
index @p ((:.:) d Unweighted (d % L '()) '() -> p (d % L '()) '()
(d :.: Unweighted) :~> p
n (forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: COPRODUCT () () +-> k) (b :: COPRODUCT () ())
       (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @d (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: COPRODUCT () () +-> k) (a :: COPRODUCT () ())
       (b :: COPRODUCT () ()).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @d (Unit '() '() -> (:++:) Unit Unit (L '()) (L '())
forall {j1} {k1} {j2} {k2} (p :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (q :: j2 +-> k2).
p a1 b1 -> (:++:) p q (L a1) (L b1)
InjL Unit '() '()
Unit)) d (d % L '()) (L '())
-> Unweighted (L '()) '() -> (:.:) d Unweighted (d % 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
:.: (L '() ~> L '()) -> ('() ~> '()) -> Unweighted (L '()) '()
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) '() ~> '()
Unit '() '()
Unit))
        r :: (d % R '()) ~> (p % '())
r = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: () +-> k) (a :: k) (b :: ()).
Representable p =>
p a b -> a ~> (p % b)
index @p ((:.:) d Unweighted (d % R '()) '() -> p (d % R '()) '()
(d :.: Unweighted) :~> p
n (forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: COPRODUCT () () +-> k) (b :: COPRODUCT () ())
       (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @d (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: COPRODUCT () () +-> k) (a :: COPRODUCT () ())
       (b :: COPRODUCT () ()).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @d (Unit '() '() -> (:++:) Unit Unit (R '()) (R '())
forall {j2} {k2} {j1} {k1} (q :: j2 +-> k2) (a1 :: k2) (b1 :: j2)
       (p :: j1 +-> k1).
q a1 b1 -> (:++:) p q (R a1) (R b1)
InjR Unit '() '()
Unit)) d (d % R '()) (R '())
-> Unweighted (R '()) '() -> (:.:) d Unweighted (d % 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
:.: (R '() ~> R '()) -> ('() ~> '()) -> Unweighted (R '()) '()
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) '() ~> '()
Unit '() '()
Unit))
    in forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: () +-> k) (b :: ()) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @p (((d % L '()) ~> (p % '())
l ((d % L '()) ~> (p % '()))
-> ((d % R '()) ~> (p % '()))
-> ((d % L '()) || (d % R '())) ~> (p % '())
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 '()) ~> (p % '())
r) (((d % L '()) || (d % R '())) ~> (p % '()))
-> (a ~> ((d % L '()) || (d % R '()))) -> a ~> (p % '())
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (CoproductColimit d % '())
a ~> ((d % L '()) || (d % R '()))
f)

cochoose
  :: forall k (d :: COPRODUCT () () +-> k) b
   . (HasBinaryCoproducts k, Representable d)
  => Obj b
  -> (d % b) ~> ((d % L '()) || (d % R '()))
cochoose :: forall k (d :: COPRODUCT () () +-> k) (b :: COPRODUCT () ()).
(HasBinaryCoproducts k, Representable d) =>
Obj b -> (d % b) ~> ((d % L '()) || (d % R '()))
cochoose Obj b
b = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: COPRODUCT () () +-> k) (a :: COPRODUCT () ()) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withRepOb @d @(L '()) ((Ob (d % L '()) => (d % 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 {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: COPRODUCT () () +-> k) (a :: COPRODUCT () ()) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withRepOb @d @(R '()) ((Ob (d % R '()) => (d % 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 a. (Ob n) => (a ~> CopowerLimit n d % '()) -> CopowerLimit n d a '()
instance (Representable d, Copowered k) => Profunctor (CopowerLimit n d :: () +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: ()) (d :: ()).
(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).
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) -> CopowerLimit n d a b -> r
\\ CopowerLimit a ~> (CopowerLimit n d % '())
f = r
(Ob a, Ob (n *. (d % '()))) => r
(Ob a, Ob b) => r
r ((Ob a, Ob (n *. (d % '()))) => r) -> (a ~> (n *. (d % '()))) -> 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 ~> (CopowerLimit n d % '())
a ~> (n *. (d % '()))
f
instance (Representable d, Copowered k) => Representable (CopowerLimit n d :: () +-> k) where
  type CopowerLimit n d % '() = n *. (d % '())
  index :: forall (a :: k) (b :: ()).
CopowerLimit n d a b -> a ~> (CopowerLimit n d % b)
index (CopowerLimit a ~> (CopowerLimit n d % '())
f) = a ~> (CopowerLimit n d % b)
a ~> (CopowerLimit n d % '())
f
  tabulate :: forall (b :: ()) (a :: k).
Ob b =>
(a ~> (CopowerLimit n d % b)) -> CopowerLimit n d a b
tabulate = (a ~> (CopowerLimit n d % b)) -> CopowerLimit n d a b
(a ~> (CopowerLimit n d % '())) -> CopowerLimit n d a '()
forall {k} n (d :: () +-> k) (a :: k).
Ob n =>
(a ~> (CopowerLimit n d % '())) -> CopowerLimit n d a '()
CopowerLimit
  repMap :: forall (a :: ()) (b :: ()).
(a ~> b) -> (CopowerLimit n d % a) ~> (CopowerLimit n d % b)
repMap a ~> b
Unit a b
Unit = forall k (a :: k) n r.
(Copowered k, Ob a) =>
(Ob (n *. a) => r) -> r
withObCopower @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 {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: () +-> k) (a :: ()) (b :: ()).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @d '() ~> '()
Unit '() '()
Unit

instance (Copowered k) => HasColimits (HaskValue n :: () +-> ()) k where
  type Colimit (HaskValue n) d = CopowerLimit n d
  colimit :: forall (d :: () +-> k).
Representable d =>
(d :.: HaskValue n) :~> Colimit (HaskValue n) d
colimit @d (d a b
d :.: HaskValue n
n) = forall k (a :: k) n r.
(Copowered k, Ob a) =>
(Ob (n *. a) => r) -> r
withObCopower @k @(d % '()) @n ((a ~> (CopowerLimit n d % '())) -> CopowerLimit n d a '()
forall {k} n (d :: () +-> k) (a :: k).
Ob n =>
(a ~> (CopowerLimit n d % '())) -> CopowerLimit n d a '()
CopowerLimit (((n *. (d % '())) ~> (n *. (d % '())))
-> n -> (d % '()) ~> (n *. (d % '()))
forall (a :: k) n (b :: k). Ob a => ((n *. a) ~> b) -> n -> a ~> b
forall k (a :: k) n (b :: k).
(Copowered k, Ob a) =>
((n *. a) ~> b) -> n -> a ~> b
uncopower (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 n
n ((d % '()) ~> (n *. (d % '())))
-> (a ~> (d % '())) -> a ~> (n *. (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 a b -> a ~> (d % b)
forall (a :: k) (b :: ()). d a b -> a ~> (d % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index d a b
d)) ((Ob (d % '()), Ob (d % '())) => CopowerLimit n d a '())
-> ((d % '()) ~> (d % '())) -> CopowerLimit n d a '()
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: () +-> k) (a :: ()) (b :: ()).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @d '() ~> '()
Unit '() '()
Unit
  colimitUniv :: forall (d :: () +-> k) (p :: () +-> k).
(Representable d, Representable p) =>
((d :.: HaskValue n) :~> p) -> Colimit (HaskValue n) d :~> p
colimitUniv @d @p (d :.: HaskValue n) :~> p
m (CopowerLimit a ~> (CopowerLimit n d % '())
f) =
    forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: () +-> k) (b :: ()) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @p (forall k (a :: k) (b :: k) n.
(Copowered k, Ob a, Ob b) =>
(n -> a ~> b) -> (n *. a) ~> b
copower @k @(d % '()) @_ @n (\n
n -> forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: () +-> k) (a :: k) (b :: ()).
Representable p =>
p a b -> a ~> (p % b)
index @p ((:.:) d (HaskValue n) (d % '()) '() -> p (d % '()) '()
(d :.: HaskValue n) :~> p
m (forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: () +-> k) (b :: ()) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @d (d % '()) ~> (d % '())
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id d (d % '()) '()
-> HaskValue n '() '() -> (:.:) d (HaskValue n) (d % '()) '()
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: n -> HaskValue n '() '()
forall {k} {j} (a :: k) (b :: j) c.
(Ob a, Ob b) =>
c -> HaskValue c a b
HaskValue n
n))) ((n *. (d % '())) ~> (p % '()))
-> (a ~> (n *. (d % '()))) -> a ~> (p % '())
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (CopowerLimit n d % '())
a ~> (n *. (d % '()))
f)
      ((Ob (d % '()), Ob (d % '())) => p a b)
-> ((d % '()) ~> (d % '())) -> p a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: () +-> k) (a :: ()) (b :: ()).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @d '() ~> '()
Unit '() '()
Unit
      ((Ob (p % '()), Ob (p % '())) => p a b)
-> ((p % '()) ~> (p % '())) -> p a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: () +-> k) (a :: ()) (b :: ()).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p '() ~> '()
Unit '() '()
Unit