{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Instance.Cat where

import Data.Type.Nat (Nat (..))

import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit (Unit (..))
import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , MultRep
  , SymMonoidal (..)
  , UnitRep
  , swap
  )
import Proarrow.Category.Monoidal.Action (Costrong (..), MonoidalAction (..), Strong (..))
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard)
import Proarrow.Category.Monoidal.Strictified ()
import Proarrow.Category.Opposite (OPPOSITE (..), Op (..), UnOp (..))
import Proarrow.Core (CAT, CategoryOf (..), Is, Kind, Profunctor (..), Promonad (..), UN, dimapDefault, type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Monoid (Comonoid (..), Monoid (..))
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..), HasBiproducts)
import Proarrow.Object.BinaryProduct
  ( HasBinaryProducts (..)
  , associatorProd
  , associatorProdInv
  , diag
  , leftUnitorProd
  , leftUnitorProdInv
  , rightUnitorProd
  , rightUnitorProdInv
  )
import Proarrow.Object.Dual (CompactClosed (..), StarAutonomous (..), coactCC)
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Composition ((:.:))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Representable (Rep, Representable (..))
import Proarrow.Profunctor.Corepresentable (Corep)
import Proarrow.Profunctor.Constant (Constant)
import Proarrow.Category.Monoidal.Distributive (Distributive (..), distLProd, distRProd)
import Proarrow.Object.NaturalNumbers (HasParamNNO (..))
import Proarrow.Category.Instance.Discrete (DISCRETE (..), Discrete (..))

newtype KIND = K Kind
type instance UN K (K k) = k

type Cat :: CAT KIND
data Cat a b where
  Cat :: forall {j} {k} p. (Profunctor (p :: j +-> k)) => Cat (K j) (K k)

-- | The category of categories and profunctors between them.
instance CategoryOf KIND where
  type (~>) = Cat
  type Ob c = (Is K c, CategoryOf (UN K c))

instance Promonad Cat where
  id :: forall (a :: KIND). Ob a => Cat a a
id = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: UN 'K a +-> UN 'K a).
Profunctor p =>
Cat ('K (UN 'K a)) ('K (UN 'K a))
Cat @Id
  Cat @p . :: forall (b :: KIND) (c :: KIND) (a :: KIND).
Cat b c -> Cat a b -> Cat a c
. Cat @q = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: j +-> k). Profunctor p => Cat ('K j) ('K k)
Cat @(p :.: q)

instance Profunctor Cat where
  dimap :: forall (c :: KIND) (a :: KIND) (b :: KIND) (d :: KIND).
(c ~> a) -> (b ~> d) -> Cat a b -> Cat c d
dimap = (c ~> a) -> (b ~> d) -> Cat a b -> Cat c d
Cat c a -> Cat b d -> Cat a b -> Cat c d
forall {k} (p :: 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 :: KIND) (b :: KIND) r.
((Ob a, Ob b) => r) -> Cat a b -> r
\\ Cat a b
Cat = r
(Ob a, Ob b) => r
r

instance HasTerminalObject KIND where
  type TerminalObject = K ()
  terminate :: forall (a :: KIND). Ob a => a ~> TerminalObject
