module Proarrow.Category.Instance.Ap where

import Control.Applicative (Applicative (..), liftA3)
import Data.Kind (Type)
import Prelude (($))

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Applicative qualified as A
import Proarrow.Core (CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, type (+->))
import Proarrow.Functor (Functor (..))
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))

type data AP (f :: Type -> Type) k = A k
type instance UN A (A k) = k

type Ap :: (j +-> k) -> AP f j +-> AP f k
data Ap p a b where
  Ap :: forall {j} {k} a b f p. (Ob a, Ob b) => {forall {j} {k} (a :: j) (b :: k) (f :: Type -> Type)
       (p :: k +-> j).
Ap p (A a) (A b) -> f (p a b)
unAp :: f (p a b)} -> Ap p (A a :: AP f j) (A b :: AP f k)

arr :: (Applicative f, Profunctor p) => p a b -> Ap p (A a) (A b :: AP f k)
arr :: forall {k} (f :: Type -> Type) k (p :: k +-> k) (a :: k) (b :: k).
(Applicative f, Profunctor p) =>
p a b -> Ap p (A a) (A b)
arr p a b
f = f (p a b) -> Ap p (A a) (A b)
forall {j} {k} (a :: j) (b :: k) (f :: Type -> Type)
       (p :: k +-> j).
(Ob a, Ob b) =>
f (p a b) -> Ap p (A a) (A b)
Ap (p a b -> f (p a b)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure p a b
f) ((Ob a, Ob b) => Ap p (A a) (A b)) -> p a b -> Ap p (A a) (A b)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
f

instance (Applicative f, Profunctor p) => Profunctor (Ap (p :: j +-> k) :: AP f j +-> AP f k) where
  dimap :: forall (c :: AP f k) (a :: AP f k) (b :: AP f j) (d :: AP f j).
(c ~> a) -> (b ~> d) -> Ap p a b -> Ap p c d
dimap (Ap f (a ~> b)
l) (Ap f (a ~> b)
r) (Ap f (p a b)
x) = f (p a b) -> Ap p (A a) (A b)
forall {j} {k} (a :: j) (b :: k) (f :: Type -> Type)
       (p :: k +-> j).
