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