{-# 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