module Proarrow.Object.Terminal where

import Data.Kind (Type)

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

class (CategoryOf k, Ob (TerminalObject :: k)) => HasTerminalObject k where
  type TerminalObject :: k
  terminate :: (Ob (a :: k)) => a ~> TerminalObject
  terminate @a = (a ~> a) -> a ~> TerminalObject
forall (a :: k) (a' :: k). (a ~> a') -> a ~> TerminalObject
forall k (a :: k) (a' :: k).
HasTerminalObject k =>
(a ~> 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)
  terminate' :: (a :: k) ~> a' -> a ~> TerminalObject
  terminate' @_ @a' a ~> a'
a = forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate @k @a' (a' ~> TerminalObject) -> (a ~> a') -> a ~> TerminalObject
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
. a ~> a'
a ((Ob a, Ob a') => a ~> TerminalObject)
-> (a ~> a') -> a ~> TerminalObject
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

-- | The type of elements of `a`.
type El a = TerminalObject ~> a

instance HasTerminalObject Type where
  type TerminalObject = ()
  terminate :: forall a. Ob a => a ~> TerminalObject
terminate a
_ = ()

instance (HasTerminalObject j, HasTerminalObject k) => HasTerminalObject (j, k) where
  type TerminalObject = '(TerminalObject, TerminalObject)
  terminate :: forall (a :: (j, k)). Ob a => a ~> TerminalObject
terminate = Fst a ~> TerminalObject
forall (a :: j). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate (Fst a ~> TerminalObject)
-> (Snd a ~> TerminalObject)
-> (:**:)
     (~>) (~>) '(Fst a, Snd a) '(TerminalObject, TerminalObject)
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)
:**: Snd a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate

instance (CategoryOf j, CategoryOf k) => HasTerminalObject (PRO j k) where
  type TerminalObject = TerminalProfunctor
  terminate :: forall (a :: PRO j k). Ob a => a ~> TerminalObject
terminate = (a :~> TerminalProfunctor) -> Prof a TerminalProfunctor
forall {k} {j} (p :: j +-> k) (q :: 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).
(CategoryOf j, CategoryOf 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