{-# 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 (..)
  , SymMonoidal (..)
  , TracedMonoidalProfunctor (..)
  )
import Proarrow.Category.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Core (CAT, CategoryOf (..), Is, Kind, Profunctor (..), Promonad (..), UN, dimapDefault, type (+->))
import Proarrow.Object.BinaryProduct
  ( HasBinaryProducts (..)
  , associatorProd
  , associatorProdInv
  , leftUnitorProd
  , leftUnitorProdInv
  , rightUnitorProd
  , rightUnitorProdInv
  )
import Proarrow.Object.Dual (CompactClosed (..), StarAutonomous (..), compactClosedTrace)
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Composition ((:.:))
import Proarrow.Profunctor.Identity (Id)

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

type Terminate :: k +-> ()
data Terminate a b where
  Terminate :: (Ob b) => Terminate '() b
instance (CategoryOf k) => Profunctor (Terminate :: k +-> ()) where
  dimap :: forall (c :: ()) (a :: ()) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Terminate a b -> Terminate c d
dimap c ~> a
Unit c a
Unit b ~> d
r Terminate a b
Terminate = Terminate c d
Terminate '() d
(Ob b, Ob d) => Terminate c d
forall {k} (b :: k). Ob b => Terminate '() b
Terminate ((Ob b, Ob d) => Terminate c d) -> (b ~> d) -> Terminate c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> d
r
  (Ob a, Ob b) => r
r \\ :: forall (a :: ()) (b :: k) r.
((Ob a, Ob b) => r) -> Terminate a b -> r
\\ Terminate a b
Terminate = r
(Ob a, Ob b) => r
r
instance HasTerminalObject KIND where
  type TerminalObject = K ()
  terminate' :: forall (a :: KIND) (a' :: KIND). (a ~> a') -> a ~> TerminalObject
terminate' a ~> a'
Cat a a'
Cat = forall {c} {a} (p :: c +-> a). Profunctor p => Cat ('K c) ('K a)
forall (p :: j +-> ()). Profunctor p => Cat ('K j) ('K ())
Cat @Terminate

type FstCat :: (j, k) +-> j
data FstCat a b where
  FstCat :: (Ob c) => a ~> b -> FstCat a '(b, c)
instance (CategoryOf j, CategoryOf k) => Profunctor (FstCat :: (j, k) +-> j) where
  dimap :: forall (c :: j) (a :: j) (b :: (j, k)) (d :: (j, k)).
(c ~> a) -> (b ~> d) -> FstCat a b -> FstCat c d
dimap c ~> a
l (a1 ~> b1
r1 :**: a2 ~> b2
r2) (FstCat a ~> b
f) = (c ~> b1) -> FstCat c '(b1, b2)
forall {k} {k} (c :: k) (a :: k) (a :: k).
Ob c =>
(a ~> a) -> FstCat a '(a, c)
FstCat (a1 ~> b1
r1 (a1 ~> b1) -> (c ~> a1) -> c ~> b1
forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> a1
a ~> b
f (a ~> a1) -> (c ~> a) -> c ~> a1
forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c ~> a
l) ((Ob a2, Ob b2) => FstCat c d) -> (a2 ~> b2) -> FstCat c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a2 ~> b2
r2
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: (j, k)) r.
((Ob a, Ob b) => r) -> FstCat a b -> r
\\ FstCat a ~> b
f = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f

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

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

instance MonoidalProfunctor Cat where
  par0 :: Cat Unit Unit
