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

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

import Proarrow.Core (PRO, CategoryOf(..), Promonad(..), Profunctor(..), (:~>), (//), CategoryOf, Kind)
import Proarrow.Category.Instance.Coproduct (COPRODUCT(..), (:++:)(..))
import Proarrow.Category.Instance.Unit (UNIT(..), Unit(..))
import Proarrow.Category.Instance.Zero (VOID)
import Proarrow.Profunctor.Corepresentable (Corepresentable(..), withCorepCod, dimapCorep)
import Proarrow.Profunctor.Ran (type (|>), Ran(..))
import Proarrow.Profunctor.Terminal (TerminalProfunctor(TerminalProfunctor'))
import Proarrow.Object (Obj)
import Proarrow.Object.Initial (HasInitialObject(..), initiate)
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts(..), lft, rgt)

type Unweighted = TerminalProfunctor

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

type HasColimits :: PRO i a -> Kind -> Constraint
class (forall (d :: PRO i k). Corepresentable d => IsCorepresentableColimit j d) => HasColimits (j :: PRO i a) k where
  type Colimit (j :: PRO i a) (d :: PRO i k) :: PRO a k
  colimit :: Corepresentable (d :: PRO i k) => Colimit j d :~> j |> d
  colimitInv :: Corepresentable (d :: PRO i k) => j |> d :~> Colimit j d


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

instance HasInitialObject k => Profunctor (InitialLimit (d :: PRO VOID k)) where
  dimap :: forall (c :: UNIT) (a :: UNIT) (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 :: PRO j k) (a :: j) (b :: k) (c :: j) (d :: k).
Corepresentable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapCorep
  (Ob a, Ob b) => r
r \\ :: forall (a :: UNIT) (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 :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ InitialObject ~> b
f
instance HasInitialObject k => Corepresentable (InitialLimit (d :: PRO VOID k)) where
  type InitialLimit d %% U = InitialObject
  coindex :: forall (a :: UNIT) (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 :: UNIT) (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 U b
forall {k} (d :: PRO VOID k) (a :: k).
(InitialObject ~> a) -> InitialLimit d U a
InitialLimit
  corepMap :: forall (a :: UNIT) (b :: UNIT).
(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 :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
instance HasInitialObject k => HasColimits (Unweighted :: PRO VOID UNIT) k where
  type Colimit Unweighted d = InitialLimit d
  colimit :: forall (d :: PRO VOID k).
Corepresentable d =>
Colimit Unweighted d :~> (Unweighted |> d)
colimit (InitialLimit @d InitialObject ~> b
f) = InitialObject ~> b
f (InitialObject ~> b)
-> ((Ob InitialObject, Ob b) => (|>) Unweighted d a b)
-> (|>) Unweighted 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
// (forall (x :: VOID). Ob x => Unweighted x a -> d x b)
-> (|>) Unweighted d a b
forall {j} {k} {i} (a :: j) (b :: k) (j2 :: PRO i j)
       (p :: PRO i k).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j2 x a -> p x b) -> Ran ('OP j2) p a b
Ran \(TerminalProfunctor' Obj x
o Obj a
_) -> ((d %% x) ~> b) -> d x b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
forall (a :: VOID) (b :: k). Ob a => ((d %% a) ~> b) -> d a b
cotabulate (((d %% x) ~> b) -> d x b) -> ((d %% x) ~> b) -> d x b
forall a b. (a -> b) -> a -> b
$ InitialObject ~> b
f (InitialObject ~> b)
-> ((d %% x) ~> InitialObject) -> (d %% x) ~> b
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
. case Obj x
o of
  colimitInv :: forall (d :: PRO VOID k).
Corepresentable d =>
(Unweighted |> d) :~> Colimit Unweighted d
colimitInv Ran{} = (InitialObject ~> b) -> InitialLimit d U b
forall {k} (d :: PRO VOID k) (a :: k).
(InitialObject ~> a) -> InitialLimit d U a
InitialLimit InitialObject ~> b
forall {k} (a :: k).
(HasInitialObject k, Ob a) =>
InitialObject ~> a
initiate


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

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

instance (HasBinaryCoproducts k, Corepresentable d) => Corepresentable (CoproductColimit d :: PRO UNIT k) where
  type CoproductColimit d %% U = (d %% L U) || (d %% R U)
  coindex :: forall (a :: UNIT) (b :: k).
CoproductColimit d a b -> (CoproductColimit d %% a) ~> b
coindex (CoproductColimit ((d %% 'L U) || (d %% 'R U)) ~> b
f) = (CoproductColimit d %% a) ~> b
((d %% 'L U) || (d %% 'R U)) ~> b
f
  cotabulate :: forall (a :: UNIT) (b :: k).
Ob a =>
((CoproductColimit d %% a) ~> b) -> CoproductColimit d a b
cotabulate = ((CoproductColimit d %% a) ~> b) -> CoproductColimit d a b
(((d %% 'L U) || (d %% 'R U)) ~> b) -> CoproductColimit d U b
forall {k} (d :: PRO (COPRODUCT UNIT UNIT) k) (b :: k).
(((d %% 'L U) || (d %% 'R U)) ~> b) -> CoproductColimit d U b
CoproductColimit
  corepMap :: forall (a :: UNIT) (b :: UNIT).
(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 U) @(d %% R U) (forall {j} {k} (p :: PRO j k) (a :: j) (b :: j).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: PRO (COPRODUCT UNIT UNIT) k)
       (a :: COPRODUCT UNIT UNIT) (b :: COPRODUCT UNIT UNIT).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @d (Unit U U -> (:++:) Unit Unit ('L U) ('L U)
forall {j} {k} (c :: CAT j) (a1 :: j) (b1 :: j) (d :: CAT k).
c a1 b1 -> (:++:) c d ('L a1) ('L b1)
InjL Unit U U
Unit)) (forall {j} {k} (p :: PRO j k) (a :: j) (b :: j).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: PRO (COPRODUCT UNIT UNIT) k)
       (a :: COPRODUCT UNIT UNIT) (b :: COPRODUCT UNIT UNIT).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @d (Unit U U -> (:++:) Unit Unit ('R U) ('R U)
forall {k} {j} (d :: CAT k) (a1 :: k) (b1 :: k) (c :: CAT j).
d a1 b1 -> (:++:) c d ('R a1) ('R b1)
InjR Unit U U
Unit))

instance HasBinaryCoproducts k => HasColimits (Unweighted :: PRO (COPRODUCT UNIT UNIT) UNIT) k where
  type Colimit Unweighted d = CoproductColimit d
  colimit :: forall (d :: PRO (COPRODUCT UNIT UNIT) k).
Corepresentable d =>
Colimit Unweighted d :~> (Unweighted |> d)
colimit (CoproductColimit @d ((d %% 'L U) || (d %% 'R U)) ~> b
f) = ((d %% 'L U) || (d %% 'R U)) ~> b
f (((d %% 'L U) || (d %% 'R U)) ~> b)
-> ((Ob ((d %% 'L U) || (d %% 'R U)), Ob b) =>
    (|>) Unweighted d a b)
-> (|>) Unweighted 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
// (forall (x :: COPRODUCT UNIT UNIT).
 Ob x =>
 Unweighted x a -> d x b)
-> (|>) Unweighted d a b
forall {j} {k} {i} (a :: j) (b :: k) (j2 :: PRO i j)
       (p :: PRO i k).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j2 x a -> p x b) -> Ran ('OP j2) p a b
Ran \(TerminalProfunctor' Obj x
o Obj a
_) -> ((d %% x) ~> b) -> d x b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
forall (a :: COPRODUCT UNIT UNIT) (b :: k).
Ob a =>
((d %% a) ~> b) -> d a b
cotabulate (((d %% x) ~> b) -> d x b) -> ((d %% x) ~> b) -> d x b
forall a b. (a -> b) -> a -> b
$ ((d %% 'L U) || (d %% 'R U)) ~> b
f (((d %% 'L U) || (d %% 'R U)) ~> b)
-> ((d %% x) ~> ((d %% 'L U) || (d %% 'R U))) -> (d %% x) ~> b
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
. forall k (d :: PRO (COPRODUCT UNIT UNIT) k)
       (b :: COPRODUCT UNIT UNIT).
(HasBinaryCoproducts k, Corepresentable d) =>
Obj b -> (d %% b) ~> ((d %% 'L U) || (d %% 'R U))
cochoose @_ @d Obj x
o
  colimitInv :: forall (d :: PRO (COPRODUCT UNIT UNIT) k).
Corepresentable d =>
(Unweighted |> d) :~> Colimit Unweighted d
colimitInv (Ran forall (x :: COPRODUCT UNIT UNIT). Ob x => j2 x a -> d x b
k) =
    let l :: d ('L U) b
l = j2 ('L U) a -> d ('L U) b
forall (x :: COPRODUCT UNIT UNIT). Ob x => j2 x a -> d x b
k (('L U ~> 'L U) -> Obj a -> TerminalProfunctor ('L U) a
forall j k (a :: j) (b :: k).
(CategoryOf j, CategoryOf k) =>
Obj a -> Obj b -> TerminalProfunctor a b
TerminalProfunctor' (Unit U U -> (:++:) Unit Unit ('L U) ('L U)
forall {j} {k} (c :: CAT j) (a1 :: j) (b1 :: j) (d :: CAT k).
c a1 b1 -> (:++:) c d ('L a1) ('L b1)
InjL Unit U U
Unit) Obj a
Unit U U
Unit)
        r :: d ('R U) b
r = j2 ('R U) a -> d ('R U) b
forall (x :: COPRODUCT UNIT UNIT). Ob x => j2 x a -> d x b
k (('R U ~> 'R U) -> Obj a -> TerminalProfunctor ('R U) a
forall j k (a :: j) (b :: k).
(CategoryOf j, CategoryOf k) =>
Obj a -> Obj b -> TerminalProfunctor a b
TerminalProfunctor' (Unit U U -> (:++:) Unit Unit ('R U) ('R U)
forall {k} {j} (d :: CAT k) (a1 :: k) (b1 :: k) (c :: CAT j).
d a1 b1 -> (:++:) c d ('R a1) ('R b1)
InjR Unit U U
Unit) Obj a
Unit U U
Unit)
    in (((d %% 'L U) || (d %% 'R U)) ~> b) -> CoproductColimit d U b
forall {k} (d :: PRO (COPRODUCT UNIT UNIT) k) (b :: k).
(((d %% 'L U) || (d %% 'R U)) ~> b) -> CoproductColimit d U b
CoproductColimit ((((d %% 'L U) || (d %% 'R U)) ~> b) -> CoproductColimit d U b)
-> (((d %% 'L U) || (d %% 'R U)) ~> b) -> CoproductColimit d U b
forall a b. (a -> b) -> a -> b
$ d ('L U) b -> (d %% 'L U) ~> b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
Corepresentable p =>
p a b -> (p %% a) ~> b
forall (a :: COPRODUCT UNIT UNIT) (b :: k). d a b -> (d %% a) ~> b
coindex d ('L U) b
l ((d %% 'L U) ~> b)
-> ((d %% 'R U) ~> b) -> ((d %% 'L U) || (d %% 'R U)) ~> 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 U) b -> (d %% 'R U) ~> b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
Corepresentable p =>
p a b -> (p %% a) ~> b
forall (a :: COPRODUCT UNIT UNIT) (b :: k). d a b -> (d %% a) ~> b
coindex d ('R U) b
r

cochoose
  :: forall k (d :: PRO (COPRODUCT UNIT UNIT) k) b
  .  (HasBinaryCoproducts k, Corepresentable d)
  => Obj b -> (d %% b) ~> ((d %% L U) || (d %% R U))
cochoose :: forall k (d :: PRO (COPRODUCT UNIT UNIT) k)
       (b :: COPRODUCT UNIT UNIT).
(HasBinaryCoproducts k, Corepresentable d) =>
Obj b -> (d %% b) ~> ((d %% 'L U) || (d %% 'R U))
cochoose Obj b
b = forall {j} {k} (p :: PRO j k) (a :: j) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: PRO (COPRODUCT UNIT UNIT) k)
       (a :: COPRODUCT UNIT UNIT) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withCorepCod @d @(L U) ((Ob (d %% 'L U) => (d %% b) ~> ((d %% 'L U) || (d %% 'R U)))
 -> (d %% b) ~> ((d %% 'L U) || (d %% 'R U)))
-> (Ob (d %% 'L U) => (d %% b) ~> ((d %% 'L U) || (d %% 'R U)))
-> (d %% b) ~> ((d %% 'L U) || (d %% 'R U))
forall a b. (a -> b) -> a -> b
$ forall {j} {k} (p :: PRO j k) (a :: j) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: PRO (COPRODUCT UNIT UNIT) k)
       (a :: COPRODUCT UNIT UNIT) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withCorepCod @d @(R U) ((Ob (d %% 'R U) => (d %% b) ~> ((d %% 'L U) || (d %% 'R U)))
 -> (d %% b) ~> ((d %% 'L U) || (d %% 'R U)))
-> (Ob (d %% 'R U) => (d %% b) ~> ((d %% 'L U) || (d %% 'R U)))
-> (d %% b) ~> ((d %% 'L U) || (d %% 'R U))
forall a b. (a -> b) -> a -> b
$ case Obj b
b of
  (InjL Unit a1 b1
Unit b1 b1
Unit) -> forall (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
forall {k} (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @(d %% L U) @(d %% R U)
  (InjR Unit a1 b1
Unit b1 b1
Unit) -> forall (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
forall {k} (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @(d %% L U) @(d %% R U)