terminate = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: UN 'K a +-> ()).
Profunctor p =>
Cat ('K (UN 'K a)) ('K ())
Cat @(Rep (Constant '()))

instance HasInitialObject KIND where
  type InitialObject = K ()
  initiate :: forall (a :: KIND). Ob a => InitialObject ~> a
initiate = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: () +-> UN 'K a).
Profunctor p =>
Cat ('K ()) ('K (UN 'K a))
Cat @(Corep (Constant '()))

data family FstCat :: (j, k) +-> j
instance (CategoryOf j, CategoryOf k) => FunctorForRep (FstCat :: (j, k) +-> j) where
  type FstCat @ '(a, b) = a
  fmap :: forall (a :: (j, k)) (b :: (j, k)).
(a ~> b) -> (FstCat @ a) ~> (FstCat @ b)
fmap (a1 ~> b1
f :**: a2 ~> b2
_) = a1 ~> b1
(FstCat @ a) ~> (FstCat @ b)
f

data family SndCat :: (j, k) +-> k
instance (CategoryOf j, CategoryOf k) => FunctorForRep (SndCat :: (j, k) +-> k) where
  type SndCat @ '(a, b) = b
  fmap :: forall (a :: (j, k)) (b :: (j, k)).
(a ~> b) -> (SndCat @ a) ~> (SndCat @ b)
fmap (a1 ~> b1
_ :**: a2 ~> b2
f) = a2 ~> b2
(SndCat @ a) ~> (SndCat @ b)
f

type (:&&&:) :: (k +-> i) -> (k +-> j) -> (k +-> (i, j))
data (p :&&&: q) a b where
  (:&&&:) :: p a c -> q b c -> (p :&&&: q) '(a, b) c
instance (Profunctor p, Profunctor q) => Profunctor (p :&&&: q) where
  dimap :: forall (c :: (i, j)) (a :: (i, j)) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> (:&&&:) p q a b -> (:&&&:) p q c d
dimap (a1 ~> b1
l1 :**: a2 ~> b2
l2) b ~> d
r (p a b
p :&&&: q b b
q) = (a1 ~> a) -> (b ~> d) -> p a b -> p a1 d
forall (c :: i) (a :: i) (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 a1 ~> b1
a1 ~> a
l1 b ~> d
r p a b
p p a1 d -> q a2 d -> (:&&&:) p q '(a1, a2) d
forall {k} {i} {j} (p :: k +-> i) (a :: i) (c :: k) (q :: k +-> j)
       (n :: j).
p a c -> q n c -> (:&&&:) p q '(a, n) c
:&&&: (a2 ~> b) -> (b ~> d) -> q b b -> q a2 d
forall (c :: j) (a :: j) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> q a b -> q 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 a2 ~> b2
a2 ~> b
l2 b ~> d
r q b b
q
  (Ob a, Ob b) => r
r \\ :: forall (a :: (i, j)) (b :: j) r.
((Ob a, Ob b) => r) -> (:&&&:) p q a b -> r
\\ (p a b
p :&&&: q b b
q) = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: i) (b :: j) 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
p ((Ob b, Ob b) => r) -> q b b -> r
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> q 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
\\ q b b
q
instance (Representable p, Representable q) => Representable (p :&&&: q) where
  type (p :&&&: q) % a = '(p % a, q % a)
  tabulate :: forall (b :: j) (a :: (i, j)).
Ob b =>
(a ~> ((p :&&&: q) % b)) -> (:&&&:) p q a b
tabulate (a1 ~> b1
p :**: a2 ~> b2
q) = (a1 ~> (p % b)) -> p a1 b
forall (b :: j) (a :: i). Ob b => (a ~> (p % b)) -> p a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate a1 ~> b1
a1 ~> (p % b)
p p a1 b -> q a2 b -> (:&&&:) p q '(a1, a2) b
forall {k} {i} {j} (p :: k +-> i) (a :: i) (c :: k) (q :: k +-> j)
       (n :: j).
p a c -> q n c -> (:&&&:) p q '(a, n) c
:&&&: (a2 ~> (q % b)) -> q a2 b
forall (b :: j) (a :: j). Ob b => (a ~> (q % b)) -> q a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate a2 ~> b2
a2 ~> (q % b)
q
  index :: forall (a :: (i, j)) (b :: j).
(:&&&:) p q a b -> a ~> ((p :&&&: q) % b)
index (p a b
p :&&&: q b b
q) = p a b -> a ~> (p % b)
forall (a :: i) (b :: j). p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index p a b
p (a ~> (p % b))
-> (b ~> (q % b)) -> (:**:) (~>) (~>) '(a, b) '(p % b, q % 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)
:**: q b b -> b ~> (q % b)
forall (a :: j) (b :: j). q a b -> a ~> (q % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index q b b
q
  repMap :: forall (a :: j) (b :: j).
(a ~> b) -> ((p :&&&: q) % a) ~> ((p :&&&: q) % b)
repMap a ~> b
f = forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> i) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p a ~> b
f ((p % a) ~> (p % b))
-> ((q % a) ~> (q % b))
-> (:**:) (~>) (~>) '(p % a, q % a) '(p % b, q % 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 {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> j) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @q a ~> b
f

instance HasBinaryProducts KIND where
  type l && r = K (UN K l, UN K r)
  withObProd :: forall (a :: KIND) (b :: KIND) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd Ob (a && b) => r
r = r
Ob (a && b) => r
r
  fst :: forall (a :: KIND) (b :: KIND). (Ob a, Ob b) => (a && b) ~> a
fst = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: (UN 'K a, UN 'K b) +-> UN 'K a).
Profunctor p =>
Cat ('K (UN 'K a, UN 'K b)) ('K (UN 'K a))
Cat @(Rep FstCat)
  snd :: forall (a :: KIND) (b :: KIND). (Ob a, Ob b) => (a && b) ~> b
snd = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: (UN 'K a, UN 'K b) +-> UN 'K b).
Profunctor p =>
Cat ('K (UN 'K a, UN 'K b)) ('K (UN 'K b))
Cat @(Rep SndCat)
  Cat @p &&& :: forall (a :: KIND) (x :: KIND) (y :: KIND).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Cat @q = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: j +-> (k, k)). Profunctor p => Cat ('K j) ('K (k, k))
Cat @(p :&&&: q)

instance HasBinaryCoproducts KIND where
  type K l || K r = K (l, r)
  withObCoprod :: forall (a :: KIND) (b :: KIND) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod Ob (a || b) => r
r = r
Ob (a || b) => r
r
  lft :: forall (a :: KIND) (b :: KIND). (Ob a, Ob b) => a ~> (a || b)
lft = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: UN 'K a +-> (UN 'K a, UN 'K b)).
Profunctor p =>
Cat ('K (UN 'K a)) ('K (UN 'K a, UN 'K b))
Cat @(Corep FstCat)
  rgt :: forall (a :: KIND) (b :: KIND). (Ob a, Ob b) => b ~> (a || b)
rgt = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: UN 'K b +-> (UN 'K a, UN 'K b)).
Profunctor p =>
Cat ('K (UN 'K b)) ('K (UN 'K a, UN 'K b))
Cat @(Corep SndCat)
  Cat @p ||| :: forall (x :: KIND) (a :: KIND) (y :: KIND).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Cat @q = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: (j, j) +-> k). Profunctor p => Cat ('K (j, j)) ('K k)
Cat @(UnOp (Rep CombineDual :.: (Op p :&&&: Op q)))

instance HasBiproducts KIND

instance MonoidalProfunctor Cat where
  par0 :: Cat Unit Unit
par0 = Cat Unit Unit
Cat ('K ()) ('K ())
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: KIND). Ob a => Cat a a
id
  Cat @p par :: forall (x1 :: KIND) (x2 :: KIND) (y1 :: KIND) (y2 :: KIND).
Cat x1 x2 -> Cat y1 y2 -> Cat (x1 ** y1) (x2 ** y2)
`par` Cat @q = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: (j, j) +-> (k, k)).
Profunctor p =>
Cat ('K (j, j)) ('K (k, k))
Cat @(p :**: q)

-- | Products as monoidal structure.
instance Monoidal KIND where
  type Unit = K ()
  type l ** r = K (UN K l, UN K r)
  withOb2 :: forall (a :: KIND) (b :: KIND) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 Ob (a ** b) => r
r = r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: KIND). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
(TerminalObject && 'K (UN 'K a)) ~> 'K (UN 'K a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(TerminalObject && a) ~> a
leftUnitorProd
  leftUnitorInv :: forall (a :: KIND). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
'K (UN 'K a) ~> (TerminalObject && 'K (UN 'K a))
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (TerminalObject && a)
leftUnitorProdInv
  rightUnitor :: forall (a :: KIND). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
('K (UN 'K a) && TerminalObject) ~> 'K (UN 'K a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(a && TerminalObject) ~> a
rightUnitorProd
  rightUnitorInv :: forall (a :: KIND). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
'K (UN 'K a) ~> ('K (UN 'K a) && TerminalObject)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (a && TerminalObject)
rightUnitorProdInv
  associator :: forall (a :: KIND) (b :: KIND) (c :: KIND).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = ((a ** b) ** c) ~> (a ** (b ** c))
(('K (UN 'K a) && 'K (UN 'K b)) && 'K (UN 'K c))
~> ('K (UN 'K a) && ('K (UN 'K b) && 'K (UN 'K 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 :: KIND) (b :: KIND) (c :: KIND).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = (a ** (b ** c)) ~> ((a ** b) ** c)
('K (UN 'K a) && ('K (UN 'K b) && 'K (UN 'K c)))
~> (('K (UN 'K a) && 'K (UN 'K b)) && 'K (UN 'K c))
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
associatorProdInv

