module Proarrow.Object.Terminal where import Data.Kind (Type) import Proarrow.Core (CategoryOf(..), Profunctor (..), PRO) import Proarrow.Object (Obj, obj) import Proarrow.Category.Instance.Product ((:**:)(..)) import Proarrow.Category.Instance.Prof (Prof(..)) import Proarrow.Profunctor.Terminal (TerminalProfunctor(..)) class (CategoryOf k, Ob (TerminalObject :: k)) => HasTerminalObject k where type TerminalObject :: k terminate' :: Obj (a :: k) -> a ~> TerminalObject terminate :: forall {k} a. (HasTerminalObject k, Ob (a :: k)) => a ~> TerminalObject terminate :: forall {k} (a :: k). (HasTerminalObject k, Ob a) => a ~> TerminalObject terminate = Obj a -> a ~> TerminalObject forall (a :: k). Obj a -> a ~> TerminalObject forall k (a :: k). HasTerminalObject k => Obj a -> a ~> TerminalObject terminate' (forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @a) type El a = TerminalObject ~> a instance HasTerminalObject Type where type TerminalObject = () terminate' :: forall a. Obj a -> a ~> TerminalObject terminate' Obj a _ a _ = () instance (HasTerminalObject j, HasTerminalObject k) => HasTerminalObject (j, k) where type TerminalObject = '(TerminalObject, TerminalObject) terminate' :: forall (a :: (j, k)). Obj a -> a ~> TerminalObject terminate' (a1 ~> b1 a1 :**: a2 ~> b2 a2) = Obj b1 -> b1 ~> TerminalObject forall (a :: j). Obj a -> a ~> TerminalObject forall k (a :: k). HasTerminalObject k => Obj a -> a ~> TerminalObject terminate' a1 ~> b1 Obj b1 a1 (b1 ~> TerminalObject) -> (b2 ~> TerminalObject) -> (:**:) (~>) (~>) '(b1, b2) '(TerminalObject, TerminalObject) forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2) (a2 :: k2) (b2 :: k2). c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2) :**: Obj b2 -> b2 ~> TerminalObject forall (a :: k). Obj a -> a ~> TerminalObject forall k (a :: k). HasTerminalObject k => Obj a -> a ~> TerminalObject terminate' a2 ~> b2 Obj b2 a2 instance (CategoryOf j, CategoryOf k) => HasTerminalObject (PRO j k) where type TerminalObject = TerminalProfunctor terminate' :: forall (a :: PRO j k). Obj a -> a ~> TerminalObject terminate' Prof{} = (a :~> TerminalProfunctor) -> Prof a TerminalProfunctor forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \a a b a -> TerminalProfunctor a b (Ob a, Ob b) => TerminalProfunctor a b forall {j} {k} (a :: j) (b :: k). (Ob a, Ob b) => TerminalProfunctor a b TerminalProfunctor ((Ob a, Ob b) => TerminalProfunctor a b) -> a a b -> TerminalProfunctor a b forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> a 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 a b a