{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Object.BinaryProduct where

import Data.Kind (Type)
import Prelude (type (~))
import Prelude qualified as P

import Proarrow.Category.Instance.Product (Fst, Snd, (:**:) (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , SymMonoidal (..)
  , TracedMonoidalProfunctor (..)
  )
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), Strong (..))
import Proarrow.Core (CAT, Category, CategoryOf (..), Is, PRO, Profunctor (..), Promonad (..), UN, src, type (+->))
import Proarrow.Object (Obj, obj)
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Product (prod, (:*:) (..))

infixl 5 &&
infixl 5 &&&
infixl 5 ***

class (CategoryOf k) => HasBinaryProducts k where
  {-# MINIMAL (fst | fst'), (snd | snd'), (&&&) #-}
  type (a :: k) && (b :: k) :: k

  fst :: (Ob (a :: k), Ob b) => (a && b) ~> a
  fst @a @b = (a ~> a) -> Obj b -> (a && b) ~> a
forall (a :: k) (a' :: k) (b :: k).
(a ~> a') -> Obj b -> (a && b) ~> a'
forall k (a :: k) (a' :: k) (b :: k).
HasBinaryProducts k =>
(a ~> 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)
  fst' :: (a :: k) ~> a' -> Obj b -> a && b ~> a'
  fst' @a @_ @b a ~> a'
a Obj b
b = a ~> a'
a (a ~> a') -> ((a && b) ~> a) -> (a && b) ~> 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
. forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @a @b ((Ob a, Ob a') => (a && b) ~> a') -> (a ~> a') -> (a && b) ~> a'
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 ~> a'
a ((Ob b, Ob b) => (a && b) ~> a') -> Obj b -> (a && b) ~> a'
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

  snd :: (Ob (a :: k), Ob b) => (a && b) ~> b
  snd @a @b = Obj a -> (b ~> b) -> (a && b) ~> b
forall (a :: k) (b :: k) (b' :: k).
Obj a -> (b ~> b') -> (a && b) ~> b'
forall k (a :: k) (b :: k) (b' :: k).
HasBinaryProducts k =>
Obj a -> (b ~> 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)
  snd' :: Obj (a :: k) -> b ~> b' -> a && b ~> b'
  snd' @a @b Obj a
a b ~> b'
b = b ~> b'
b (b ~> b') -> ((a && b) ~> b) -> (a && b) ~> b'
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 k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @a @b ((Ob a, Ob a) => (a && b) ~> b') -> Obj a -> (a && b) ~> 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 a
a ((Ob b, Ob b') => (a && b) ~> b') -> (b ~> b') -> (a && b) ~> 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
\\ b ~> 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 k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @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 k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @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

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

diag :: forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> a && a
diag :: forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
diag = a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id (a ~> a) -> (a ~> a) -> a ~> (a && 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)
&&& a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id

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. (Ob a, Ob b) => (a && b) ~> a
fst = (a && b) ~> a
(a, b) -> a
forall a b. (a, b) -> a
P.fst
  snd :: forall a b. (Ob a, Ob b) => (a && b) ~> b
snd = (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 () where
  type '() && '() = '()
  fst :: forall (a :: ()) (b :: ()). (Ob a, Ob b) => (a && b) ~> a
fst = (a && b) ~> a
Unit '() '()
U.Unit
  snd :: forall (a :: ()) (b :: ()). (Ob a, Ob b) => (a && b) ~> b
snd = (a && b) ~> b
Unit '() '()
U.Unit
  a ~> x
Unit a x
U.Unit &&& :: forall (a :: ()) (x :: ()) (y :: ()).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> y
Unit '() y
U.Unit = a ~> (x && y)
Unit '() '()
U.Unit

instance (HasBinaryProducts j, HasBinaryProducts k) => HasBinaryProducts (j, k) where
  type a && b = '(Fst a && Fst b, Snd a && Snd b)
  fst :: forall (a :: (j, k)) (b :: (j, k)). (Ob a, Ob b) => (a && b) ~> a
fst @'(a1, a2) @'(b1, b2) = forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @a1 @b1 ((Fst a && Fst b) ~> Fst a)
-> ((Snd a && Snd b) ~> Snd a)
-> (:**:)
     (~>) (~>) '(Fst a && Fst b, Snd a && Snd b) '(Fst a, Snd a)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @a2 @b2
  snd :: forall (a :: (j, k)) (b :: (j, k)). (Ob a, Ob b) => (a && b) ~> b
snd @a @b = forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @(Fst a) @(Fst b) ((Fst a && Fst b) ~> Fst b)
-> ((Snd a && Snd b) ~> Snd b)
-> (:**:)
     (~>) (~>) '(Fst a && Fst b, Snd a && Snd b) '(Fst b, Snd b)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @(Snd a) @(Snd b)
  (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 {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
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). (Ob a, Ob b) => (a && b) ~> a
fst = ((a :*: b) :~> a) -> Prof (a :*: b) a
forall {k} {j} (p :: j +-> k) (q :: 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). (Ob a, Ob b) => (a && b) ~> b
snd = ((a :*: b) :~> b) -> Prof (a :*: b) b
forall {k} {j} (p :: j +-> k) (q :: 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 {k} {j} (p :: j +-> k) (q :: 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 :: forall {k} (a :: k). (HasProducts k, Ob a) => TerminalObject && a ~> a
leftUnitorProd :: forall {k} (a :: k).
(HasProducts k, Ob a) =>
(TerminalObject && a) ~> a
leftUnitorProd = forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @TerminalObject

leftUnitorProdInv :: forall {k} (a :: k). (HasProducts k, Ob a) => a ~> TerminalObject && a
leftUnitorProdInv :: forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (TerminalObject && a)
leftUnitorProdInv = a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate (a ~> TerminalObject) -> (a ~> 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)
&&& a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id

rightUnitorProd :: forall {k} (a :: k). (HasProducts k, Ob a) => a && TerminalObject ~> a
rightUnitorProd :: forall {k} (a :: k).
(HasProducts k, Ob a) =>
(a && TerminalObject) ~> a
rightUnitorProd = forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @_ @TerminalObject

rightUnitorProdInv :: forall {k} (a :: k). (HasProducts k, Ob a) => a ~> a && TerminalObject
rightUnitorProdInv :: forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (a && TerminalObject)
rightUnitorProdInv = a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id (a ~> 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)
&&& a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate

associatorProd :: forall {k} (a :: k) b c. (HasProducts k, Ob a, Ob b, Ob c) => (a && b) && c ~> a && (b && c)
associatorProd :: forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
associatorProd = (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @a @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
. forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @(a && b) @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)
&&& (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @a @b ((a && b) ~> b) -> (c ~> 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)
*** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @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
\\ (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (b ~> 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)
*** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b)

associatorProdInv :: forall {k} (a :: k) b c. (HasProducts k, Ob a, Ob b, Ob c) => a && (b && c) ~> (a && b) && c
associatorProdInv :: forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
associatorProdInv = (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @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)
*** forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @b @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)
&&& (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @b @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
. forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @a @(b && c)) ((Ob (b && c), Ob (b && c)) => (a && (b && c)) ~> ((a && b) && c))
-> ((b && c) ~> (b && c)) -> (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
\\ (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b Obj b -> (c ~> c) -> (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)
*** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c)

swapProd' :: (HasBinaryProducts k) => (a :: k) ~> a' -> b ~> b' -> (a && b) ~> (b' && a')
swapProd' :: forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
HasBinaryProducts k =>
(a ~> a') -> (b ~> b') -> (a && b) ~> (b' && a')
swapProd' a ~> a'
a b ~> b'
b = Obj a -> (b ~> b') -> (a && b) ~> b'
forall (a :: k) (b :: k) (b' :: k).
Obj a -> (b ~> b') -> (a && b) ~> b'
forall k (a :: k) (b :: k) (b' :: k).
HasBinaryProducts k =>
Obj a -> (b ~> b') -> (a && b) ~> b'
snd' ((a ~> a') -> Obj a
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src a ~> a'
a) b ~> 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)
&&& (a ~> a') -> Obj b -> (a && b) ~> a'
forall (a :: k) (a' :: k) (b :: k).
(a ~> a') -> Obj b -> (a && b) ~> a'
forall k (a :: k) (a' :: k) (b :: k).
HasBinaryProducts k =>
(a ~> a') -> Obj b -> (a && b) ~> a'
fst' a ~> a'
a ((b ~> b') -> Obj b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src b ~> b'
b)

swapProd :: (HasBinaryProducts k, Ob a, Ob b) => (a :: k) && b ~> b && a
swapProd :: forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> (b && a)
swapProd @_ @a @b = (a ~> a) -> (b ~> b) -> (a && b) ~> (b && a)
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
HasBinaryProducts k =>
(a ~> a') -> (b ~> b') -> (a && b) ~> (b' && a')
swapProd' (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)

newtype PROD k = PR k
type instance UN PR (PR k) = k

type Prod :: j +-> k -> PROD j +-> PROD k
data Prod p (a :: PROD k) b where
  Prod :: {forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Prod p ('PR a) ('PR b) -> p a b
unProd :: p a b} -> Prod p (PR a) (PR b)

instance (Profunctor p) => Profunctor (Prod p) where
  dimap :: forall (c :: PROD k) (a :: PROD k) (b :: PROD j) (d :: PROD j).
(c ~> a) -> (b ~> d) -> Prod p a b -> Prod p c d
dimap (Prod a ~> b
l) (Prod a ~> b
r) (Prod p a b
p) = p a b -> Prod p ('PR a) ('PR b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Prod p ('PR a) ('PR b)
Prod ((a ~> a) -> (b ~> b) -> p a b -> p a b
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a ~> b
a ~> a
l a ~> b
b ~> b
r p a b
p)
  (Ob a, Ob b) => r
r \\ :: forall (a :: PROD k) (b :: PROD j) r.
((Ob a, Ob b) => r) -> Prod p a b -> r
\\ Prod p a b
f = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
f
instance (Promonad p) => Promonad (Prod p) where
  id :: forall (a :: PROD j). Ob a => Prod p a a
id = p (UN 'PR a) (UN 'PR a) -> Prod p ('PR (UN 'PR a)) ('PR (UN 'PR a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Prod p ('PR a) ('PR b)
Prod p (UN 'PR a) (UN 'PR a)
forall (a :: j). Ob a => p a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  Prod p a b
f . :: forall (b :: PROD j) (c :: PROD j) (a :: PROD j).
Prod p b c -> Prod p a b -> Prod p a c
. Prod p a b
g = p a b -> Prod p ('PR a) ('PR b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Prod p ('PR a) ('PR b)
Prod (p a b
f p a b -> p a a -> p a b
forall (b :: j) (c :: j) (a :: j). p b c -> p a b -> p 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
. p a a
p a 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). Ob a => a ~> TerminalObject
terminate = (UN 'PR a ~> TerminalObject)
-> Prod (~>) ('PR (UN 'PR a)) ('PR TerminalObject)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Prod p ('PR a) ('PR b)
Prod UN 'PR a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate
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). (Ob a, Ob b) => (a && b) ~> a
fst @(PR a) @(PR b) = ((UN 'PR a && UN 'PR b) ~> UN 'PR a)
-> Prod (~>) ('PR (UN 'PR a && UN 'PR b)) ('PR (UN 'PR a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Prod p ('PR a) ('PR b)
Prod (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @a @b)
  snd :: forall (a :: PROD k) (b :: PROD k). (Ob a, Ob b) => (a && b) ~> b
snd @(PR a) @(PR b) = ((UN 'PR a && UN 'PR b) ~> UN 'PR b)
-> Prod (~>) ('PR (UN 'PR a && UN 'PR b)) ('PR (UN 'PR b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Prod p ('PR a) ('PR b)
Prod (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @a @b)
  Prod a ~> b
f &&& :: forall (a :: PROD k) (x :: PROD k) (y :: PROD k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Prod a ~> b
g = (a ~> (b && b)) -> Prod (~>) ('PR a) ('PR (b && b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Prod p ('PR a) ('PR b)
Prod (a ~> b
f (a ~> b) -> (a ~> b) -> a ~> (b && b)
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)
&&& a ~> b
a ~> b
g)
  Prod a ~> b
f *** :: forall (a :: PROD k) (b :: PROD k) (x :: PROD k) (y :: PROD k).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** Prod a ~> b
g = ((a && a) ~> (b && b)) -> Prod (~>) ('PR (a && a)) ('PR (b && b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Prod p ('PR a) ('PR b)
Prod (a ~> b
f (a ~> b) -> (a ~> b) -> (a && a) ~> (b && 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
g)
instance (HasInitialObject k) => HasInitialObject (PROD k) where
  type InitialObject = PR InitialObject
  initiate :: forall (a :: PROD k). Ob a => InitialObject ~> a
initiate = (InitialObject ~> UN 'PR a)
-> Prod (~>) ('PR InitialObject) ('PR (UN 'PR a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Prod p ('PR a) ('PR b)
Prod InitialObject ~> UN 'PR a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate

instance (HasProducts k, Category cat) => MonoidalProfunctor (Prod cat :: CAT (PROD k)) where
  par0 :: Prod cat Unit Unit
par0 = Prod cat Unit Unit
Prod cat ('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 cat a a
id
  Prod cat x1 x2
f par :: forall (x1 :: PROD k) (x2 :: PROD k) (y1 :: PROD k) (y2 :: PROD k).
Prod cat x1 x2 -> Prod cat y1 y2 -> Prod cat (x1 ** y1) (x2 ** y2)
`par` Prod cat y1 y2
g = x1 ~> x2
Prod cat x1 x2
f (x1 ~> x2) -> (y1 ~> y2) -> (x1 && y1) ~> (x2 && y2)
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)
*** y1 ~> y2
Prod cat y1 y2
g

instance (HasProducts k) => Monoidal (PROD k) where
  type Unit = TerminalObject
  type a ** b = a && b

  leftUnitor :: forall (a :: PROD k). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
(TerminalObject && 'PR (UN 'PR a)) ~> 'PR (UN 'PR a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(TerminalObject && a) ~> a
leftUnitorProd
  leftUnitorInv :: forall (a :: PROD k). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
'PR (UN 'PR a) ~> (TerminalObject && 'PR (UN 'PR a))
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (TerminalObject && a)
leftUnitorProdInv
  rightUnitor :: forall (a :: PROD k). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
('PR (UN 'PR a) && TerminalObject) ~> 'PR (UN 'PR a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(a && TerminalObject) ~> a
rightUnitorProd
  rightUnitorInv :: forall (a :: PROD k). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
'PR (UN 'PR a) ~> ('PR (UN 'PR a) && TerminalObject)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (a && TerminalObject)
rightUnitorProdInv
  associator :: forall (a :: PROD k) (b :: PROD k) (c :: PROD k).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(PR a) @(PR b) @(PR c) = (((UN 'PR a && UN 'PR b) && UN 'PR c)
 ~> (UN 'PR a && (UN 'PR b && UN 'PR c)))
-> Prod
     (~>)
     ('PR ((UN 'PR a && UN 'PR b) && UN 'PR c))
     ('PR (UN 'PR a && (UN 'PR b && UN 'PR c)))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Prod p ('PR a) ('PR b)
Prod (forall (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
associatorProd @a @b @c)
  associatorInv :: forall (a :: PROD k) (b :: PROD k) (c :: PROD k).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(PR a) @(PR b) @(PR c) = ((UN 'PR a && (UN 'PR b && UN 'PR c))
 ~> ((UN 'PR a && UN 'PR b) && UN 'PR c))
-> Prod
     (~>)
     ('PR (UN 'PR a && (UN 'PR b && UN 'PR c)))
     ('PR ((UN 'PR a && UN 'PR b) && UN 'PR c))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Prod p ('PR a) ('PR b)
Prod (forall (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
associatorProdInv @a @b @c)

instance (HasProducts k) => SymMonoidal (PROD k) where
  swap' :: forall (a :: PROD k) (a' :: PROD k) (b :: PROD k) (b' :: PROD k).
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' (Prod a ~> b
a) (Prod a ~> b
b) = ((a && a) ~> (b && b)) -> Prod (~>) ('PR (a && a)) ('PR (b && b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Prod p ('PR a) ('PR b)
Prod ((a ~> b) -> (a ~> b) -> (a && a) ~> (b && b)
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
HasBinaryProducts k =>
(a ~> a') -> (b ~> b') -> (a && b) ~> (b' && a')
swapProd' a ~> b
a a ~> b
b)

instance MonoidalProfunctor (->) where
  par0 :: Unit -> Unit
par0 = () -> ()
Unit -> Unit
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  x1 -> x2
f par :: forall x1 x2 y1 y2.
(x1 -> x2) -> (y1 -> y2) -> (x1 ** y1) -> (x2 ** y2)
`par` y1 -> y2
g = x1 ~> x2
x1 -> x2
f (x1 ~> x2) -> (y1 ~> y2) -> (x1 && y1) ~> (x2 && y2)
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)
*** y1 ~> y2
y1 -> y2
g

instance Monoidal Type where
  type Unit = TerminalObject
  type a ** b = a && b
  leftUnitor :: forall a. Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
(TerminalObject && a) ~> a
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(TerminalObject && a) ~> a
leftUnitorProd
  leftUnitorInv :: forall a. Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
a ~> (TerminalObject && a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (TerminalObject && a)
leftUnitorProdInv
  rightUnitor :: forall a. Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
(a && TerminalObject) ~> a
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(a && TerminalObject) ~> a
rightUnitorProd
  rightUnitorInv :: forall a. Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
a ~> (a && TerminalObject)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (a && TerminalObject)
rightUnitorProdInv
  associator :: forall a b c.
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = ((a ** b) ** c) ~> (a ** (b ** c))
((a && b) && c) ~> (a && (b && c))
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
associatorProd
  associatorInv :: forall a b c.
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = (a ** (b ** c)) ~> ((a ** b) ** c)
(a && (b && c)) ~> ((a && b) && c)
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
associatorProdInv

instance SymMonoidal Type where
  swap' :: forall a a' b b'. (a ~> a') -> (b ~> 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) (a' :: k) (b :: k) (b' :: k).
HasBinaryProducts k =>
(a ~> a') -> (b ~> b') -> (a && b) ~> (b' && a')
swapProd'

instance Strong (->) (->) where
  act :: forall a b x y. (a -> b) -> (x -> y) -> Act a x -> Act b y
act = (a -> b) -> (x -> y) -> (a ** x) -> b ** y
(a -> b) -> (x -> y) -> Act a x -> Act b y
forall x1 x2 y1 y2.
(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
instance MonoidalAction Type Type where
  type Act p x = p ** x
  unitor :: forall x. Ob x => Act Unit x ~> x
unitor = (Unit ** x) ~> x
Act Unit x ~> x
forall a. Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor
  unitorInv :: forall x. Ob x => x ~> Act Unit x
unitorInv = x ~> (Unit ** x)
x ~> Act Unit x
forall a. Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv
  multiplicator :: forall a b x.
(Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator = (a ** (b ** x)) ~> ((a ** b) ** x)
Act a (Act b x) ~> Act (a ** b) x
forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
forall a b c.
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv
  multiplicatorInv :: forall a b x.
(Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv = ((a ** b) ** x) ~> (a ** (b ** x))
Act (a ** b) x ~> Act a (Act b x)
forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
forall a b c.
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator

instance TracedMonoidalProfunctor (->) where
  trace :: forall u x y.
(Ob x, Ob y, Ob u) =>
((x ** u) -> (y ** u)) -> x -> y
trace (x ** u) -> (y ** u)
f x
x = let (y
y, u
u) = (x ** u) -> (y ** u)
f (x
x, u
u) in y
y

instance MonoidalProfunctor U.Unit where
  par0 :: Unit Unit Unit
par0 = Unit '() '()
Unit Unit Unit
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: ()). Ob a => Unit a a
id
  Unit x1 x2
f par :: forall (x1 :: ()) (x2 :: ()) (y1 :: ()) (y2 :: ()).
Unit x1 x2 -> Unit y1 y2 -> Unit (x1 ** y1) (x2 ** y2)
`par` Unit y1 y2
g = x1 ~> x2
Unit x1 x2
f (x1 ~> x2) -> (y1 ~> y2) -> (x1 && y1) ~> (x2 && y2)
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)
*** y1 ~> y2
Unit y1 y2
g

instance Monoidal () where
  type Unit = TerminalObject
  type a ** b = a && b
  leftUnitor :: forall (a :: ()). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
(TerminalObject && '()) ~> '()
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(TerminalObject && a) ~> a
leftUnitorProd
  leftUnitorInv :: forall (a :: ()). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
'() ~> (TerminalObject && '())
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (TerminalObject && a)
leftUnitorProdInv
  rightUnitor :: forall (a :: ()). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
('() && TerminalObject) ~> '()
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(a && TerminalObject) ~> a
rightUnitorProd
  rightUnitorInv :: forall (a :: ()). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
'() ~> ('() && TerminalObject)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (a && TerminalObject)
rightUnitorProdInv
  associator :: forall (a :: ()) (b :: ()) (c :: ()).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = ((a ** b) ** c) ~> (a ** (b ** c))
(('() && '()) && '()) ~> ('() && ('() && '()))
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
associatorProd
  associatorInv :: forall (a :: ()) (b :: ()) (c :: ()).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = (a ** (b ** c)) ~> ((a ** b) ** c)
('() && ('() && '())) ~> (('() && '()) && '())
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
associatorProdInv

instance SymMonoidal () where
  swap' :: forall (a :: ()) (a' :: ()) (b :: ()) (b' :: ()).
(a ~> a') -> (b ~> 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) (a' :: k) (b :: k) (b' :: k).
HasBinaryProducts k =>
(a ~> a') -> (b ~> b') -> (a && b) ~> (b' && a')
swapProd'

instance Strong U.Unit U.Unit where
  act :: forall (a :: ()) (b :: ()) (x :: ()) (y :: ()).
Unit a b -> Unit x y -> Unit (Act a x) (Act b y)
act = Unit a b -> Unit x y -> Unit (a ** x) (b ** y)
Unit a b -> Unit x y -> Unit (Act a x) (Act b y)
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)
forall (x1 :: ()) (x2 :: ()) (y1 :: ()) (y2 :: ()).
Unit x1 x2 -> Unit y1 y2 -> Unit (x1 ** y1) (x2 ** y2)
par
instance MonoidalAction () () where
  type Act p x = p ** x
  unitor :: forall (x :: ()). Ob x => Act Unit x ~> x
unitor = (Unit ** '()) ~> '()
Act Unit x ~> x
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
forall (a :: ()). Ob a => (Unit ** a) ~> a
leftUnitor
  unitorInv :: forall (x :: ()). Ob x => x ~> Act Unit x
unitorInv = x ~> Act Unit x
'() ~> (Unit ** '())
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
forall (a :: ()). Ob a => a ~> (Unit ** a)
leftUnitorInv
  multiplicator :: forall (a :: ()) (b :: ()) (x :: ()).
(Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator = ('() ** ('() ** '())) ~> (('() ** '()) ** '())
Act a (Act b x) ~> Act (a ** b) x
forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
forall (a :: ()) (b :: ()) (c :: ()).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv
  multiplicatorInv :: forall (a :: ()) (b :: ()) (x :: ()).
(Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv = (('() ** '()) ** '()) ~> ('() ** ('() ** '()))
Act (a ** b) x ~> Act a (Act b x)
forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
forall (a :: ()) (b :: ()) (c :: ()).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator

instance TracedMonoidalProfunctor U.Unit where
  trace :: forall (u :: ()) (x :: ()) (y :: ()).
(Ob x, Ob y, Ob u) =>
Unit (x ** u) (y ** u) -> Unit x y
trace Unit (x ** u) (y ** u)
U.Unit = Unit x y
Unit '() '()
U.Unit

class (Act a b ~ a && b) => ActIsProd a b
instance (Act a b ~ a && b) => ActIsProd a b
class (Strong ((~>) :: CAT k) p, HasProducts k, forall (a :: k) (b :: k). ActIsProd a b) => StrongProd (p :: CAT k)
instance (Strong ((~>) :: CAT k) p, HasProducts k, forall (a :: k) (b :: k). ActIsProd a b) => StrongProd (p :: CAT k)

first' :: forall {k} (p :: CAT k) c a b. (StrongProd p, Ob c) => p a b -> p (a && c) (b && c)
first' :: forall {k} (p :: CAT k) (c :: k) (a :: k) (b :: k).
(StrongProd p, Ob c) =>
p a b -> p (a && c) (b && c)
first' p a b
p = ((a && c) ~> (c && a))
-> ((c && b) ~> (b && c))
-> p (c && a) (c && b)
-> p (a && c) (b && c)
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> (b && a)
swapProd @_ @a @c) (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> (b && a)
swapProd @_ @c @b) (forall {k} (p :: CAT k) (c :: k) (a :: k) (b :: k).
(StrongProd p, Ob c) =>
p a b -> p (c && a) (c && b)
forall (p :: CAT k) (c :: k) (a :: k) (b :: k).
(StrongProd p, Ob c) =>
p a b -> p (c && a) (c && b)
second' @_ @c p a b
p) ((Ob a, Ob b) => p (a && c) (b && c))
-> p a b -> p (a && c) (b && c)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
p

second' :: forall {k} (p :: CAT k) c a b. (StrongProd p, Ob c) => p a b -> p (c && a) (c && b)
second' :: forall {k} (p :: CAT k) (c :: k) (a :: k) (b :: k).
(StrongProd p, Ob c) =>
p a b -> p (c && a) (c && b)
second' p a b
p = forall {m} {m'} {c} {d} (w :: m +-> m') (p :: c +-> d) (a :: m')
       (b :: m) (x :: d) (y :: c).
Strong w p =>
w a b -> p x y -> p (Act a x) (Act b y)
forall (w :: k +-> k) (p :: k +-> k) (a :: k) (b :: k) (x :: k)
       (y :: k).
Strong w p =>
w a b -> p x y -> p (Act a x) (Act b y)
act @((~>) :: CAT k) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c) p a b
p