data family Swap :: (j, k) +-> (k, j)
instance (CategoryOf j, CategoryOf k) => FunctorForRep (Swap :: (j, k) +-> (k, j)) where
  type Swap @ '(a, b) = '(b, a)
  fmap :: forall (a :: (j, k)) (b :: (j, k)).
(a ~> b) -> (Swap @ a) ~> (Swap @ b)
fmap (a1 ~> b1
f1 :**: a2 ~> b2
f2) = a2 ~> b2
f2 (a2 ~> b2) -> (a1 ~> b1) -> (:**:) (~>) (~>) '(a2, a1) '(b2, b1)
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)
:**: a1 ~> b1
f1
instance SymMonoidal KIND where
  swap :: forall (a :: KIND) (b :: KIND).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @(K j) @(K k) = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: (UN 'K a, UN 'K b) +-> (UN 'K b, UN 'K a)).
Profunctor p =>
Cat ('K (UN 'K a, UN 'K b)) ('K (UN 'K b, UN 'K a))
Cat @(Rep Swap :: (j, k) +-> (k, j))

instance Distributive KIND where
  distL :: forall (a :: KIND) (b :: KIND) (c :: KIND).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
forall (a :: KIND) (b :: KIND) (c :: KIND).
(BiCCC KIND, Ob a, Ob b, Ob c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
distLProd @a @b @c
  distR :: forall (a :: KIND) (b :: KIND) (c :: KIND).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
((a || b) && c) ~> ((a && c) || (b && c))
forall (a :: KIND) (b :: KIND) (c :: KIND).
(BiCCC KIND, Ob a, Ob b, Ob c) =>
((a || b) && c) ~> ((a && c) || (b && c))
distRProd @a @b @c
  distL0 :: forall (a :: KIND). Ob a => (a ** InitialObject) ~> InitialObject
distL0 = (a ** InitialObject) ~> InitialObject
('K (UN 'K a) && 'K ()) ~> 'K ()
forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
forall (a :: KIND) (b :: KIND). (Ob a, Ob b) => (a && b) ~> b
snd
  distR0 :: forall (a :: KIND). Ob a => (InitialObject ** a) ~> InitialObject
distR0 = (InitialObject ** a) ~> InitialObject
('K () && 'K (UN 'K a)) ~> 'K ()
forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
forall (a :: KIND) (b :: KIND). (Ob a, Ob b) => (a && b) ~> a
fst

-- | A strictified monoidal category as a monoid in Cat.
instance (Monoidal k) => Monoid (K [k]) where
  mempty :: Unit ~> 'K [k]
mempty = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: () +-> [k]). Profunctor p => Cat ('K ()) ('K [k])
Cat @(Rep UnitRep)
  mappend :: ('K [k] ** 'K [k]) ~> 'K [k]
mappend = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: ([k], [k]) +-> [k]).
Profunctor p =>
Cat ('K ([k], [k])) ('K [k])
Cat @(Rep MultRep)

instance (Ob a) => Comonoid (a :: KIND) where
  counit :: a ~> Unit
counit = a ~> Unit
'K (UN 'K a) ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
forall (a :: KIND). Ob a => a ~> TerminalObject
terminate
  comult :: a ~> (a ** a)
