{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Instance.CatProf where

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

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

newtype KIND = K Kind

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 '()))

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 Fst)
  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 Snd)
  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) :.: Rep Diag)

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 Fst)
  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 Snd)
  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 @(Corep Diag :.: (p :**: q))

instance HasBiproducts KIND

instance MonoidalProfunctor Cat where
  one :: Cat Unit Unit
one = 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 ** :: forall (x1 :: KIND) (x2 :: KIND) (y1 :: KIND) (y2 :: KIND).
Cat x1 x2 -> Cat y1 y2 -> Cat (x1 ** y1) (x2 ** y2)
** 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
  absorbL :: forall (a :: KIND). Ob a => (a ** InitialObject) ~> InitialObject
absorbL = (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
  absorbR :: forall (a :: KIND). Ob a => (InitialObject ** a) ~> InitialObject
absorbR = (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 (t :: (KIND, KIND) +-> KIND)) => Costrong t Cat where
  coact :: forall (a :: KIND) (x :: KIND) (y :: KIND).
(Ob a, Ob x, Ob y) =>
Cat (Act t a x) (Act t a y) -> Cat x y
coact @u = forall {m} {k} (t :: (m, k) +-> k) (u :: m) (x :: k) (y :: k).
(CompactClosed m, MonoidalAction t, Ob x, Ob y, Ob u) =>
(Act t u x ~> Act t u y) -> x ~> y
forall (t :: (KIND, KIND) +-> KIND) (u :: KIND) (x :: KIND)
       (y :: KIND).
(CompactClosed KIND, MonoidalAction t, Ob x, Ob y, Ob u) =>
(Act t u x ~> Act t u y) -> x ~> y
coactCC @t @u