-- | The terminal profunctor, with exactly one value between any two objects: the terminal object of the
-- category of profunctors @j +-> k@.
module Proarrow.Profunctor.Instance.Terminal (TerminalProfunctor (.., TerminalProfunctor)) where

import Proarrow.Category.Enriched.Dagger (Dagger, DaggerProfunctor (..))
import Proarrow.Category.Enriched.Thin (DecidableProfunctor (..), Decision (..), ThinProfunctor (..))
import Proarrow.Category.Instance.Bool (BOOL (..))
import Proarrow.Category.Monoidal (Monoidal, MonoidalProfunctor (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), type (+->))
import Proarrow.Object (pattern Obj, type Obj)

-- | The profunctor with exactly one value between any two objects: the terminal object of the
-- category of profunctors @j +-> k@.
type TerminalProfunctor :: j +-> k
data TerminalProfunctor a b where
  TerminalProfunctor' :: Obj a -> Obj b -> TerminalProfunctor (a :: j) (b :: k)

instance (CategoryOf j, CategoryOf k) => Profunctor (TerminalProfunctor :: j +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a)
-> (b ~> d) -> TerminalProfunctor a b -> TerminalProfunctor c d
dimap c ~> a
l b ~> d
r TerminalProfunctor a b
TerminalProfunctor = TerminalProfunctor c d
(Ob c, Ob a) => TerminalProfunctor c d
forall {j} {k} (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor ((Ob c, Ob a) => TerminalProfunctor c d)
-> (c ~> a) -> TerminalProfunctor c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ c ~> a
l ((Ob b, Ob d) => TerminalProfunctor c d)
-> (b ~> d) -> TerminalProfunctor c d
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> d
r
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> TerminalProfunctor a b -> r
\\ TerminalProfunctor a b
TerminalProfunctor = r
(Ob a, Ob b) => r
r

instance (CategoryOf k) => Promonad (TerminalProfunctor :: k +-> k) where
  id :: forall (a :: k). Ob a => TerminalProfunctor a a
id = TerminalProfunctor a a
forall {j} {k} (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor
  TerminalProfunctor b c
TerminalProfunctor . :: forall (b :: k) (c :: k) (a :: k).
TerminalProfunctor b c
-> TerminalProfunctor a b -> TerminalProfunctor a c
. TerminalProfunctor a b
TerminalProfunctor = TerminalProfunctor a c
forall {j} {k} (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor

instance (Monoidal j, Monoidal k) => MonoidalProfunctor (TerminalProfunctor :: j +-> k) where
  one :: TerminalProfunctor Unit Unit
one = Obj Unit -> Obj Unit -> TerminalProfunctor Unit Unit
forall j (a :: j) k (b :: k).
Obj a -> Obj b -> TerminalProfunctor a b
TerminalProfunctor' Obj Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one Obj Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one
  TerminalProfunctor' Obj x1
a1 Obj x2
b1 ** :: forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
TerminalProfunctor x1 x2
-> TerminalProfunctor y1 y2
-> TerminalProfunctor (x1 ** y1) (x2 ** y2)
** TerminalProfunctor' Obj y1
a2 Obj y2
b2 = Obj (x1 ** y1)
-> Obj (x2 ** y2) -> TerminalProfunctor (x1 ** y1) (x2 ** y2)
forall j (a :: j) k (b :: k).
Obj a -> Obj b -> TerminalProfunctor a b
TerminalProfunctor' (Obj x1
a1 Obj x1 -> Obj y1 -> Obj (x1 ** y1)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** Obj y1
a2) (Obj x2
b1 Obj x2 -> Obj y2 -> Obj (x2 ** y2)
forall (x1 :: j) (x2 :: j) (y1 :: j) (y2 :: j).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** Obj y2
b2)

instance (Dagger k) => DaggerProfunctor (TerminalProfunctor :: k +-> k) where
  dagger :: forall (a :: k) (b :: k).
TerminalProfunctor a b -> TerminalProfunctor b a
dagger TerminalProfunctor a b
TerminalProfunctor = TerminalProfunctor b a
forall {j} {k} (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor

pattern TerminalProfunctor
  :: forall {j} {k} a b. (CategoryOf j, CategoryOf k) => (Ob (a :: j), Ob (b :: k)) => TerminalProfunctor a b
pattern $bTerminalProfunctor :: forall {j} {k} (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
$mTerminalProfunctor :: forall {r} {j} {k} {a :: j} {b :: k}.
(CategoryOf j, CategoryOf k) =>
TerminalProfunctor a b -> ((Ob a, Ob b) => r) -> ((# #) -> r) -> r
TerminalProfunctor = TerminalProfunctor' Obj Obj

{-# COMPLETE TerminalProfunctor #-}

instance (CategoryOf j, CategoryOf k) => ThinProfunctor (TerminalProfunctor :: j +-> k)

instance (CategoryOf j, CategoryOf k) => DecidableProfunctor (TerminalProfunctor :: j +-> k) where
  type Holds TerminalProfunctor a b = TRU
  decide :: forall (a :: k) (b :: j).
(Ob a, Ob b) =>
Decision TerminalProfunctor a b (Holds TerminalProfunctor a b)
decide = TerminalProfunctor a b -> Decision TerminalProfunctor a b 'TRU
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Decision p a b 'TRU
Yes TerminalProfunctor a b
forall {j} {k} (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor
  toHolds :: forall (a :: k) (b :: j) r.
TerminalProfunctor a b
-> ((Holds TerminalProfunctor a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds TerminalProfunctor a b
TerminalProfunctor (Holds TerminalProfunctor a b ~ 'TRU, Ob a, Ob b) => r
r = r
(Holds TerminalProfunctor a b ~ 'TRU, Ob a, Ob b) => r
r