comult = a ~> (a ** a)
'K (UN 'K a) ~> ('K (UN 'K a) && 'K (UN 'K a))
forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
diag
instance CopyDiscard KIND

type Curry :: (i, j) +-> k -> i +-> (OPPOSITE j, k)
data Curry p a b where
  Curry :: p c '(a, b) -> Curry p '(OP b, c) a
instance (Profunctor (p :: (i, j) +-> k), CategoryOf i, CategoryOf j) => Profunctor (Curry p :: i +-> (OPPOSITE j, k)) where
  dimap :: forall (c :: (OPPOSITE j, k)) (a :: (OPPOSITE j, k)) (b :: i)
       (d :: i).
(c ~> a) -> (b ~> d) -> Curry p a b -> Curry p c d
dimap (Op b1 ~> a1
l1 :**: a2 ~> b2
l2) b ~> d
r (Curry p c '(b, b)
p) = p a2 '(d, a1) -> Curry p '( 'OP a1, a2) d
forall {k} {k} {k} (p :: (k, k) +-> k) (a :: k) (a :: k) (n :: k).
p a '(a, n) -> Curry p '( 'OP n, a) a
Curry ((a2 ~> c) -> ('(b, b) ~> '(d, a1)) -> p c '(b, b) -> p a2 '(d, a1)
forall (c :: k) (a :: k) (b :: (i, j)) (d :: (i, 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 a2 ~> b2
a2 ~> c
l2 (b ~> d
r (b ~> d) -> (b1 ~> a1) -> (:**:) (~>) (~>) '(b, b1) '(d, a1)
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)
:**: b1 ~> a1
l1) p c '(b, b)
p) ((Ob b, Ob d) => Curry p c d) -> (b ~> d) -> Curry p c d
forall (a :: i) (b :: i) r. ((Ob a, Ob b) => r) -> (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
\\ b ~> d
r ((Ob a2, Ob b2) => Curry p c d) -> (a2 ~> b2) -> Curry p c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ a2 ~> b2
l2
  (Ob a, Ob b) => r
r \\ :: forall (a :: (OPPOSITE j, k)) (b :: i) r.
((Ob a, Ob b) => r) -> Curry p a b -> r
\\ Curry p c '(b, b)
f = r
(Ob c, Ob '(b, b)) => r
(Ob a, Ob b) => r
r ((Ob c, Ob '(b, b)) => r) -> p c '(b, b) -> r
forall (a :: k) (b :: (i, j)) 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 c '(b, b)
f

type Uncurry :: i +-> (OPPOSITE j, k) -> (i, j) +-> k
data Uncurry p a b where
  Uncurry :: p '(OP b, c) a -> Uncurry p c '(a, b)
instance (Profunctor (p :: i +-> (OPPOSITE j, k)), CategoryOf j, CategoryOf k) => Profunctor (Uncurry p :: (i, j) +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: (i, j)) (d :: (i, j)).
(c ~> a) -> (b ~> d) -> Uncurry p a b -> Uncurry p c d
dimap c ~> a
l (a1 ~> b1
r1 :**: a2 ~> b2
r2) (Uncurry p '( 'OP b, a) a
p) = p '( 'OP b2, c) b1 -> Uncurry p c '(b1, b2)
forall {i} {k} {k} (p :: i +-> (OPPOSITE k, k)) (a :: k) (c :: k)
       (n :: i).
p '( 'OP a, c) n -> Uncurry p c '(n, a)
Uncurry (('( 'OP b2, c) ~> '( 'OP b, a))
-> (a ~> b1) -> p '( 'OP b, a) a -> p '( 'OP b2, c) b1
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
forall (c :: (OPPOSITE j, k)) (a :: (OPPOSITE j, k)) (b :: i)
       (d :: i).
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap ((a2 ~> b2) -> Op (~>) ('OP b2) ('OP a2)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op a2 ~> b2
r2 Op (~>) ('OP b2) ('OP a2)
-> (c ~> a) -> (:**:) (Op (~>)) (~>) '( 'OP b2, c) '( 'OP a2, 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)
:**: c ~> a
l) a1 ~> b1
a ~> b1
r1 p '( 'OP b, a) a
p)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: (i, j)) r.
((Ob a, Ob b) => r) -> Uncurry p a b -> r
\\ Uncurry p '( 'OP b, a) a
f = r
(Ob a, Ob b) => r
(Ob '( 'OP b, a), Ob a) => r
r ((Ob '( 'OP b, a), Ob a) => r) -> p '( 'OP b, a) a -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: (OPPOSITE j, k)) (b :: i) r.
((Ob a, Ob b) => r) -> p a b -> r
\\ p '( 'OP b, a) a
f

