{-# 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)