{-# LANGUAGE AllowAmbiguousTypes #-} {-# OPTIONS_GHC -Wno-orphans #-} module Proarrow.Object.BinaryProduct where import Data.Kind (Type) import qualified Prelude as P import Proarrow.Category.Instance.Product ((:**:)(..)) import Proarrow.Category.Monoidal (Monoidal (..), SymMonoidal(..), MonoidalProfunctor (..)) import Proarrow.Core (PRO, CategoryOf(..), Promonad (..), Profunctor(..), UN, CAT, Is, dimapDefault) import Proarrow.Object (Obj, obj) import Proarrow.Object.Terminal (HasTerminalObject (..)) import Proarrow.Profunctor.Product ((:*:) (..), prod) import Proarrow.Category.Instance.Prof (Prof(..)) import Proarrow.Category.Instance.Unit qualified as U infixl 5 && infixl 5 &&& infixl 5 *** class CategoryOf k => HasBinaryProducts k where type (a :: k) && (b :: k) :: k fst' :: Obj (a :: k) -> Obj b -> a && b ~> a snd' :: Obj (a :: k) -> Obj b -> a && b ~> b (&&&) :: (a :: k) ~> x -> a ~> y -> a ~> x && y (***) :: forall a b x y. (a :: k) ~> x -> b ~> y -> a && b ~> x && y a ~> x l *** b ~> y r = (a ~> x l (a ~> x) -> ((a && b) ~> a) -> (a && b) ~> x 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 . forall (a :: k) (b :: k). (HasBinaryProducts k, Ob a, Ob b) => (a && b) ~> a forall {k} (a :: k) (b :: k). (HasBinaryProducts k, Ob a, Ob b) => (a && b) ~> a fst @a @b) ((a && b) ~> x) -> ((a && b) ~> y) -> (a && b) ~> (x && y) forall (a :: k) (x :: k) (y :: k). (a ~> x) -> (a ~> y) -> a ~> (x && y) forall k (a :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (a ~> y) -> a ~> (x && y) &&& (b ~> y r (b ~> y) -> ((a && b) ~> b) -> (a && b) ~> y 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 . forall (a :: k) (b :: k). (HasBinaryProducts k, Ob a, Ob b) => (a && b) ~> b forall {k} (a :: k) (b :: k). (HasBinaryProducts k, Ob a, Ob b) => (a && b) ~> b snd @a @b) ((Ob a, Ob x) => (a && b) ~> (x && y)) -> (a ~> x) -> (a && b) ~> (x && y) 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 ~> x l ((Ob b, Ob y) => (a && b) ~> (x && y)) -> (b ~> y) -> (a && b) ~> (x && y) 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 ~> y r fst :: forall {k} (a :: k) (b :: k). (HasBinaryProducts k, Ob a, Ob b) => (a && b) ~> a fst :: forall {k} (a :: k) (b :: k). (HasBinaryProducts k, Ob a, Ob b) => (a && b) ~> a fst = Obj a -> Obj b -> (a && b) ~> a forall (a :: k) (b :: k). Obj a -> Obj b -> (a && b) ~> a forall k (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> a fst' (forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @a) (forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @b) snd :: forall {k} (a :: k) (b :: k). (HasBinaryProducts k, Ob a, Ob b) => (a && b) ~> b snd :: forall {k} (a :: k) (b :: k). (HasBinaryProducts k, Ob a, Ob b) => (a && b) ~> b snd = Obj a -> Obj b -> (a && b) ~> b forall (a :: k) (b :: k). Obj a -> Obj b -> (a && b) ~> b forall k (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> b snd' (forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @a) (forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @b) first :: forall {k} (c :: k) (a :: k) (b :: k). (HasBinaryProducts k, Ob c) => a ~> b -> (a && c) ~> (b && c) first :: forall {k} (c :: k) (a :: k) (b :: k). (HasBinaryProducts k, Ob c) => (a ~> b) -> (a && c) ~> (b && c) first a ~> b f = a ~> b f (a ~> b) -> (c ~> c) -> (a && c) ~> (b && c) forall (a :: k) (b :: k) (x :: k) (y :: k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) *** forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @c second :: forall {k} (c :: k) (a :: k) (b :: k). (HasBinaryProducts k, Ob c) => a ~> b -> (c && a) ~> (c && b) second :: forall {k} (c :: k) (a :: k) (b :: k). (HasBinaryProducts k, Ob c) => (a ~> b) -> (c && a) ~> (c && b) second a ~> b f = forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @c Obj c -> (a ~> b) -> (c && a) ~> (c && b) forall (a :: k) (b :: k) (x :: k) (y :: k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) *** a ~> b f type HasProducts k = (HasTerminalObject k, HasBinaryProducts k) class a ** b ~ a && b => TensorIsProduct a b instance a ** b ~ a && b => TensorIsProduct a b class (HasProducts k, Monoidal k, (Unit :: k) ~ TerminalObject, forall (a :: k) (b :: k). TensorIsProduct a b) => Cartesian k instance (HasProducts k, Monoidal k, (Unit :: k) ~ TerminalObject, forall (a :: k) (b :: k). TensorIsProduct a b) => Cartesian k instance HasBinaryProducts Type where type a && b = (a, b) fst' :: forall a b. Obj a -> Obj b -> (a && b) ~> a fst' Obj a _ Obj b _ = (a && b) ~> a (a, b) -> a forall a b. (a, b) -> a P.fst snd' :: forall a b. Obj a -> Obj b -> (a && b) ~> b snd' Obj a _ Obj b _ = (a && b) ~> b (a, b) -> b forall a b. (a, b) -> b P.snd a ~> x f &&& :: forall a x y. (a ~> x) -> (a ~> y) -> a ~> (x && y) &&& a ~> y g = \a a -> (a ~> x a -> x f a a, a ~> y a -> y g a a) instance HasBinaryProducts U.UNIT where type U.U && U.U = U.U fst' :: forall (a :: UNIT) (b :: UNIT). Obj a -> Obj b -> (a && b) ~> a fst' Obj a Unit a a U.Unit Obj b Unit b b U.Unit = (a && b) ~> a Unit U U U.Unit snd' :: forall (a :: UNIT) (b :: UNIT). Obj a -> Obj b -> (a && b) ~> b snd' Obj a Unit a a U.Unit Obj b Unit b b U.Unit = (a && b) ~> b Unit U U U.Unit a ~> x Unit a x U.Unit &&& :: forall (a :: UNIT) (x :: UNIT) (y :: UNIT). (a ~> x) -> (a ~> y) -> a ~> (x && y) &&& a ~> y Unit U y U.Unit = a ~> (x && y) Unit U U U.Unit instance (HasBinaryProducts j, HasBinaryProducts k) => HasBinaryProducts (j, k) where type '(a1, a2) && '(b1, b2) = '(a1 && b1, a2 && b2) fst' :: forall (a :: (j, k)) (b :: (j, k)). Obj a -> Obj b -> (a && b) ~> a fst' (a1 ~> b1 a1 :**: a2 ~> b2 a2) (a1 ~> b1 b1 :**: a2 ~> b2 b2) = Obj b1 -> Obj b1 -> (b1 && b1) ~> b1 forall (a :: j) (b :: j). Obj a -> Obj b -> (a && b) ~> a forall k (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> a fst' a1 ~> b1 Obj b1 a1 a1 ~> b1 Obj b1 b1 ((b1 && b1) ~> b1) -> ((b2 && b2) ~> b2) -> (:**:) (~>) (~>) '(b1 && b1, b2 && b2) '(b1, b2) forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2) (a2 :: k2) (b2 :: k2). c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2) :**: Obj b2 -> Obj b2 -> (b2 && b2) ~> b2 forall (a :: k) (b :: k). Obj a -> Obj b -> (a && b) ~> a forall k (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> a fst' a2 ~> b2 Obj b2 a2 a2 ~> b2 Obj b2 b2 snd' :: forall (a :: (j, k)) (b :: (j, k)). Obj a -> Obj b -> (a && b) ~> b snd' (a1 ~> b1 a1 :**: a2 ~> b2 a2) (a1 ~> b1 b1 :**: a2 ~> b2 b2) = Obj b1 -> Obj b1 -> (b1 && b1) ~> b1 forall (a :: j) (b :: j). Obj a -> Obj b -> (a && b) ~> b forall k (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> b snd' a1 ~> b1 Obj b1 a1 a1 ~> b1 Obj b1 b1 ((b1 && b1) ~> b1) -> ((b2 && b2) ~> b2) -> (:**:) (~>) (~>) '(b1 && b1, b2 && b2) '(b1, b2) forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2) (a2 :: k2) (b2 :: k2). c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2) :**: Obj b2 -> Obj b2 -> (b2 && b2) ~> b2 forall (a :: k) (b :: k). Obj a -> Obj b -> (a && b) ~> b forall k (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> b snd' a2 ~> b2 Obj b2 a2 a2 ~> b2 Obj b2 b2 (a1 ~> b1 f1 :**: a2 ~> b2 f2) &&& :: forall (a :: (j, k)) (x :: (j, k)) (y :: (j, k)). (a ~> x) -> (a ~> y) -> a ~> (x && y) &&& (a1 ~> b1 g1 :**: a2 ~> b2 g2) = (a1 ~> b1 f1 (a1 ~> b1) -> (a1 ~> b1) -> a1 ~> (b1 && b1) forall (a :: j) (x :: j) (y :: j). (a ~> x) -> (a ~> y) -> a ~> (x && y) forall k (a :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (a ~> y) -> a ~> (x && y) &&& a1 ~> b1 a1 ~> b1 g1) (a1 ~> (b1 && b1)) -> (a2 ~> (b2 && b2)) -> (:**:) (~>) (~>) '(a1, a2) '(b1 && b1, b2 && b2) forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2) (a2 :: k2) (b2 :: k2). c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2) :**: (a2 ~> b2 f2 (a2 ~> b2) -> (a2 ~> b2) -> a2 ~> (b2 && b2) forall (a :: k) (x :: k) (y :: k). (a ~> x) -> (a ~> y) -> a ~> (x && y) forall k (a :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (a ~> y) -> a ~> (x && y) &&& a2 ~> b2 a2 ~> b2 g2) instance (CategoryOf j, CategoryOf k) => HasBinaryProducts (PRO j k) where type p && q = p :*: q fst' :: forall (a :: PRO j k) (b :: PRO j k). Obj a -> Obj b -> (a && b) ~> a fst' Prof{} Prof{} = ((a :*: b) :~> a) -> Prof (a :*: b) a forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof (:*:) a b a b -> a a b (a :*: b) :~> a forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (q :: PRO j k). (:*:) p q a b -> p a b fstP snd' :: forall (a :: PRO j k) (b :: PRO j k). Obj a -> Obj b -> (a && b) ~> b snd' Prof{} Prof{} = ((a :*: b) :~> b) -> Prof (a :*: b) b forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof (:*:) a b a b -> b a b (a :*: b) :~> b forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (q :: PRO j k). (:*:) p q a b -> q a b sndP Prof a :~> x l &&& :: forall (a :: PRO j k) (x :: PRO j k) (y :: PRO j k). (a ~> x) -> (a ~> y) -> a ~> (x && y) &&& Prof a :~> y r = (a :~> (x :*: y)) -> Prof a (x :*: y) forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof ((a :~> x) -> (a :~> y) -> a :~> (x :*: y) forall {j} {k} (r :: j -> k -> Type) (p :: j -> k -> Type) (q :: j -> k -> Type). (r :~> p) -> (r :~> q) -> r :~> (p :*: q) prod a a b -> x a b a :~> x l a a b -> y a b a :~> y r) leftUnitorProd :: HasProducts k => Obj (a :: k) -> TerminalObject && a ~> a leftUnitorProd :: forall k (a :: k). HasProducts k => Obj a -> (TerminalObject && a) ~> a leftUnitorProd = Obj TerminalObject -> (a ~> a) -> (TerminalObject && a) ~> a forall (a :: k) (b :: k). Obj a -> Obj b -> (a && b) ~> b forall k (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> b snd' (forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @TerminalObject) leftUnitorProdInv :: HasProducts k => Obj (a :: k) -> a ~> TerminalObject && a leftUnitorProdInv :: forall k (a :: k). HasProducts k => Obj a -> a ~> (TerminalObject && a) leftUnitorProdInv Obj a a = Obj a -> a ~> TerminalObject forall (a :: k). Obj a -> a ~> TerminalObject forall k (a :: k). HasTerminalObject k => Obj a -> a ~> TerminalObject terminate' Obj a a (a ~> TerminalObject) -> Obj a -> a ~> (TerminalObject && a) forall (a :: k) (x :: k) (y :: k). (a ~> x) -> (a ~> y) -> a ~> (x && y) forall k (a :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (a ~> y) -> a ~> (x && y) &&& Obj a a rightUnitorProd :: HasProducts k => Obj (a :: k) -> a && TerminalObject ~> a rightUnitorProd :: forall k (a :: k). HasProducts k => Obj a -> (a && TerminalObject) ~> a rightUnitorProd Obj a a = Obj a -> Obj TerminalObject -> (a && TerminalObject) ~> a forall (a :: k) (b :: k). Obj a -> Obj b -> (a && b) ~> a forall k (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> a fst' Obj a a (forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @TerminalObject) rightUnitorProdInv :: HasProducts k => Obj (a :: k) -> a ~> a && TerminalObject rightUnitorProdInv :: forall k (a :: k). HasProducts k => Obj a -> a ~> (a && TerminalObject) rightUnitorProdInv Obj a a = Obj a a Obj a -> (a ~> TerminalObject) -> a ~> (a && TerminalObject) forall (a :: k) (x :: k) (y :: k). (a ~> x) -> (a ~> y) -> a ~> (x && y) forall k (a :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (a ~> y) -> a ~> (x && y) &&& Obj a -> a ~> TerminalObject forall (a :: k). Obj a -> a ~> TerminalObject forall k (a :: k). HasTerminalObject k => Obj a -> a ~> TerminalObject terminate' Obj a a associatorProd :: HasProducts k => Obj (a :: k) -> Obj b -> Obj c -> (a && b) && c ~> a && (b && c) associatorProd :: forall k (a :: k) (b :: k) (c :: k). HasProducts k => Obj a -> Obj b -> Obj c -> ((a && b) && c) ~> (a && (b && c)) associatorProd Obj a a Obj b b Obj c c = (Obj a -> Obj b -> (a && b) ~> a forall (a :: k) (b :: k). Obj a -> Obj b -> (a && b) ~> a forall k (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> a fst' Obj a a Obj b b ((a && b) ~> a) -> (((a && b) && c) ~> (a && b)) -> ((a && b) && c) ~> a 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 . Obj (a && b) -> Obj c -> ((a && b) && c) ~> (a && b) forall (a :: k) (b :: k). Obj a -> Obj b -> (a && b) ~> a forall k (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> a fst' (Obj a a Obj a -> Obj b -> Obj (a && b) forall (a :: k) (b :: k) (x :: k) (y :: k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) *** Obj b b) Obj c c) (((a && b) && c) ~> a) -> (((a && b) && c) ~> (b && c)) -> ((a && b) && c) ~> (a && (b && c)) forall (a :: k) (x :: k) (y :: k). (a ~> x) -> (a ~> y) -> a ~> (x && y) forall k (a :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (a ~> y) -> a ~> (x && y) &&& (Obj a -> Obj b -> (a && b) ~> b forall (a :: k) (b :: k). Obj a -> Obj b -> (a && b) ~> b forall k (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> b snd' Obj a a Obj b b ((a && b) ~> b) -> Obj c -> ((a && b) && c) ~> (b && c) forall (a :: k) (b :: k) (x :: k) (y :: k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) *** Obj c c) ((Ob (a && b), Ob (a && b)) => ((a && b) && c) ~> (a && (b && c))) -> Obj (a && b) -> ((a && b) && c) ~> (a && (b && c)) 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 a a Obj a -> Obj b -> Obj (a && b) forall (a :: k) (b :: k) (x :: k) (y :: k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) *** Obj b b) associatorProdInv :: HasProducts k => Obj (a :: k) -> Obj b -> Obj c -> a && (b && c) ~> (a && b) && c associatorProdInv :: forall k (a :: k) (b :: k) (c :: k). HasProducts k => Obj a -> Obj b -> Obj c -> (a && (b && c)) ~> ((a && b) && c) associatorProdInv Obj a a Obj b b Obj c c = (Obj a a Obj a -> ((b && c) ~> b) -> (a && (b && c)) ~> (a && b) forall (a :: k) (b :: k) (x :: k) (y :: k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) *** Obj b -> Obj c -> (b && c) ~> b forall (a :: k) (b :: k). Obj a -> Obj b -> (a && b) ~> a forall k (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> a fst' Obj b b Obj c c) ((a && (b && c)) ~> (a && b)) -> ((a && (b && c)) ~> c) -> (a && (b && c)) ~> ((a && b) && c) forall (a :: k) (x :: k) (y :: k). (a ~> x) -> (a ~> y) -> a ~> (x && y) forall k (a :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (a ~> y) -> a ~> (x && y) &&& (Obj b -> Obj c -> (b && c) ~> c forall (a :: k) (b :: k). Obj a -> Obj b -> (a && b) ~> b forall k (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> b snd' Obj b b Obj c c ((b && c) ~> c) -> ((a && (b && c)) ~> (b && c)) -> (a && (b && c)) ~> c 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 . Obj a -> Obj (b && c) -> (a && (b && c)) ~> (b && c) forall (a :: k) (b :: k). Obj a -> Obj b -> (a && b) ~> b forall k (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> b snd' Obj a a (Obj b b Obj b -> Obj c -> Obj (b && c) forall (a :: k) (b :: k) (x :: k) (y :: k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) *** Obj c c)) ((Ob (a && b), Ob (a && b)) => (a && (b && c)) ~> ((a && b) && c)) -> ((a && b) ~> (a && b)) -> (a && (b && c)) ~> ((a && b) && c) 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 a a Obj a -> Obj b -> (a && b) ~> (a && b) forall (a :: k) (b :: k) (x :: k) (y :: k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) *** Obj b b) swapProd :: forall {k} (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> (b && a) swapProd :: forall {k} (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> (b && a) swapProd Obj a a Obj b b = Obj a -> Obj b -> (a && b) ~> b forall (a :: k) (b :: k). Obj a -> Obj b -> (a && b) ~> b forall k (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> b snd' Obj a a Obj b b ((a && b) ~> b) -> ((a && b) ~> a) -> (a && b) ~> (b && a) forall (a :: k) (x :: k) (y :: k). (a ~> x) -> (a ~> y) -> a ~> (x && y) forall k (a :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (a ~> y) -> a ~> (x && y) &&& Obj a -> Obj b -> (a && b) ~> a forall (a :: k) (b :: k). Obj a -> Obj b -> (a && b) ~> a forall k (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> a fst' Obj a a Obj b b newtype PROD k = PR k type instance UN PR (PR k) = k type Prod :: CAT (PROD k) data Prod (a :: PROD k) b where Prod :: (Ob a, Ob b) => UN PR a ~> UN PR b -> Prod a b mkProd :: CategoryOf k => (a :: k) ~> b -> Prod (PR a) (PR b) mkProd :: forall k (a :: k) (b :: k). CategoryOf k => (a ~> b) -> Prod ('PR a) ('PR b) mkProd a ~> b f = (UN 'PR ('PR a) ~> UN 'PR ('PR b)) -> Prod ('PR a) ('PR b) forall {j} (a :: PROD j) (b :: PROD j). (Ob a, Ob b) => (UN 'PR a ~> UN 'PR b) -> Prod a b Prod a ~> b UN 'PR ('PR a) ~> UN 'PR ('PR b) f ((Ob a, Ob b) => Prod ('PR a) ('PR b)) -> (a ~> b) -> Prod ('PR a) ('PR 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 \\ a ~> b f instance CategoryOf k => Profunctor (Prod :: CAT (PROD k)) where dimap :: forall (c :: PROD k) (a :: PROD k) (b :: PROD k) (d :: PROD k). (c ~> a) -> (b ~> d) -> Prod a b -> Prod c d dimap = (c ~> a) -> (b ~> d) -> Prod a b -> Prod c d Prod c a -> Prod b d -> Prod a b -> Prod c d forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k). Promonad p => p c a -> p b d -> p a b -> p c d dimapDefault (Ob a, Ob b) => r r \\ :: forall (a :: PROD k) (b :: PROD k) r. ((Ob a, Ob b) => r) -> Prod a b -> r \\ Prod UN 'PR a ~> UN 'PR b f = r (Ob (UN 'PR a), Ob (UN 'PR b)) => r (Ob a, Ob b) => r r ((Ob (UN 'PR a), Ob (UN 'PR b)) => r) -> (UN 'PR a ~> UN 'PR b) -> r 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 \\ UN 'PR a ~> UN 'PR b f instance CategoryOf k => Promonad (Prod :: CAT (PROD k)) where id :: forall (a :: PROD k). Ob a => Prod a a id = (UN 'PR a ~> UN 'PR a) -> Prod a a forall {j} (a :: PROD j) (b :: PROD j). (Ob a, Ob b) => (UN 'PR a ~> UN 'PR b) -> Prod a b Prod UN 'PR a ~> UN 'PR a forall (a :: k). Ob a => a ~> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id Prod UN 'PR b ~> UN 'PR c f . :: forall (b :: PROD k) (c :: PROD k) (a :: PROD k). Prod b c -> Prod a b -> Prod a c . Prod UN 'PR a ~> UN 'PR b g = (UN 'PR a ~> UN 'PR c) -> Prod a c forall {j} (a :: PROD j) (b :: PROD j). (Ob a, Ob b) => (UN 'PR a ~> UN 'PR b) -> Prod a b Prod (UN 'PR b ~> UN 'PR c f (UN 'PR b ~> UN 'PR c) -> (UN 'PR a ~> UN 'PR b) -> UN 'PR a ~> UN 'PR c 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 . UN 'PR a ~> UN 'PR b g) instance CategoryOf k => CategoryOf (PROD k) where type (~>) = Prod type Ob a = (Is PR a, Ob (UN PR a)) instance HasTerminalObject k => HasTerminalObject (PROD k) where type TerminalObject = PR TerminalObject terminate' :: forall (a :: PROD k). Obj a -> a ~> TerminalObject terminate' (Prod UN 'PR a ~> UN 'PR a a) = (UN 'PR ('PR (UN 'PR a)) ~> UN 'PR ('PR TerminalObject)) -> Prod ('PR (UN 'PR a)) ('PR TerminalObject) forall {j} (a :: PROD j) (b :: PROD j). (Ob a, Ob b) => (UN 'PR a ~> UN 'PR b) -> Prod a b Prod ((UN 'PR a ~> UN 'PR a) -> UN 'PR a ~> TerminalObject forall (a :: k). Obj a -> a ~> TerminalObject forall k (a :: k). HasTerminalObject k => Obj a -> a ~> TerminalObject terminate' UN 'PR a ~> UN 'PR a a) instance HasBinaryProducts k => HasBinaryProducts (PROD k) where type a && b = PR (UN PR a && UN PR b) fst' :: forall (a :: PROD k) (b :: PROD k). Obj a -> Obj b -> (a && b) ~> a fst' (Prod UN 'PR a ~> UN 'PR a a) (Prod UN 'PR b ~> UN 'PR b b) = ((UN 'PR a && UN 'PR b) ~> UN 'PR a) -> Prod ('PR (UN 'PR a && UN 'PR b)) ('PR (UN 'PR a)) forall k (a :: k) (b :: k). CategoryOf k => (a ~> b) -> Prod ('PR a) ('PR b) mkProd ((UN 'PR a ~> UN 'PR a) -> (UN 'PR b ~> UN 'PR b) -> (UN 'PR a && UN 'PR b) ~> UN 'PR a forall (a :: k) (b :: k). Obj a -> Obj b -> (a && b) ~> a forall k (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> a fst' UN 'PR a ~> UN 'PR a a UN 'PR b ~> UN 'PR b b) snd' :: forall (a :: PROD k) (b :: PROD k). Obj a -> Obj b -> (a && b) ~> b snd' (Prod UN 'PR a ~> UN 'PR a a) (Prod UN 'PR b ~> UN 'PR b b) = ((UN 'PR a && UN 'PR b) ~> UN 'PR b) -> Prod ('PR (UN 'PR a && UN 'PR b)) ('PR (UN 'PR b)) forall k (a :: k) (b :: k). CategoryOf k => (a ~> b) -> Prod ('PR a) ('PR b) mkProd ((UN 'PR a ~> UN 'PR a) -> (UN 'PR b ~> UN 'PR b) -> (UN 'PR a && UN 'PR b) ~> UN 'PR b forall (a :: k) (b :: k). Obj a -> Obj b -> (a && b) ~> b forall k (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> b snd' UN 'PR a ~> UN 'PR a a UN 'PR b ~> UN 'PR b b) Prod UN 'PR a ~> UN 'PR x f &&& :: forall (a :: PROD k) (x :: PROD k) (y :: PROD k). (a ~> x) -> (a ~> y) -> a ~> (x && y) &&& Prod UN 'PR ('PR (UN 'PR a)) ~> UN 'PR y g = (UN 'PR a ~> (UN 'PR x && UN 'PR y)) -> Prod ('PR (UN 'PR a)) ('PR (UN 'PR x && UN 'PR y)) forall k (a :: k) (b :: k). CategoryOf k => (a ~> b) -> Prod ('PR a) ('PR b) mkProd (UN 'PR a ~> UN 'PR x f (UN 'PR a ~> UN 'PR x) -> (UN 'PR a ~> UN 'PR y) -> UN 'PR a ~> (UN 'PR x && UN 'PR y) forall (a :: k) (x :: k) (y :: k). (a ~> x) -> (a ~> y) -> a ~> (x && y) forall k (a :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (a ~> y) -> a ~> (x && y) &&& UN 'PR a ~> UN 'PR y UN 'PR ('PR (UN 'PR a)) ~> UN 'PR y g) Prod UN 'PR a ~> UN 'PR x f *** :: forall (a :: PROD k) (b :: PROD k) (x :: PROD k) (y :: PROD k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) *** Prod UN 'PR b ~> UN 'PR y g = ((UN 'PR a && UN 'PR b) ~> (UN 'PR x && UN 'PR y)) -> Prod ('PR (UN 'PR a && UN 'PR b)) ('PR (UN 'PR x && UN 'PR y)) forall k (a :: k) (b :: k). CategoryOf k => (a ~> b) -> Prod ('PR a) ('PR b) mkProd (UN 'PR a ~> UN 'PR x f (UN 'PR a ~> UN 'PR x) -> (UN 'PR b ~> UN 'PR y) -> (UN 'PR a && UN 'PR b) ~> (UN 'PR x && UN 'PR y) forall (a :: k) (b :: k) (x :: k) (y :: k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) *** UN 'PR b ~> UN 'PR y g) instance HasProducts k => Monoidal (PROD k) where type Unit = TerminalObject type a ** b = a && b a ~> b f par :: forall (a :: PROD k) (b :: PROD k) (c :: PROD k) (d :: PROD k). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` c ~> d g = a ~> b f (a ~> b) -> (c ~> d) -> (a && c) ~> (b && d) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) forall (a :: PROD k) (b :: PROD k) (x :: PROD k) (y :: PROD k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) *** c ~> d g leftUnitor :: forall (a :: PROD k). Obj a -> (Unit ** a) ~> a leftUnitor = (a ~> a) -> (Unit ** a) ~> a (a ~> a) -> (TerminalObject && a) ~> a forall k (a :: k). HasProducts k => Obj a -> (TerminalObject && a) ~> a leftUnitorProd leftUnitorInv :: forall (a :: PROD k). Obj a -> a ~> (Unit ** a) leftUnitorInv = (a ~> a) -> a ~> (Unit ** a) (a ~> a) -> a ~> (TerminalObject && a) forall k (a :: k). HasProducts k => Obj a -> a ~> (TerminalObject && a) leftUnitorProdInv rightUnitor :: forall (a :: PROD k). Obj a -> (a ** Unit) ~> a rightUnitor = (a ~> a) -> (a ** Unit) ~> a (a ~> a) -> (a && TerminalObject) ~> a forall k (a :: k). HasProducts k => Obj a -> (a && TerminalObject) ~> a rightUnitorProd rightUnitorInv :: forall (a :: PROD k). Obj a -> a ~> (a ** Unit) rightUnitorInv = (a ~> a) -> a ~> (a ** Unit) (a ~> a) -> a ~> (a && TerminalObject) forall k (a :: k). HasProducts k => Obj a -> a ~> (a && TerminalObject) rightUnitorProdInv associator :: forall (a :: PROD k) (b :: PROD k) (c :: PROD k). Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c)) associator = (a ~> a) -> (b ~> b) -> (c ~> c) -> ((a ** b) ** c) ~> (a ** (b ** c)) (a ~> a) -> (b ~> b) -> (c ~> c) -> ((a && b) && c) ~> (a && (b && c)) forall k (a :: k) (b :: k) (c :: k). HasProducts k => Obj a -> Obj b -> Obj c -> ((a && b) && c) ~> (a && (b && c)) associatorProd associatorInv :: forall (a :: PROD k) (b :: PROD k) (c :: PROD k). Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c) associatorInv = (a ~> a) -> (b ~> b) -> (c ~> c) -> (a ** (b ** c)) ~> ((a ** b) ** c) (a ~> a) -> (b ~> b) -> (c ~> c) -> (a && (b && c)) ~> ((a && b) && c) forall k (a :: k) (b :: k) (c :: k). HasProducts k => Obj a -> Obj b -> Obj c -> (a && (b && c)) ~> ((a && b) && c) associatorProdInv instance HasProducts k => SymMonoidal (PROD k) where swap' :: forall (a :: PROD k) (b :: PROD k). Obj a -> Obj b -> (a ** b) ~> (b ** a) swap' (Prod UN 'PR a ~> UN 'PR a a) (Prod UN 'PR b ~> UN 'PR b b) = ((UN 'PR a && UN 'PR b) ~> (UN 'PR b && UN 'PR a)) -> Prod ('PR (UN 'PR a && UN 'PR b)) ('PR (UN 'PR b && UN 'PR a)) forall k (a :: k) (b :: k). CategoryOf k => (a ~> b) -> Prod ('PR a) ('PR b) mkProd ((UN 'PR a ~> UN 'PR a) -> (UN 'PR b ~> UN 'PR b) -> (UN 'PR a && UN 'PR b) ~> (UN 'PR b && UN 'PR a) forall {k} (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> (b && a) swapProd UN 'PR a ~> UN 'PR a a UN 'PR b ~> UN 'PR b b) instance HasProducts k => MonoidalProfunctor (Prod :: CAT (PROD k)) where lift0 :: Prod Unit Unit lift0 = Prod Unit Unit Prod ('PR TerminalObject) ('PR TerminalObject) forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a forall (a :: PROD k). Ob a => Prod a a id lift2 :: forall (x1 :: PROD k) (x2 :: PROD k) (y1 :: PROD k) (y2 :: PROD k). Prod x1 x2 -> Prod y1 y2 -> Prod (x1 ** y1) (x2 ** y2) lift2 = (x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2) Prod x1 x2 -> Prod y1 y2 -> Prod (x1 ** y1) (x2 ** y2) forall k (a :: k) (b :: k) (c :: k) (d :: k). Monoidal k => (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) forall (a :: PROD k) (b :: PROD k) (c :: PROD k) (d :: PROD k). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) par instance Monoidal Type where type Unit = TerminalObject type a ** b = a && b a ~> b f par :: forall a b c d. (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` c ~> d g = a ~> b f (a ~> b) -> (c ~> d) -> (a && c) ~> (b && d) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) forall a b x y. (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) *** c ~> d g leftUnitor :: forall a. Obj a -> (Unit ** a) ~> a leftUnitor = (a ~> a) -> (Unit ** a) ~> a (a ~> a) -> (TerminalObject && a) ~> a forall k (a :: k). HasProducts k => Obj a -> (TerminalObject && a) ~> a leftUnitorProd leftUnitorInv :: forall a. Obj a -> a ~> (Unit ** a) leftUnitorInv = (a ~> a) -> a ~> (Unit ** a) (a ~> a) -> a ~> (TerminalObject && a) forall k (a :: k). HasProducts k => Obj a -> a ~> (TerminalObject && a) leftUnitorProdInv rightUnitor :: forall a. Obj a -> (a ** Unit) ~> a rightUnitor = (a ~> a) -> (a ** Unit) ~> a (a ~> a) -> (a && TerminalObject) ~> a forall k (a :: k). HasProducts k => Obj a -> (a && TerminalObject) ~> a rightUnitorProd rightUnitorInv :: forall a. Obj a -> a ~> (a ** Unit) rightUnitorInv = (a ~> a) -> a ~> (a ** Unit) (a ~> a) -> a ~> (a && TerminalObject) forall k (a :: k). HasProducts k => Obj a -> a ~> (a && TerminalObject) rightUnitorProdInv associator :: forall a b c. Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c)) associator = (a ~> a) -> (b ~> b) -> (c ~> c) -> ((a ** b) ** c) ~> (a ** (b ** c)) (a ~> a) -> (b ~> b) -> (c ~> c) -> ((a && b) && c) ~> (a && (b && c)) forall k (a :: k) (b :: k) (c :: k). HasProducts k => Obj a -> Obj b -> Obj c -> ((a && b) && c) ~> (a && (b && c)) associatorProd associatorInv :: forall a b c. Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c) associatorInv = (a ~> a) -> (b ~> b) -> (c ~> c) -> (a ** (b ** c)) ~> ((a ** b) ** c) (a ~> a) -> (b ~> b) -> (c ~> c) -> (a && (b && c)) ~> ((a && b) && c) forall k (a :: k) (b :: k) (c :: k). HasProducts k => Obj a -> Obj b -> Obj c -> (a && (b && c)) ~> ((a && b) && c) associatorProdInv instance SymMonoidal Type where swap' :: forall a b. Obj a -> Obj b -> (a ** b) ~> (b ** a) swap' = (a ~> a) -> (b ~> b) -> (a ** b) ~> (b ** a) (a ~> a) -> (b ~> b) -> (a && b) ~> (b && a) forall {k} (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> (b && a) swapProd instance MonoidalProfunctor (->) where lift0 :: Unit -> Unit lift0 = () -> () Unit -> Unit forall a. Ob a => a -> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id lift2 :: forall x1 x2 y1 y2. (x1 -> x2) -> (y1 -> y2) -> (x1 ** y1) -> (x2 ** y2) lift2 = (x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2) (x1 -> x2) -> (y1 -> y2) -> (x1 ** y1) -> x2 ** y2 forall k (a :: k) (b :: k) (c :: k) (d :: k). Monoidal k => (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) forall a b c d. (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) par instance Monoidal U.UNIT where type Unit = TerminalObject type a ** b = a && b a ~> b f par :: forall (a :: UNIT) (b :: UNIT) (c :: UNIT) (d :: UNIT). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` c ~> d g = a ~> b f (a ~> b) -> (c ~> d) -> (a && c) ~> (b && d) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryProducts k => (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) forall (a :: UNIT) (b :: UNIT) (x :: UNIT) (y :: UNIT). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) *** c ~> d g leftUnitor :: forall (a :: UNIT). Obj a -> (Unit ** a) ~> a leftUnitor = (a ~> a) -> (Unit ** a) ~> a (a ~> a) -> (TerminalObject && a) ~> a forall k (a :: k). HasProducts k => Obj a -> (TerminalObject && a) ~> a leftUnitorProd leftUnitorInv :: forall (a :: UNIT). Obj a -> a ~> (Unit ** a) leftUnitorInv = (a ~> a) -> a ~> (Unit ** a) (a ~> a) -> a ~> (TerminalObject && a) forall k (a :: k). HasProducts k => Obj a -> a ~> (TerminalObject && a) leftUnitorProdInv rightUnitor :: forall (a :: UNIT). Obj a -> (a ** Unit) ~> a rightUnitor = (a ~> a) -> (a ** Unit) ~> a (a ~> a) -> (a && TerminalObject) ~> a forall k (a :: k). HasProducts k => Obj a -> (a && TerminalObject) ~> a rightUnitorProd rightUnitorInv :: forall (a :: UNIT). Obj a -> a ~> (a ** Unit) rightUnitorInv = (a ~> a) -> a ~> (a ** Unit) (a ~> a) -> a ~> (a && TerminalObject) forall k (a :: k). HasProducts k => Obj a -> a ~> (a && TerminalObject) rightUnitorProdInv associator :: forall (a :: UNIT) (b :: UNIT) (c :: UNIT). Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c)) associator = (a ~> a) -> (b ~> b) -> (c ~> c) -> ((a ** b) ** c) ~> (a ** (b ** c)) (a ~> a) -> (b ~> b) -> (c ~> c) -> ((a && b) && c) ~> (a && (b && c)) forall k (a :: k) (b :: k) (c :: k). HasProducts k => Obj a -> Obj b -> Obj c -> ((a && b) && c) ~> (a && (b && c)) associatorProd associatorInv :: forall (a :: UNIT) (b :: UNIT) (c :: UNIT). Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c) associatorInv = (a ~> a) -> (b ~> b) -> (c ~> c) -> (a ** (b ** c)) ~> ((a ** b) ** c) (a ~> a) -> (b ~> b) -> (c ~> c) -> (a && (b && c)) ~> ((a && b) && c) forall k (a :: k) (b :: k) (c :: k). HasProducts k => Obj a -> Obj b -> Obj c -> (a && (b && c)) ~> ((a && b) && c) associatorProdInv instance SymMonoidal U.UNIT where swap' :: forall (a :: UNIT) (b :: UNIT). Obj a -> Obj b -> (a ** b) ~> (b ** a) swap' = (a ~> a) -> (b ~> b) -> (a ** b) ~> (b ** a) (a ~> a) -> (b ~> b) -> (a && b) ~> (b && a) forall {k} (a :: k) (b :: k). HasBinaryProducts k => Obj a -> Obj b -> (a && b) ~> (b && a) swapProd instance MonoidalProfunctor U.Unit where lift0 :: Unit Unit Unit lift0 = Unit Unit Unit Unit U U forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a forall (a :: UNIT). Ob a => Unit a a id lift2 :: forall (x1 :: UNIT) (x2 :: UNIT) (y1 :: UNIT) (y2 :: UNIT). Unit x1 x2 -> Unit y1 y2 -> Unit (x1 ** y1) (x2 ** y2) lift2 = (x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2) Unit x1 x2 -> Unit y1 y2 -> Unit (x1 ** y1) (x2 ** y2) forall k (a :: k) (b :: k) (c :: k) (d :: k). Monoidal k => (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) forall (a :: UNIT) (b :: UNIT) (c :: UNIT) (d :: UNIT). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) par