par0 = Cat Unit Unit
Cat ('K ()) ('K ())
forall {k} (p :: PRO 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 {c} {a} (p :: c +-> a). Profunctor p => Cat ('K c) ('K a)
forall (p :: (j, j) +-> (k, k)).
Profunctor p =>
Cat ('K (j, j)) ('K (k, k))
Cat @(p :**: q)

instance Monoidal KIND where
  type Unit = K ()
  type l ** r = K (UN K l, UN K 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

type Swap :: h +-> i -> j +-> k -> (h, j) +-> (k, i)
data Swap p q a b where
  Swap :: p a b -> q c d -> Swap p q '(a, c) '(d, b)
instance (Profunctor p, Profunctor q) => Profunctor (Swap p q) where
  dimap :: forall (c :: (k, i)) (a :: (k, i)) (b :: (h, j)) (d :: (h, j)).
(c ~> a) -> (b ~> d) -> Swap p q a b -> Swap p q c d
dimap (a1 ~> b1
l1 :**: a2 ~> b2
l2) (a1 ~> b1
r1 :**: a2 ~> b2
r2) (Swap p a b
p q c d
q) = p a1 b2 -> q a2 b1 -> Swap p q '(a1, a2) '(b1, b2)
forall {h} {i} (p :: h +-> i) (c :: i) (a :: h) (p :: h +-> i)
       (b :: i) (d :: h).
p c a -> p b d -> Swap p p '(c, b) '(d, a)
Swap ((a1 ~> a) -> (b ~> b2) -> p a b -> p a1 b2
forall (c :: i) (a :: i) (b :: h) (d :: h).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a1 ~> a
a1 ~> b1
l1 b ~> b2
a2 ~> b2
r2 p a b
p) ((a2 ~> c) -> (d ~> b1) -> q c d -> q a2 b1
forall (c :: i) (a :: i) (b :: h) (d :: h).
(c ~> a) -> (b ~> d) -> q a b -> q c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a2 ~> b2
a2 ~> c
l2 a1 ~> b1
d ~> b1
r1 q c d
q)
  (Ob a, Ob b) => r
r \\ :: forall (a :: (k, i)) (b :: (h, j)) r.
((Ob a, Ob b) => r) -> Swap p q a b -> r
\\ Swap p a b
p q c d
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 :: h) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p ((Ob c, Ob d) => r) -> q c d -> r
forall (a :: i) (b :: h) r. ((Ob a, Ob b) => r) -> q a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ q c d
q
instance SymMonoidal KIND where
  swap' :: forall (a :: KIND) (a' :: KIND) (b :: KIND) (b' :: KIND).
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' (Cat @p) (Cat @q) = forall {c} {a} (p :: c +-> a). Profunctor p => Cat ('K c) ('K a)
forall (p :: (j, j) +-> (k, k)).
Profunctor p =>
Cat ('K (j, j)) ('K (k, k))
Cat @(Swap p q)

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

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

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

type DUAL k = ((), OPPOSITE k)
type Dual a = '( '(), OP a)

type DoubleNeg :: DUAL (DUAL k) +-> k
data DoubleNeg a b where
  DoubleNeg :: a ~> b -> DoubleNeg a (Dual (Dual b))
instance (CategoryOf k) => Profunctor (DoubleNeg :: DUAL (DUAL k) +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: DUAL (DUAL k)) (d :: DUAL (DUAL k)).
(c ~> a) -> (b ~> d) -> DoubleNeg a b -> DoubleNeg c d
dimap c ~> a
l (Unit a1 b1
Unit :**: Op (Unit a1 b1
Unit :**: Op b1 ~> a1
r)) (DoubleNeg a ~> b
f) = (c ~> a1) -> DoubleNeg c (Dual (Dual a1))
forall {k} (a :: k) (c :: k).
(a ~> c) -> DoubleNeg a (Dual (Dual c))
DoubleNeg (b1 ~> a1
r (b1 ~> a1) -> (c ~> b1) -> c ~> a1
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b1
a ~> b
f (a ~> b1) -> (c ~> a) -> c ~> b1
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c ~> a
l)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: DUAL (DUAL k)) r.
((Ob a, Ob b) => r) -> DoubleNeg a b -> r
\\ DoubleNeg a ~> b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
p
instance StarAutonomous KIND where
  type Bottom = K ()
  bottomObj :: Obj Bottom
bottomObj = Obj Bottom
Cat ('K ()) ('K ())
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: KIND). Ob a => Cat a a
id
  doubleNeg :: forall (a :: KIND).