(Ob a, Ob b) =>
f (p a b) -> Ap p (A a) (A b)
Ap (((a ~> b) -> (a ~> b) -> p a b -> p a b)
-> f (a ~> b) -> f (a ~> b) -> f (p a b) -> f (p a b)
forall (f :: Type -> Type) a b c d.
Applicative f =>
(a -> b -> c -> d) -> f a -> f b -> f c -> f d
liftA3 (a ~> b) -> (a ~> b) -> p a b -> p a b
(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 :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap f (a ~> b)
l f (a ~> b)
r f (p a b)
x)
  (Ob a, Ob b) => r
r \\ :: forall (a :: AP f k) (b :: AP f j) r.
((Ob a, Ob b) => r) -> Ap p a b -> r
\\ Ap{} = r
(Ob a, Ob b) => r
r
instance (Applicative f, Promonad p) => Promonad (Ap (p :: k +-> k) :: AP f k +-> AP f k) where
  id :: forall (a :: AP f k). Ob a => Ap p a a
id = f (p (UN A a) (UN A a)) -> Ap p (A (UN A a)) (A (UN A a))
forall {j} {k} (a :: j) (b :: k) (f :: Type -> Type)
       (p :: k +-> j).
(Ob a, Ob b) =>
f (p a b) -> Ap p (A a) (A b)
Ap (p (UN A a) (UN A a) -> f (p (UN A a) (UN A a))
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure p (UN A a) (UN A a)
forall (a :: k). Ob a => p a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)
  Ap f (p a b)
f . :: forall (b :: AP f k) (c :: AP f k) (a :: AP f k).
Ap p b c -> Ap p a b -> Ap p a c
. Ap f (p a b)
g = f (p a b) -> Ap p (A a) (A b)
forall {j} {k} (a :: j) (b :: k) (f :: Type -> Type)
       (p :: k +-> j).
(Ob a, Ob b) =>
f (p a b) -> Ap p (A a) (A b)
Ap ((p a b -> p a a -> p a b) -> f (p a b) -> f (p a a) -> f (p a b)
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 p a b -> p a a -> p a b
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p a c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
(.) f (p a b)
f f (p a a)
f (p a b)
g)
instance (Applicative f, CategoryOf k) => CategoryOf (AP f k) where
  type (~>) = Ap (~>)
  type Ob a = (Is A a, Ob (UN A a))

instance (Applicative f, CategoryOf k) => Functor (A :: k -> AP f k) where
  map :: forall (a :: k) (b :: k). (a ~> b) -> A a ~> A b
map = (a ~> b) -> A a ~> A b
(a ~> b) -> Ap (~>) (A a) (A b)
forall {k} (f :: Type -> Type) k (p :: k +-> k) (a :: k) (b :: k).
(Applicative f, Profunctor p) =>
p a b -> Ap p (A a) (A b)
arr
instance (Applicative f, Monoidal k) => A.Applicative (A :: k -> AP f k) where
  pure :: forall (a :: k). (Unit ~> a) -> Unit ~> A a
pure = (Unit ~> a) -> Unit ~> A a
(Unit ~> a) -> Ap (~>) (A Unit) (A a)
forall {k} (f :: Type -> Type) k (p :: k +-> k) (a :: k) (b :: k).
(Applicative f, Profunctor p) =>
p a b -> Ap p (A a) (A b)
arr
  liftA2 :: forall (a :: k) (b :: k) (c :: k).
(Ob a, Ob b) =>
((a ** b) ~> c) -> (A a ** A b) ~> A c
liftA2 = ((a ** b) ~> c) -> (A a ** A b) ~> A c
((a ** b) ~> c) -> Ap (~>) (A (a ** b)) (A c)
forall {k} (f :: Type -> Type) k (p :: k +-> k) (a :: k) (b :: k).
(Applicative f, Profunctor p) =>
p a b -> Ap p (A a) (A b)
arr

instance (Applicative f, HasInitialObject k) => HasInitialObject (AP f k) where
  type InitialObject = A InitialObject
  initiate :: forall (a :: AP f k). Ob a => InitialObject ~> a
initiate = (InitialObject ~> UN A a) -> Ap (~>) (A InitialObject) (A (UN A a))
forall {k} (f :: Type -> Type) k (p :: k +-> k) (a :: k) (b :: k).
(Applicative f, Profunctor p) =>
p a b -> Ap p (A a) (A b)
arr InitialObject ~> UN A a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate
instance (Applicative f, HasTerminalObject k) => HasTerminalObject (AP f k) where
  type TerminalObject = A TerminalObject
  terminate :: forall (a :: AP f k). Ob a => a ~> TerminalObject
terminate = (UN A a ~> TerminalObject)
-> Ap (~>) (A (UN A a)) (A TerminalObject)
forall {k} (f :: Type -> Type) k (p :: k +-> k) (a :: k) (b :: k).
(Applicative f, Profunctor p) =>
p a b -> Ap p (A a) (A b)
arr UN A a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate
instance (Applicative f, HasBinaryProducts k) => HasBinaryProducts (AP f k) where
  type a && b = A (UN A a && UN A b)
  withObProd :: forall (a :: AP f k) (b :: AP f k) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @(A a) @(A b) Ob (a && b) => r
r = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @a @b r
Ob (UN A a && UN A b) => r
Ob (a && b) => r
r
  fst :: forall (a :: AP f k) (b :: AP f k). (Ob a, Ob b) => (a && b) ~> a
fst @(A a) @(A b) = ((UN A a && UN A b) ~> UN A a)
-> Ap (~>) (A (UN A a && UN A b)) (A (UN A a))
forall {k} (f :: Type -> Type) k (p :: k +-> k) (a :: k) (b :: k).
(Applicative f, Profunctor p) =>
p a b -> Ap p (A a) (A b)
arr (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @a @b)
  snd :: forall (a :: AP f k) (b :: AP f k). (Ob a, Ob b) => (a && b) ~> b
snd @(A a) @(A b) = ((UN A a && UN A b) ~> UN A b)
-> Ap (~>) (A (UN A a && UN A b)) (A (UN A b))
forall {k} (f :: Type -> Type) k (p :: k +-> k) (a :: k) (b :: k).
(Applicative f, Profunctor p) =>
p a b -> Ap p (A a) (A b)
arr (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @a @b)
  Ap @al @bl f (a ~> b)
f &&& :: forall (a :: AP f k) (x :: AP f k) (y :: AP f k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Ap @ar @br f (a ~> b)
g = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @al @ar ((Ob (a && a) => a ~> (x && y)) -> a ~> (x && y))
-> (Ob (a && a) => a ~> (x && y)) -> a ~> (x && y)
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @bl @br ((Ob (b && b) => a ~> (x && y)) -> a ~> (x && y))
-> (Ob (b && b) => a ~> (x && y)) -> a ~> (x && y)
forall a b. (a -> b) -> a -> b
$ f (a ~> (b && b)) -> Ap (~>) (A a) (A (b && b))
forall {j} {k} (a :: j) (b :: k) (f :: Type -> Type)
       (p :: k +-> j).
(Ob a, Ob b) =>
f (p a b) -> Ap p (A a) (A b)
Ap (((a ~> b) -> (a ~> b) -> a ~> (b && b))
-> f (a ~> b) -> f (a ~> b) -> f (a ~> (b && b))
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (a ~> b) -> (a ~> b) -> a ~> (b && b)
(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)
(&&&) f (a ~> b)
f f (a ~> b)
g)
instance (Applicative f, HasBinaryCoproducts k) => HasBinaryCoproducts (AP f k) where
  type a || b = A (UN A a || UN A b)
  withObCoprod :: forall (a :: AP f k) (b :: AP f k) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @(A a) @(A b) Ob (a || b) => r
r = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a @b r
Ob (UN A a || UN A b) => r
Ob (a || b) => r
r
  lft :: forall (a :: AP f k) (b :: AP f k). (Ob a, Ob b) => a ~> (a || b)
lft @(A a) @(A b) = (UN A a ~> (UN A a || UN A b))
-> A (UN A a) ~> A (UN A a || UN A b)
forall (a :: k) (b :: k). (a ~> b) -> A a ~> A b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @a @b)
  rgt :: forall (a :: AP f k) (b :: AP f k). (Ob a, Ob b) => b ~> (a || b)
rgt @(A a) @(A b) = (UN A b ~> (UN A a || UN A b))
-> A (UN A b) ~> A (UN A a || UN A b)
forall (a :: k) (b :: k). (a ~> b) -> A a ~> A b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @a @b)
  Ap @al @bl f (a ~> b)
