module Proarrow.Object.Initial where import Data.Kind (Type) import Data.Void (Void, absurd) import Proarrow.Core (CategoryOf(..), PRO) import Proarrow.Object (Obj, obj) import Proarrow.Category.Instance.Product ((:**:)(..)) import Proarrow.Category.Instance.Prof (Prof(..)) import Proarrow.Profunctor.Initial (InitialProfunctor) class (CategoryOf k, Ob (InitialObject :: k)) => HasInitialObject k where type InitialObject :: k initiate' :: Obj (a :: k) -> InitialObject ~> a initiate :: forall {k} a. (HasInitialObject k, Ob (a :: k)) => InitialObject ~> a initiate :: forall {k} (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a initiate = Obj a -> InitialObject ~> a forall (a :: k). Obj a -> InitialObject ~> a forall k (a :: k). HasInitialObject k => Obj a -> InitialObject ~> a initiate' (forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @a) instance HasInitialObject Type where type InitialObject = Void initiate' :: forall a. Obj a -> InitialObject ~> a initiate' Obj a _ = InitialObject ~> a Void -> a forall a. Void -> a absurd instance (HasInitialObject j, HasInitialObject k) => HasInitialObject (j, k) where type InitialObject = '(InitialObject, InitialObject) initiate' :: forall (a :: (j, k)). Obj a -> InitialObject ~> a initiate' (a1 ~> b1 a1 :**: a2 ~> b2 a2) = Obj b1 -> InitialObject ~> b1 forall (a :: j). Obj a -> InitialObject ~> a forall k (a :: k). HasInitialObject k => Obj a -> InitialObject ~> a initiate' a1 ~> b1 Obj b1 a1 (InitialObject ~> b1) -> (InitialObject ~> b2) -> (:**:) (~>) (~>) '(InitialObject, InitialObject) '(b1, b2) 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 -> InitialObject ~> b2 forall (a :: k). Obj a -> InitialObject ~> a forall k (a :: k). HasInitialObject k => Obj a -> InitialObject ~> a initiate' a2 ~> b2 Obj b2 a2 instance (CategoryOf j, CategoryOf k) => HasInitialObject (PRO j k) where type InitialObject = InitialProfunctor initiate' :: forall (a :: PRO j k). Obj a -> InitialObject ~> a initiate' Prof{} = (InitialProfunctor :~> a) -> Prof InitialProfunctor a forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof InitialProfunctor a b -> a a b InitialProfunctor :~> a \case