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