module Proarrow.Object.Initial where

import Data.Kind (Type)
import Data.Void (Void, absurd)

import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Core (CategoryOf (..), PRO, Profunctor (..), Promonad (..))
import Proarrow.Object (obj)
import Proarrow.Profunctor.Initial (InitialProfunctor)

class (CategoryOf k, Ob (InitialObject :: k)) => HasInitialObject k where
  {-# MINIMAL initiate | initiate' #-}
  type InitialObject :: k
  initiate :: (Ob (a :: k)) => InitialObject ~> a
  initiate @a = (a ~> a) -> InitialObject ~> a
forall (a' :: k) (a :: k). (a' ~> a) -> InitialObject ~> a
forall k (a' :: k) (a :: k).
HasInitialObject k =>
(a' ~> 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)
  initiate' :: (a' :: k) ~> a -> InitialObject ~> a
  initiate' @a' a' ~> a
a = a' ~> a
a (a' ~> a) -> (InitialObject ~> a') -> InitialObject ~> a
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 (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @k @a' ((Ob a', Ob a) => InitialObject ~> a)
-> (a' ~> a) -> InitialObject ~> a
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
\\ a' ~> a
a

instance HasInitialObject Type where
  type InitialObject = Void
  initiate :: forall a. Ob a => InitialObject ~> a
initiate = 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)). Ob a => InitialObject ~> a
initiate = InitialObject ~> Fst a
forall (a :: j). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate (InitialObject ~> Fst a)
-> (InitialObject ~> Snd a)
-> (:**:) (~>) (~>) '(InitialObject, InitialObject) '(Fst a, Snd a)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: InitialObject ~> Snd a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate

instance (CategoryOf j, CategoryOf k) => HasInitialObject (PRO j k) where
  type InitialObject = InitialProfunctor
  initiate :: forall (a :: PRO j k). Ob a => InitialObject ~> a
initiate = (InitialProfunctor :~> a) -> Prof InitialProfunctor a
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \case {}