instance Closed KIND where
  type K a ~~> K b = K (OPPOSITE a, b)
  withObExp :: forall (a :: KIND) (b :: KIND) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp Ob (a ~~> b) => r
r = r
Ob (a ~~> b) => r
r
  curry :: forall (a :: KIND) (b :: KIND) (c :: KIND).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry (Cat @p) = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: UN 'K a +-> (OPPOSITE (UN 'K b), k)).
Profunctor p =>
Cat ('K (UN 'K a)) ('K (OPPOSITE (UN 'K b), k))
Cat @(Curry p)
  apply :: forall (a :: KIND) (b :: KIND).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: ((OPPOSITE (UN 'K a), UN 'K b), UN 'K a) +-> UN 'K b).
Profunctor p =>
Cat ('K ((OPPOSITE (UN 'K a), UN 'K b), UN 'K a)) ('K (UN 'K b))
Cat @(Uncurry Id)
  Cat @p ^^^ :: forall (a :: KIND) (b :: KIND) (x :: KIND) (y :: KIND).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ Cat @q = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: (OPPOSITE k, j) +-> (OPPOSITE j, k)).
Profunctor p =>
Cat ('K (OPPOSITE k, j)) ('K (OPPOSITE j, k))
Cat @(Op q :**: p)

instance StarAutonomous KIND where
  type Dual (K a) = K (OPPOSITE a)
  dual :: forall (a :: KIND) (b :: KIND). (a ~> b) -> Dual b ~> Dual a
