module Proarrow.Profunctor.Terminal (TerminalProfunctor(.., TerminalProfunctor')) where

import Proarrow.Core (PRO, Profunctor (..), CategoryOf(..))
import Proarrow.Object (Obj, obj)
import Proarrow.Category.Monoidal (MonoidalProfunctor(..), Monoidal (par))

type TerminalProfunctor :: PRO j k
data TerminalProfunctor a b where
  TerminalProfunctor :: (Ob a, Ob b) => TerminalProfunctor a b

instance (CategoryOf j, CategoryOf k) => Profunctor (TerminalProfunctor :: PRO j k) where
  dimap :: forall (c :: j) (a :: j) (b :: k) (d :: k).
(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).
(Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor ((Ob c, Ob a) => TerminalProfunctor c d)
-> (c ~> a) -> TerminalProfunctor c d
forall (a :: j) (b :: j) 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
\\ c ~> a
l ((Ob b, Ob d) => TerminalProfunctor c d)
-> (b ~> d) -> TerminalProfunctor c d
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
\\ b ~> d
r
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: k) r.
((Ob a, Ob b) => r) -> TerminalProfunctor a b -> r
\\ TerminalProfunctor a b
TerminalProfunctor = r
(Ob a, Ob b) => r
r

instance (Monoidal j, Monoidal k) => MonoidalProfunctor (TerminalProfunctor :: PRO j k) where
  lift0 :: TerminalProfunctor Unit Unit
lift0 = TerminalProfunctor Unit Unit
forall {j} {k} (a :: j) (b :: k).
(Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor
  lift2 :: forall (x1 :: j) (x2 :: k) (y1 :: j) (y2 :: k).
TerminalProfunctor x1 x2
-> TerminalProfunctor y1 y2
-> TerminalProfunctor (x1 ** y1) (x2 ** y2)
lift2 (TerminalProfunctor' Obj x1
a1 Obj x2
b1) (TerminalProfunctor' Obj y1
a2 Obj y2
b2) = Obj (x1 ** y1)
-> Obj (x2 ** y2) -> TerminalProfunctor (x1 ** y1) (x2 ** y2)
forall j k (a :: j) (b :: k).
(CategoryOf j, CategoryOf k) =>
Obj a -> Obj b -> TerminalProfunctor a b
TerminalProfunctor' (Obj x1
a1 Obj x1 -> Obj y1 -> Obj (x1 ** y1)
forall (a :: j) (b :: j) (c :: j) (d :: j).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Obj y1
a2) (Obj x2
b1 Obj x2 -> Obj y2 -> Obj (x2 ** y2)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Obj y2
b2)

getObs :: (CategoryOf j, CategoryOf k) => TerminalProfunctor (a :: j) (b :: k) -> (Obj a, Obj b)
getObs :: forall j k (a :: j) (b :: k).
(CategoryOf j, CategoryOf k) =>
TerminalProfunctor a b -> (Obj a, Obj b)
getObs TerminalProfunctor a b
TerminalProfunctor = (Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj, Obj b
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj)

pattern TerminalProfunctor' :: (CategoryOf j, CategoryOf k) => Obj (a :: j) -> Obj (b :: k) -> TerminalProfunctor a b
pattern $mTerminalProfunctor' :: forall {r} {j} {k} {a :: j} {b :: k}.
(CategoryOf j, CategoryOf k) =>
TerminalProfunctor a b
-> (Obj a -> Obj b -> r) -> ((# #) -> r) -> r
$bTerminalProfunctor' :: forall j k (a :: j) (b :: k).
(CategoryOf j, CategoryOf k) =>
Obj a -> Obj b -> TerminalProfunctor a b
TerminalProfunctor' x y <- (getObs -> (x, y)) where
  TerminalProfunctor' Obj a
a Obj b
b = TerminalProfunctor a b
(Ob a, Ob a) => TerminalProfunctor a b
forall {j} {k} (a :: j) (b :: k).
(Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor ((Ob a, Ob a) => TerminalProfunctor a b)
-> Obj a -> TerminalProfunctor a b
forall (a :: j) (b :: j) 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
\\ Obj a
a ((Ob b, Ob b) => TerminalProfunctor a b)
-> Obj b -> TerminalProfunctor a b
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
\\ Obj b
b

{-# COMPLETE TerminalProfunctor' #-}