{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Colimit where

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

import Proarrow.Adjunction (Adjunction (..), unit')
import Proarrow.Category.Instance.Coproduct (COLLAGE (..), COPRODUCT, pattern InjL, pattern InjR)
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.Initial (HasInitialObject (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Representable (Representable (..), dimapRep, withRepObj)
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 (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
  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 :: PRO 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 :: PRO k1 k2) (a :: k1) (b :: k2) 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 {j} {i} (p :: PRO j i) (q :: PRO i j) (a :: i) (b :: i).
Adjunction p q =>
(a ~> b) -> (:.:) q p a b
forall (p :: PRO k' k) (q :: PRO k k') (a :: k) (b :: k).
Adjunction p q =>
(a ~> b) -> (:.:) q p a b
unit' @f @g (d a b -> a ~> a
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
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 :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap ((:.:) f g a b -> a ~> b
(f :.: g) :~> (~>)
forall {j} {k} (p :: PRO k j) (q :: PRO j k).
Adjunction p q =>
(p :.: q) :~> (~>)
counit (f a b
f f a b -> g b b -> (:.:) f g a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: g b b
g)) 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 ~> InitialObject -> 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 ~> InitialObject
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 :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ 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 ~> InitialObject
f) = a ~> (InitialLimit d % b)
a ~> InitialObject
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 ~> InitialObject) -> InitialLimit d a '()
forall {k} (d :: VOID +-> k) (a :: k).
(a ~> InitialObject) -> 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 :: PRO 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 ~> InitialObject
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 (a' :: k) (a :: k). (a' ~> a) -> InitialObject ~> a
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 :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> InitialObject
f)

type CoproductColimit :: COPRODUCT () () +-> k -> () +-> k
data CoproductColimit d a b where
  CoproductColimit :: forall d a. a ~> ((d % L '()) || (d % R '())) -> 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 ~> ((d % L '()) || (d % R '()))
f) = r
(Ob a, Ob ((d % L '()) || (d % R '()))) => r
(Ob a, Ob b) => r
r ((Ob a, Ob ((d % L '()) || (d % R '()))) => r)
-> (a ~> ((d % L '()) || (d % R '()))) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> ((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 ~> ((d % L '()) || (d % R '()))
f) = a ~> (CoproductColimit d % b)
a ~> ((d % L '()) || (d % R '()))
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 ~> ((d % L '()) || (d % R '()))) -> CoproductColimit d a '()
forall {k} (d :: COPRODUCT () () +-> k) (a :: k).
(a ~> ((d % L '()) || (d % R '()))) -> 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 (('() ~> '()) -> (:++:) (~>) (~>) (L '()) (L '())
forall {k} {j} (a' :: COLLAGE InitialProfunctor)
       (b' :: COLLAGE InitialProfunctor) (a :: k) (b :: k).
(a' ~ L a, b' ~ L b) =>
(a ~> b) -> (:++:) (~>) (~>) a' b'
InjL '() ~> '()
Unit '() '()
Unit)) (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: COPRODUCT () () +-> k) (a :: COPRODUCT () ())
       (b :: COPRODUCT () ()).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @d (('() ~> '()) -> (:++:) (~>) (~>) (R '()) (R '())
forall {k} {j} (a' :: COLLAGE InitialProfunctor)
       (b' :: COLLAGE InitialProfunctor) (a :: j) (b :: j).
(a' ~ R a, b' ~ R b) =>
(a ~> b) -> (:++:) (~>) (~>) a' b'
InjR '() ~> '()
Unit '() '()
Unit))

instance (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 ~> ((d % L '()) || (d % R '()))) -> CoproductColimit d a '()
forall {k} (d :: COPRODUCT () () +-> k) (a :: k).
(a ~> ((d % L '()) || (d % R '()))) -> 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 :: PRO 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 ~> ((d % L '()) || (d % R '()))
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 (('() ~> '()) -> (:++:) (~>) (~>) (L '()) (L '())
forall {k} {j} (a' :: COLLAGE InitialProfunctor)
       (b' :: COLLAGE InitialProfunctor) (a :: k) (b :: k).
(a' ~ L a, b' ~ L b) =>
(a ~> b) -> (:++:) (~>) (~>) a' b'
InjL '() ~> '()
Unit '() '()
Unit)) 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' (('() ~> '()) -> (:++:) (~>) (~>) (L '()) (L '())
forall {k} {j} (a' :: COLLAGE InitialProfunctor)
       (b' :: COLLAGE InitialProfunctor) (a :: k) (b :: k).
(a' ~ L a, b' ~ L b) =>
(a ~> b) -> (:++:) (~>) (~>) a' b'
InjL '() ~> '()
Unit '() '()
Unit) '() ~> '()
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 (('() ~> '()) -> (:++:) (~>) (~>) (R '()) (R '())
forall {k} {j} (a' :: COLLAGE InitialProfunctor)
       (b' :: COLLAGE InitialProfunctor) (a :: j) (b :: j).
(a' ~ R a, b' ~ R b) =>
(a ~> b) -> (:++:) (~>) (~>) a' b'
InjR '() ~> '()
Unit '() '()
Unit)) 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' (('() ~> '()) -> (:++:) (~>) (~>) (R '()) (R '())
forall {k} {j} (a' :: COLLAGE InitialProfunctor)
       (b' :: COLLAGE InitialProfunctor) (a :: j) (b :: j).
(a' ~ R a, b' ~ R b) =>
(a ~> b) -> (:++:) (~>) (~>) a' b'
InjR '() ~> '()
Unit '() '()
Unit) '() ~> '()
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 :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. 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
withRepObj @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
withRepObj @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 a ~> b
Unit b b
Unit) -> forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @(d % L '()) @(d % R '())
  (InjR a ~> b
Unit b b
Unit) -> forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @(d % L '()) @(d % R '())