dual (Cat @p) = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: OPPOSITE k +-> OPPOSITE j).
Profunctor p =>
Cat ('K (OPPOSITE k)) ('K (OPPOSITE j))
Cat @(Op p)
  dualInv :: forall (a :: KIND) (b :: KIND).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv (Cat @p) = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: UN 'K b +-> UN 'K a).
Profunctor p =>
Cat ('K (UN 'K b)) ('K (UN 'K a))
Cat @(UnOp p)
  linDist :: forall (a :: KIND) (b :: KIND) (c :: KIND).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist (Cat @p) = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: UN 'K a +-> OPPOSITE (UN 'K b, UN 'K c)).
Profunctor p =>
Cat ('K (UN 'K a)) ('K (OPPOSITE (UN 'K b, UN 'K c)))
Cat @(Rep CombineDual :.: Curry p)
  linDistInv :: forall (a :: KIND) (b :: KIND) (c :: KIND).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv (Cat @p) = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: (j, UN 'K b) +-> OPPOSITE (UN 'K c)).
Profunctor p =>
Cat ('K (j, UN 'K b)) ('K (OPPOSITE (UN 'K c)))
Cat @(Uncurry (Rep DistribDual :.: p))

data family CombineDual :: (OPPOSITE j, OPPOSITE k) +-> OPPOSITE (j, k)
instance (CategoryOf j, CategoryOf k) => FunctorForRep (CombineDual :: (OPPOSITE j, OPPOSITE k) +-> OPPOSITE (j, k)) where
  type CombineDual @ '(OP a, OP b) = OP '(a, b)
  fmap :: forall (a :: (OPPOSITE j, OPPOSITE k))
       (b :: (OPPOSITE j, OPPOSITE k)).
(a ~> b) -> (CombineDual @ a) ~> (CombineDual @ b)
fmap (Op b1 ~> a1
l :**: Op b1 ~> a1
r) = (:**:) (~>) (~>) '(b1, b1) '(a1, a1)
-> Op ((~>) :**: (~>)) ('OP '(a1, a1)) ('OP '(b1, b1))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op (b1 ~> a1
l (b1 ~> a1) -> (b1 ~> a1) -> (:**:) (~>) (~>) '(b1, b1) '(a1, a1)
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)
:**: b1 ~> a1
r)

data family DistribDual :: OPPOSITE (j, k) +-> (OPPOSITE j, OPPOSITE k)
instance (CategoryOf j, CategoryOf k) => FunctorForRep (DistribDual :: OPPOSITE (j, k) +-> (OPPOSITE j, OPPOSITE k)) where
  type DistribDual @ OP '(a, b) = '(OP a, OP b)
  fmap :: forall (a :: OPPOSITE (j, k)) (b :: OPPOSITE (j, k)).
(a ~> b) -> (DistribDual @ a) ~> (DistribDual @ b)
fmap (Op (a1 ~> b1
l :**: a2 ~> b2
r)) = (a1 ~> b1) -> Op (~>) ('OP b1) ('OP a1)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op a1 ~> b1
l Op (~>) ('OP b1) ('OP a1)
-> Op (~>) ('OP b2) ('OP a2)
-> (:**:) (Op (~>)) (Op (~>)) '( 'OP b1, 'OP b2) '( 'OP a1, 'OP a2)
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) -> Op (~>) ('OP b2) ('OP a2)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op a2 ~> b2
r

data family DualUnit :: OPPOSITE () +-> ()
instance FunctorForRep (DualUnit :: OPPOSITE () +-> ()) where
  type DualUnit @ OP '() = '()
  fmap :: forall (a :: OPPOSITE ()) (b :: OPPOSITE ()).
(a ~> b) -> (DualUnit @ a) ~> (DualUnit @ b)
fmap (Op Unit b1 a1
Unit) = (DualUnit @ a) ~> (DualUnit @ b)
Unit '() '()
Unit

instance CompactClosed KIND where
  distribDual :: forall (a :: KIND) (b :: KIND).
(Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: OPPOSITE (UN 'K a, UN 'K b)
             +-> (OPPOSITE (UN 'K a), OPPOSITE (UN 'K b))).
