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

import Proarrow.Category.Dagger (DaggerProfunctor (..))
import Proarrow.Category.Monoidal (Monoidal, MonoidalProfunctor (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), type (+->))
import Proarrow.Object (pattern Obj, type Obj)
import Proarrow.Preorder.ThinCategory (Codiscrete, ThinProfunctor (..))

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 :: 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 :: 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
\\ 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 (Monoidal j, Monoidal k) => MonoidalProfunctor (TerminalProfunctor :: j +-> k) where
  par0 :: TerminalProfunctor Unit Unit
par0 = 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
par0 Obj Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0
  TerminalProfunctor' Obj x1
a1 Obj x2
b1 par :: forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
TerminalProfunctor x1 x2
-> TerminalProfunctor y1 y2
-> TerminalProfunctor (x1 ** y1) (x2 ** y2)
`par` 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)
`par` 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)
`par` Obj y2
b2)

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

{-# COMPLETE TerminalProfunctor #-}

instance (CategoryOf j, CategoryOf k) => ThinProfunctor (TerminalProfunctor :: j +-> k) where
  arr :: forall (a :: k) (b :: j).
(Ob a, Ob b, HasArrow TerminalProfunctor a b) =>
TerminalProfunctor a b
arr = TerminalProfunctor a b
forall j k (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor
  withArr :: forall (a :: k) (b :: j) r.
TerminalProfunctor a b
-> (HasArrow TerminalProfunctor a b => r) -> r
withArr TerminalProfunctor a b
TerminalProfunctor HasArrow TerminalProfunctor a b => r
r = r
HasArrow TerminalProfunctor a b => r
r

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