f ||| :: forall (x :: AP f k) (a :: AP f k) (y :: AP f k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Ap @ar @br f (a ~> b)
g = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @al @ar ((Ob (a || a) => (x || y) ~> a) -> (x || y) ~> a)
-> (Ob (a || a) => (x || y) ~> a) -> (x || y) ~> a
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @bl @br ((Ob (b || b) => (x || y) ~> a) -> (x || y) ~> a)
-> (Ob (b || b) => (x || y) ~> a) -> (x || y) ~> a
forall a b. (a -> b) -> a -> b
$ f ((a || a) ~> b) -> Ap (~>) (A (a || a)) (A b)
forall {j} {k} (a :: j) (b :: k) (f :: Type -> Type)
       (p :: k +-> j).
(Ob a, Ob b) =>
f (p a b) -> Ap p (A a) (A b)
Ap (((a ~> b) -> (a ~> b) -> (a || a) ~> b)
-> f (a ~> b) -> f (a ~> b) -> f ((a || a) ~> b)
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (a ~> b) -> (a ~> b) -> (a || a) ~> b
(a ~> b) -> (a ~> b) -> (a || a) ~> b
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
(|||) f (a ~> b)
f f (a ~> b)
g)

instance (Applicative f, MonoidalProfunctor p) => MonoidalProfunctor (Ap (p :: j +-> k) :: AP f j +-> AP f k) where
  par0 :: Ap p Unit Unit
par0 = p Unit Unit -> Ap p (A Unit) (A Unit)
forall {k} (f :: Type -> Type) k (p :: k +-> k) (a :: k) (b :: k).
(Applicative f, Profunctor p) =>
p a b -> Ap p (A a) (A b)
arr p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0
  Ap @al @bl f (p a b)
l par :: forall (x1 :: AP f k) (x2 :: AP f j) (y1 :: AP f k) (y2 :: AP f j).
Ap p x1 x2 -> Ap p y1 y2 -> Ap p (x1 ** y1) (x2 ** y2)
`par` Ap @ar @br f (p a b)
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @al @ar ((Ob (a ** a) => Ap p (x1 ** y1) (x2 ** y2))
 -> Ap p (x1 ** y1) (x2 ** y2))
-> (Ob (a ** a) => Ap p (x1 ** y1) (x2 ** y2))
-> Ap p (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @j @bl @br ((Ob (b ** b) => Ap p (x1 ** y1) (x2 ** y2))
 -> Ap p (x1 ** y1) (x2 ** y2))
-> (Ob (b ** b) => Ap p (x1 ** y1) (x2 ** y2))
-> Ap p (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$ f (p (a ** a) (b ** b)) -> Ap p (A (a ** a)) (A (b ** b))
forall {j} {k} (a :: j) (b :: k) (f :: Type -> Type)
       (p :: k +-> j).
(Ob a, Ob b) =>
f (p a b) -> Ap p (A a) (A b)
Ap ((p a b -> p a b -> p (a ** a) (b ** b))
-> f (p a b) -> f (p a b) -> f (p (a ** a) (b ** b))
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 p a b -> p a b -> p (a ** a) (b ** b)
forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
p x1 x2 -> p y1 y2 -> p (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 f (p a b)
l f (p a b)
r)

instance (Applicative f, Monoidal k) => Monoidal (AP f k) where
  type Unit = A Unit
  type a ** b = A (UN A a ** UN A b)
  withOb2 :: forall (a :: AP f k) (b :: AP f k) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @(A a) @(A b) Ob (a ** b) => r
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @b r
Ob (UN A a ** UN A b) => r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: AP f k). Ob a => (Unit ** a) ~> a
leftUnitor = ((Unit ** UN A a) ~> UN A a)
-> Ap (~>) (A (Unit ** UN A a)) (A (UN A a))
forall {k} (f :: Type -> Type) k (p :: k +-> k) (a :: k) (b :: k).
(Applicative f, Profunctor p) =>
p a b -> Ap p (A a) (A b)
arr (Unit ** UN A a) ~> UN A a
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor
  leftUnitorInv :: forall (a :: AP f k). Ob a => a ~> (Unit ** a)
leftUnitorInv = (UN A a ~> (Unit ** UN A a))
-> Ap (~>) (A (UN A a)) (A (Unit ** UN A a))
forall {k} (f :: Type -> Type) k (p :: k +-> k) (a :: k) (b :: k).
(Applicative f, Profunctor p) =>
p a b -> Ap p (A a) (A b)
arr UN A a ~> (Unit ** UN A a)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv
  rightUnitor :: forall (a :: AP f k). Ob a => (a ** Unit) ~> a
rightUnitor = ((UN A a ** Unit) ~> UN A a)
-> Ap (~>) (A (UN A a ** Unit)) (A (UN A a))
forall {k} (f :: Type -> Type) k (p :: k +-> k) (a :: k) (b :: k).
(Applicative f, Profunctor p) =>
p a b -> Ap p (A a) (A b)
arr (UN A a ** Unit) ~> UN A a
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor
  rightUnitorInv :: forall (a :: AP f k). Ob a => a ~> (a ** Unit)
rightUnitorInv = (UN A a ~> (UN A a ** Unit))
-> Ap (~>) (A (UN A a)) (A (UN A a ** Unit))
forall {k} (f :: Type -> Type) k (p :: k +-> k) (a :: k) (b :: k).
(Applicative f, Profunctor p) =>
p a b -> Ap p (A a) (A b)
arr UN A a ~> (UN A a ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv
  associator :: forall (a :: AP f k) (b :: AP f k) (c :: AP f k).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(A a) @(A b) @(A c) = (((UN A a ** UN A b) ** UN A c) ~> (UN A a ** (UN A b ** UN A c)))
-> Ap
     (~>)
     (A ((UN A a ** UN A b) ** UN A c))
     (A (UN A a ** (UN A b ** UN A c)))
forall {k} (f :: Type -> Type) k (p :: k +-> k) (a :: k) (b :: k).
(Applicative f, Profunctor p) =>
p a b -> Ap p (A a) (A b)
arr (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @a @b @c)
  associatorInv :: forall (a :: AP f k) (b :: AP f k) (c :: AP f k).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(A a) @(A b) @(A c) = ((UN A a ** (UN A b ** UN A c)) ~> ((UN A a ** UN A b) ** UN A c))
-> Ap
     (~>)
     (A (UN A a ** (UN A b ** UN A c)))
     (A ((UN A a ** UN A b) ** UN A c))
forall {k} (f :: Type -> Type) k (p :: k +-> k) (a :: k) (b :: k).
(Applicative f, Profunctor p) =>
p a b -> Ap p (A a) (A b)
arr (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @_ @a @b @c)

instance (Applicative f, SymMonoidal k) => SymMonoidal (AP f k) where
  swap :: forall (a :: AP f k) (b :: AP f k).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @(A a) @(A b) = ((UN A a ** UN A b) ~> (UN A b ** UN A a))
-> Ap (~>) (A (UN A a ** UN A b)) (A (UN A b ** UN A a))
forall {k} (f :: Type -> Type) k (p :: k +-> k) (a :: k) (b :: k).
(Applicative f, Profunctor p) =>
p a b -> Ap p (A a) (A b)
arr (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @a @b)