{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Instance.Cat where

import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit (Unit (..))
import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , MultFtor
  , SymMonoidal (..)
  , UnitFtor
  , swap
  )
import Proarrow.Category.Monoidal.Action (Costrong (..), MonoidalAction (..), Strong (..))
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 (..), CopyDiscard, 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 (..), compactClosedCoact)
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)

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 {b} {a} (p :: b +-> a). Profunctor p => Cat ('K b) ('K a)
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 {b} {a} (p :: b +-> a). Profunctor p => Cat ('K b) ('K a)
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

data family Terminate :: k +-> ()
instance (CategoryOf k) => FunctorForRep (Terminate :: k +-> ()) where
  type Terminate @ a = '()
  fmap :: forall (a :: k) (b :: k).
(a ~> b) -> (Terminate @ a) ~> (Terminate @ b)
fmap a ~> b
_ = (Terminate @ a) ~> (Terminate @ b)
Unit '() '()
Unit

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

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

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) (b :: i) (c :: k) (q :: k +-> j)
       (a :: j).
p b c -> q a c -> (:&&&:) p q '(b, a) 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) (b :: i) (c :: k) (q :: k +-> j)
       (a :: j).
p b c -> q a c -> (:&&&:) p q '(b, a) 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 K l && K r = K (l, 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 {b} {a} (p :: b +-> a). Profunctor p => Cat ('K b) ('K a)
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 {b} {a} (p :: b +-> a). Profunctor p => Cat ('K b) ('K a)
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 {b} {a} (p :: b +-> a). Profunctor p => Cat ('K b) ('K a)
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 {b} {a} (p :: b +-> a). Profunctor p => Cat ('K b) ('K a)
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 {b} {a} (p :: b +-> a). Profunctor p => Cat ('K b) ('K a)
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 {b} {a} (p :: b +-> a). Profunctor p => Cat ('K b) ('K a)
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 {b} {a} (p :: b +-> a). Profunctor p => Cat ('K b) ('K a)
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 {b} {a} (p :: b +-> a). Profunctor p => Cat ('K b) ('K a)
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))

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

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) (b :: k) (a :: k) (a :: k).
p b '(a, a) -> Curry p '( 'OP a, b) 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)) (b :: k) (c :: k)
       (a :: i).
p '( 'OP b, c) a -> Uncurry p c '(a, b)
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 {b} {a} (p :: b +-> a). Profunctor p => Cat ('K b) ('K a)
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 {b} {a} (p :: b +-> a). Profunctor p => Cat ('K b) ('K a)
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 {b} {a} (p :: b +-> a). Profunctor p => Cat ('K b) ('K a)
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 {b} {a} (p :: b +-> a). Profunctor p => Cat ('K b) ('K a)
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 {b} {a} (p :: b +-> a). Profunctor p => Cat ('K b) ('K a)
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 {b} {a} (p :: b +-> a). Profunctor p => Cat ('K b) ('K a)
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 {b} {a} (p :: b +-> a). Profunctor p => Cat ('K b) ('K a)
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 {b} {a} (p :: b +-> a). Profunctor p => Cat ('K b) ('K a)
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 {b} {a} (p :: b +-> a). Profunctor p => Cat ('K b) ('K a)
forall (p :: OPPOSITE () +-> ()).
Profunctor p =>
Cat ('K (OPPOSITE ())) ('K ())
Cat @(Rep DualUnit)

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 (Act b x) ~> Act (a ** 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 (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
  multiplicatorInv :: forall (a :: KIND) (b :: KIND) (x :: KIND).
(Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act 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 ** 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

instance Strong KIND (Id :: CAT KIND) where
  act :: forall (a :: KIND) (b :: KIND) (x :: KIND) (y :: KIND).
(a ~> b) -> Id x y -> Id (Act a x) (Act b y)
act = Id a b -> Id x y -> Id (a ** x) (b ** y)
Id a b
-> Id x y -> Id ('K (UN 'K a, UN 'K x)) ('K (UN 'K b, UN 'K 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).
Id x1 x2 -> Id y1 y2 -> Id (x1 ** y1) (x2 ** y2)
par (Id a b
 -> Id x y -> Id ('K (UN 'K a, UN 'K x)) ('K (UN 'K b, UN 'K y)))
-> (Cat a b -> Id a b)
-> Cat a b
-> Id x y
-> Id ('K (UN 'K a, UN 'K x)) ('K (UN 'K b, UN 'K y))
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ~> b) -> Id a b
Cat a b -> Id a b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id

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
compactClosedCoact @u