(StarAutonomous KIND, Ob a) =>
Dual (Dual a) ~> a
doubleNeg = forall {c} {a} (p :: c +-> a). Profunctor p => Cat ('K c) ('K a)
forall (p :: DUAL (DUAL (UN 'K a)) +-> UN 'K a).
Profunctor p =>
Cat ('K (DUAL (DUAL (UN 'K a)))) ('K (UN 'K a))
Cat @DoubleNeg

type DistribDual :: j +-> j' -> k +-> k' -> DUAL (j', k') +-> (DUAL j, DUAL k)
data DistribDual p q a b where
  DistribDual :: p c a -> q d b -> DistribDual p q '(Dual a, Dual b) (Dual '(c, d))
instance (Profunctor p, Profunctor q) => Profunctor (DistribDual p q) where
  dimap :: forall (c :: (DUAL j, DUAL k)) (a :: (DUAL j, DUAL k))
       (b :: DUAL (j', k')) (d :: DUAL (j', k')).
(c ~> a) -> (b ~> d) -> DistribDual p q a b -> DistribDual p q c d
dimap ((Unit a1 b1
Unit :**: Op b1 ~> a1
l1) :**: (Unit a1 b1
Unit :**: Op b1 ~> a1
l2)) (Unit a1 b1
Unit :**: (Op (a1 ~> b1
r1 :**: a2 ~> b2
r2))) (DistribDual p c a
f q d b
g) =
    p a1 a1
-> q a2 a1 -> DistribDual p q '(Dual a1, Dual a1) (Dual '(a1, a2))
forall {j} {j'} {k} {k'} (p :: j +-> j') (c :: j') (a :: j)
       (q :: k +-> k') (p :: k') (b :: k).
p c a -> q p b -> DistribDual p q '(Dual a, Dual b) (Dual '(c, p))
DistribDual ((a1 ~> c) -> (a ~> a1) -> p c a -> p a1 a1
forall (c :: j') (a :: j') (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a1 ~> b1
a1 ~> c
r1 b1 ~> a1
a ~> a1
l1 p c a
f) ((a2 ~> d) -> (b ~> a1) -> q d b -> q a2 a1
forall (c :: k') (a :: k') (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> q a b -> q c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a2 ~> b2
a2 ~> d
r2 b1 ~> a1
b ~> a1
l2 q d b
g)
  (Ob a, Ob b) => r
r \\ :: forall (a :: (DUAL j, DUAL k)) (b :: DUAL (j', k')) r.
((Ob a, Ob b) => r) -> DistribDual p q a b -> r
\\ DistribDual p c a
f q d b
g = r
(Ob c, Ob a) => r
(Ob a, Ob b) => r
r ((Ob c, Ob a) => r) -> p c a -> r
forall (a :: j') (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p c a
f ((Ob d, Ob b) => r) -> q d b -> r
forall (a :: k') (b :: k) r. ((Ob a, Ob b) => r) -> q a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ q d b
g

instance CompactClosed KIND where
  distribDual' :: forall (a :: KIND) (a' :: KIND) (b :: KIND) (b' :: KIND).
(a ~> a') -> (b ~> b') -> Dual (a' ** b') ~> (Dual a ** Dual b)
distribDual' (Cat @p) (Cat @q) = forall {c} {a} (p :: c +-> a). Profunctor p => Cat ('K c) ('K a)
forall (p :: DUAL (k, k) +-> (DUAL j, DUAL j)).
Profunctor p =>
Cat ('K (DUAL (k, k))) ('K (DUAL j, DUAL j))
Cat @(DistribDual p q)

instance TracedMonoidalProfunctor Cat where
  trace :: forall (u :: KIND) (x :: KIND) (y :: KIND).
(Ob x, Ob y, Ob u) =>
Cat (x ** u) (y ** u) -> Cat x y
trace = (('K (UN 'K x) ** 'K (UN 'K u)) ~> ('K (UN 'K y) ** 'K (UN 'K u)))
-> 'K (UN 'K x) ~> 'K (UN 'K y)
Cat (x ** u) (y ** u) -> Cat x y
forall {k} (u :: k) (x :: k) (y :: k).
(CompactClosed k, Ob x, Ob y, Ob u) =>
((x ** u) ~> (y ** u)) -> x ~> y
compactClosedTrace