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' #-}