Profunctor p =>
Cat
  ('K (OPPOSITE (UN 'K a, UN 'K b)))
  ('K (OPPOSITE (UN 'K a), OPPOSITE (UN 'K b)))
Cat @(Rep DistribDual)
  dualUnit :: Dual Unit ~> Unit
dualUnit = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: OPPOSITE () +-> ()).
Profunctor p =>
Cat ('K (OPPOSITE ())) ('K ())
Cat @(Rep DualUnit)

data family Succ :: DISCRETE Nat +-> DISCRETE Nat
instance FunctorForRep Succ where
  type Succ @ D n = D (S n)
  fmap :: forall (a :: DISCRETE Nat) (b :: DISCRETE Nat).
(a ~> b) -> (Succ @ a) ~> (Succ @ b)
fmap a ~> b
Discrete a b
Refl = (Succ @ a) ~> (Succ @ b)
Discrete (Succ @ a) (Succ @ a)
forall {k} (a :: DISCRETE k). Discrete a a
Refl
type NNOUniv :: a +-> x -> x +-> x -> (a, DISCRETE Nat) +-> x
data NNOUniv z s a b where
  NNOZ :: Ob x => z x a -> NNOUniv z s x '(a, D Z)
  NNOS :: (s :.: NNOUniv z s) x '(a, D n) -> NNOUniv z s x '(a, D (S n))
instance (Profunctor z, Profunctor s) => Profunctor (NNOUniv z s) where
  dimap :: forall (c :: k) (a :: k) (b :: (a, DISCRETE Nat))
       (d :: (a, DISCRETE Nat)).
(c ~> a) -> (b ~> d) -> NNOUniv z s a b -> NNOUniv z s c d
dimap c ~> a
l (a1 ~> b1
ra :**: Discrete a2 b2
Refl) (NNOZ z a a
z) = z c b1 -> NNOUniv z s c '(b1, 'D 'Z)
forall {x} {a} (x :: x) (z :: a +-> x) (a :: a) (s :: x +-> x).
Ob x =>
z x a -> NNOUniv z s x '(a, 'D 'Z)
NNOZ ((c ~> a) -> (a ~> b1) -> z a a -> z c b1
forall (c :: k) (a :: k) (b :: a) (d :: a).
(c ~> a) -> (b ~> d) -> z a b -> z 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 c ~> a
l a1 ~> b1
a ~> b1
ra z a a
z) ((Ob c, Ob a) => NNOUniv z s c d) -> (c ~> a) -> NNOUniv z s c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ c ~> a
l
  dimap c ~> a
l (a1 ~> b1
ra :**: Discrete a2 b2
Refl) (NNOS (:.:) s (NNOUniv z s) a '(a, 'D n)
s) = (:.:) s (NNOUniv z s) c '(b1, 'D n)
-> NNOUniv z s c '(b1, 'D ('S n))
forall {x} {k} (s :: x +-> x) (z :: k +-> x) (x :: x) (a :: k)
       (n :: Nat).
(:.:) s (NNOUniv z s) x '(a, 'D n) -> NNOUniv z s x '(a, 'D ('S n))
NNOS ((c ~> a)
-> ('(a, 'D n) ~> '(b1, 'D n))
-> (:.:) s (NNOUniv z s) a '(a, 'D n)
-> (:.:) s (NNOUniv z s) c '(b1, 'D n)
forall (c :: k) (a :: k) (b :: (a, DISCRETE Nat))
       (d :: (a, DISCRETE Nat)).
(c ~> a)
-> (b ~> d)
-> (:.:) s (NNOUniv z s) a b
-> (:.:) s (NNOUniv z s) 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 c ~> a
l (a1 ~> b1
ra (a1 ~> b1)
-> Discrete ('D n) ('D n)
-> (:**:) (~>) Discrete '(a1, 'D n) '(b1, 'D n)
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)
:**: Discrete ('D n) ('D n)
forall {k} (a :: DISCRETE k). Discrete a a
Refl) (:.:) s (NNOUniv z s) a '(a, 'D n)
s)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: (a, DISCRETE Nat)) r.
((Ob a, Ob b) => r) -> NNOUniv z s a b -> r
\\ NNOZ z a a
z = r
(Ob a, Ob a) => r
(Ob a, Ob b) => r
r ((Ob a, Ob a) => r) -> z a a -> r
forall (a :: k) (b :: a) r. ((Ob a, Ob b) => r) -> z 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
\\ z a a
z
  (Ob a, Ob b) => r
r \\ NNOS (:.:) s (NNOUniv z s) a '(a, 'D n)
s = r
(Ob a, Ob b) => r
(Ob a, Ob '(a, 'D n)) => r
r ((Ob a, Ob '(a, 'D n)) => r)
-> (:.:) s (NNOUniv z s) a '(a, 'D n) -> r
forall (a :: k) (b :: (a, DISCRETE Nat)) r.
((Ob a, Ob b) => r) -> (:.:) s (NNOUniv z s) 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
\\ (:.:) s (NNOUniv z s) a '(a, 'D n)
s
instance HasParamNNO KIND where
  type NNO = K (DISCRETE Nat)
  zero :: Unit ~> NNO
zero = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: () +-> DISCRETE Nat).
Profunctor p =>
Cat ('K ()) ('K (DISCRETE Nat))
Cat @(Rep (Constant (D Z)))
  succ :: NNO ~> NNO
succ = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: DISCRETE Nat +-> DISCRETE Nat).
Profunctor p =>
Cat ('K (DISCRETE Nat)) ('K (DISCRETE Nat))
Cat @(Rep Succ)
  nnoUniv :: forall (a :: KIND) (x :: KIND).
(a ~> x) -> (x ~> x) -> (a ** NNO) ~> x
nnoUniv (Cat @z) (Cat @s) = forall {a} {n} (p :: a +-> n). Profunctor p => Cat ('K a) ('K n)
forall (p :: (j, DISCRETE Nat) +-> k).
Profunctor p =>
Cat ('K (j, DISCRETE Nat)) ('K k)
Cat @(NNOUniv z s)

instance MonoidalAction KIND KIND where
  type Act a x = a ** x
  withObAct :: forall (a :: KIND) (x :: KIND) r.
(Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct Ob (Act a x) => r
r = r
Ob (Act a x) => r
r
  unitor :: forall (x :: KIND). Ob x => Act Unit x ~> x
unitor = (Unit ** 'K (UN 'K x)) ~> 'K (UN 'K x)
Act Unit x ~> x
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
forall (a :: KIND). Ob a => (Unit ** a) ~> a
leftUnitor
  unitorInv :: forall (x :: KIND). Ob x => x ~> Act Unit x
unitorInv = x ~> Act Unit x
'K (UN 'K x) ~> (Unit ** 'K (UN 'K x))
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
forall (a :: KIND). Ob a => a ~> (Unit ** a)
leftUnitorInv
  multiplicator :: forall (a :: KIND) (b :: KIND) (x :: KIND).
(Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicator = (('K (UN 'K a) ** 'K (UN 'K b)) ** 'K (UN 'K x))
~> ('K (UN 'K a) ** ('K (UN 'K b) ** 'K (UN 'K 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 :: KIND) (b :: KIND) (c :: KIND).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator
  multiplicatorInv :: forall (a :: KIND) (b :: KIND) (x :: KIND).
(Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicatorInv = ('K (UN 'K a) ** ('K (UN 'K b) ** 'K (UN 'K x)))
~> (('K (UN 'K a) ** 'K (UN 'K b)) ** 'K (UN 'K 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 :: KIND) (b :: KIND) (c :: KIND).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv

instance Strong KIND Cat where
  act :: forall (a :: KIND) (b :: KIND) (x :: KIND) (y :: KIND).
(a ~> b) -> Cat x y -> Cat (Act a x) (Act b y)
act = (a ~> b) -> Cat x y -> Cat (Act a x) (Act b y)
Cat a b -> Cat x y -> Cat (a ** x) (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 :: KIND) (x2 :: KIND) (y1 :: KIND) (y2 :: KIND).
Cat x1 x2 -> Cat y1 y2 -> Cat (x1 ** y1) (x2 ** y2)
par

instance Costrong KIND Cat where
  coact :: forall (a :: KIND) (x :: KIND) (y :: KIND).
(Ob a, Ob x, Ob y) =>
Cat (Act a x) (Act a y) -> Cat x y
coact @u = forall {m} {k} (u :: m) (x :: k) (y :: k).
(CompactClosed m, MonoidalAction m k, Ob x, Ob y, Ob u) =>
(Act u x ~> Act u y) -> x ~> y
forall (u :: KIND) (x :: KIND) (y :: KIND).
(CompactClosed KIND, MonoidalAction KIND KIND, Ob x, Ob y, Ob u) =>
(Act u x ~> Act u y) -> x ~> y
coactCC @u