{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Instance.Cat where

import Data.Void (Void)
import GHC.Base (Any)

import Proarrow.Category.Instance.Coproduct (COPRODUCT (..), (:++:) (..))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit (Unit (..))
import Proarrow.Category.Instance.Zero (VOID, no)
import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , SymMonoidal (..)
  , TracedMonoidalProfunctor (..)
  , swap
  )
import Proarrow.Category.Opposite (OPPOSITE (..), Op (..), UnOp (..))
import Proarrow.Core (CAT, CategoryOf (..), Is, Kind, Profunctor (..), Promonad (..), UN, dimapDefault, obj, type (+->))
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Object.BinaryProduct
  ( HasBinaryProducts (..)
  , associatorProd
  , associatorProdInv
  , leftUnitorProd
  , leftUnitorProdInv
  , rightUnitorProd
  , rightUnitorProdInv
  )
import Proarrow.Object.Dual (CompactClosed (..), StarAutonomous (..), combineDual, compactClosedTrace)
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 (Representable (..))

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 (CategoryOf k) => Representable (Terminate :: k +-> ()) where
  type Terminate % a = '()
  tabulate :: forall (b :: k) (a :: ()).
Ob b =>
(a ~> (Terminate % b)) -> Terminate a b
tabulate a ~> (Terminate % b)
Unit a '()
Unit = Terminate a b
Terminate '() b
forall {k} (b :: k). Ob b => Terminate '() b
Terminate
  index :: forall (a :: ()) (b :: k). Terminate a b -> a ~> (Terminate % b)
index Terminate a b
Terminate = a ~> (Terminate % b)
Unit '() '()
Unit
  repMap :: forall (a :: k) (b :: k).
(a ~> b) -> (Terminate % a) ~> (Terminate % b)
repMap 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 {c} {a} (p :: c +-> a). Profunctor p => Cat ('K c) ('K a)
forall (p :: UN 'K a +-> ()).
Profunctor p =>
Cat ('K (UN 'K a)) ('K ())
Cat @Terminate

type Initiate :: VOID +-> k
data Initiate a b where
  Initiate :: (Ob a, Ob b) => Void -> Initiate a b
instance (CategoryOf k) => Profunctor (Initiate :: VOID +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: VOID) (d :: VOID).
(c ~> a) -> (b ~> d) -> Initiate a b -> Initiate c d
dimap c ~> a
_ b ~> d
_ = \case {}
  \\ :: forall (a :: k) (b :: VOID) r.
((Ob a, Ob b) => r) -> Initiate a b -> r
(\\) (Ob a, Ob b) => r
_ = \case {}
instance (CategoryOf k) => Representable (Initiate :: VOID +-> k) where
  type Initiate % a = Any
  tabulate :: forall (b :: VOID) (a :: k).
Ob b =>
(a ~> (Initiate % b)) -> Initiate a b
tabulate = (a ~> Any) -> Initiate a b
(a ~> (Initiate % b)) -> Initiate a b
forall a. Bottom => a
forall a. a
no
  index :: forall (a :: k) (b :: VOID). Initiate a b -> a ~> (Initiate % b)
index = \case {}
  repMap :: forall (a :: VOID) (b :: VOID).
(a ~> b) -> (Initiate % a) ~> (Initiate % b)
repMap = \case {}

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

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
instance (CategoryOf j, CategoryOf k) => Representable (FstCat :: (j, k) +-> j) where
  type FstCat % '(a, b) = a
  tabulate :: forall (b :: (j, k)) (a :: j).
Ob b =>
(a ~> (FstCat % b)) -> FstCat a b
tabulate = (a ~> (FstCat % b)) -> FstCat a b
(a ~> Fst b) -> FstCat a '(Fst b, Snd b)
forall {k} {k} (c :: k) (a :: k) (a :: k).
Ob c =>
(a ~> a) -> FstCat a '(a, c)
FstCat
  index :: forall (a :: j) (b :: (j, k)). FstCat a b -> a ~> (FstCat % b)
index (FstCat a ~> b
f) = a ~> b
a ~> (FstCat % b)
f
  repMap :: forall (a :: (j, k)) (b :: (j, k)).
(a ~> b) -> (FstCat % a) ~> (FstCat % b)
repMap (a1 ~> b1
f :**: a2 ~> b2
_) = a1 ~> b1
(FstCat % a) ~> (FstCat % 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
instance (CategoryOf j, CategoryOf k) => Representable (SndCat :: (j, k) +-> k) where
  type SndCat % '(a, b) = b
  tabulate :: forall (b :: (j, k)) (a :: k).
Ob b =>
(a ~> (SndCat % b)) -> SndCat a b
tabulate = (a ~> (SndCat % b)) -> SndCat a b
(a ~> Snd b) -> SndCat a '(Fst b, Snd b)
forall {j} {k} (c :: j) (a :: k) (a :: k).
Ob c =>
(a ~> a) -> SndCat a '(c, a)
SndCat
  index :: forall (a :: k) (b :: (j, k)). SndCat a b -> a ~> (SndCat % b)
index (SndCat a ~> c
f) = a ~> c
a ~> (SndCat % b)
f
  repMap :: forall (a :: (j, k)) (b :: (j, k)).
(a ~> b) -> (SndCat % a) ~> (SndCat % b)
repMap (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 :: 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 (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) (c :: i) (c :: k) (q :: k +-> j)
       (a :: j).
p c c -> q a c -> (:&&&:) p q '(c, 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 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)

type LftCat :: j +-> COPRODUCT j k
data LftCat a b where
  LftCat :: a ~> b -> LftCat (L a) b
instance (CategoryOf j, CategoryOf k) => Profunctor (LftCat :: j +-> COPRODUCT j k) where
  dimap :: forall (c :: COPRODUCT j k) (a :: COPRODUCT j k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> LftCat a b -> LftCat c d
dimap (InjL a1 ~> b1
l) b ~> d
r (LftCat a ~> b
f) = (a1 ~> d) -> LftCat (L a1) d
forall {k} {k} (c :: k) (b :: k). (c ~> b) -> LftCat (L c) b
LftCat (b ~> d
r (b ~> d) -> (a1 ~> b) -> a1 ~> d
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
. b1 ~> b
a ~> b
f (b1 ~> b) -> (a1 ~> b1) -> a1 ~> b
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
. a1 ~> b1
l)
  dimap (InjR a1 ~> b1
_) b ~> d
_ LftCat a b
f = case LftCat a b
f of {}
  (Ob a, Ob b) => r
r \\ :: forall (a :: COPRODUCT j k) (b :: j) r.
((Ob a, Ob b) => r) -> LftCat a b -> r
\\ LftCat 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
instance (CategoryOf j, CategoryOf k) => Representable (LftCat :: j +-> COPRODUCT j k) where
  type LftCat % a = L a
  tabulate :: forall (b :: j) (a :: COPRODUCT j k).
Ob b =>
(a ~> (LftCat % b)) -> LftCat a b
tabulate (InjL a1 ~> b1
f) = (a1 ~> b) -> LftCat (L a1) b
forall {k} {k} (c :: k) (b :: k). (c ~> b) -> LftCat (L c) b
LftCat a1 ~> b
a1 ~> b1
f
  index :: forall (a :: COPRODUCT j k) (b :: j).
LftCat a b -> a ~> (LftCat % b)
index (LftCat a ~> b
f) = (a ~> b) -> (:++:) (~>) (~>) (L a) (L b)
forall {j1} {k1} {j2} {k2} (p :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (q :: j2 +-> k2).
p a1 b1 -> (:++:) p q (L a1) (L b1)
InjL a ~> b
f
  repMap :: forall (a :: j) (b :: j). (a ~> b) -> (LftCat % a) ~> (LftCat % b)
repMap = (a ~> b) -> (LftCat % a) ~> (LftCat % b)
(a ~> b) -> (:++:) (~>) (~>) (L a) (L b)
forall {j1} {k1} {j2} {k2} (p :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (q :: j2 +-> k2).
p a1 b1 -> (:++:) p q (L a1) (L b1)
InjL

type RgtCat :: k +-> COPRODUCT j k
data RgtCat a b where
  RgtCat :: a ~> b -> RgtCat (R a) b
instance (CategoryOf j, CategoryOf k) => Profunctor (RgtCat :: k +-> COPRODUCT j k) where
  dimap :: forall (c :: COPRODUCT j k) (a :: COPRODUCT j k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> RgtCat a b -> RgtCat c d
dimap (InjR a1 ~> b1
l) b ~> d
r (RgtCat a ~> b
f) = (a1 ~> d) -> RgtCat (R a1) d
forall {k} {j} (c :: k) (b :: k). (c ~> b) -> RgtCat (R c) b
RgtCat (b ~> d
r (b ~> d) -> (a1 ~> b) -> a1 ~> d
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
. b1 ~> b
a ~> b
f (b1 ~> b) -> (a1 ~> b1) -> a1 ~> b
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
. a1 ~> b1
l)
  dimap (InjL a1 ~> b1
_) b ~> d
_ RgtCat a b
f = case RgtCat a b
f of {}
  (Ob a, Ob b) => r
r \\ :: forall (a :: COPRODUCT j k) (b :: k) r.
((Ob a, Ob b) => r) -> RgtCat a b -> r
\\ RgtCat 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 :: 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
f
instance (CategoryOf j, CategoryOf k) => Representable (RgtCat :: k +-> COPRODUCT j k) where
  type RgtCat % a = R a
  tabulate :: forall (b :: k) (a :: COPRODUCT j k).
Ob b =>
(a ~> (RgtCat % b)) -> RgtCat a b
tabulate (InjR a1 ~> b1
f) = (a1 ~> b) -> RgtCat (R a1) b
forall {k} {j} (c :: k) (b :: k). (c ~> b) -> RgtCat (R c) b
RgtCat a1 ~> b
a1 ~> b1
f
  index :: forall (a :: COPRODUCT j k) (b :: k).
RgtCat a b -> a ~> (RgtCat % b)
index (RgtCat a ~> b
f) = (a ~> b) -> (:++:) (~>) (~>) (R a) (R b)
forall {j2} {k2} {j1} {k1} (q :: j2 +-> k2) (a1 :: k2) (b1 :: j2)
       (p :: j1 +-> k1).
q a1 b1 -> (:++:) p q (R a1) (R b1)
InjR a ~> b
f
  repMap :: forall (a :: k) (b :: k). (a ~> b) -> (RgtCat % a) ~> (RgtCat % b)
repMap = (a ~> b) -> (RgtCat % a) ~> (RgtCat % b)
(a ~> b) -> (:++:) (~>) (~>) (R a) (R b)
forall {j2} {k2} {j1} {k1} (q :: j2 +-> k2) (a1 :: k2) (b1 :: j2)
       (p :: j1 +-> k1).
q a1 b1 -> (:++:) p q (R a1) (R b1)
InjR

type (:|||:) :: (i +-> k) -> (j +-> k) -> (COPRODUCT i j +-> k)
data (p :|||: q) a b where
  InjLP :: p a b -> (p :|||: q) a (L b)
  InjRP :: q a b -> (p :|||: q) a (R b)
instance (Profunctor p, Profunctor q) => Profunctor (p :|||: q) where
  dimap :: forall (c :: j) (a :: j) (b :: COPRODUCT i j) (d :: COPRODUCT i j).
(c ~> a) -> (b ~> d) -> (:|||:) p q a b -> (:|||:) p q c d
dimap c ~> a
l (InjL a1 ~> b1
r) (InjLP p a b
p) = p c b1 -> (:|||:) p q c (L b1)
forall {i} {k} {j} (p :: i +-> k) (a :: k) (c :: i) (q :: j +-> k).
p a c -> (:|||:) p q a (L c)
InjLP ((c ~> a) -> (b ~> b1) -> p a b -> p c b1
forall (c :: j) (a :: j) (b :: i) (d :: i).
(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 c ~> a
l a1 ~> b1
b ~> b1
r p a b
p)
  dimap c ~> a
l (InjR a1 ~> b1
r) (InjRP q a b
p) = q c b1 -> (:|||:) p q c (R b1)
forall {j} {k} {i} (q :: j +-> k) (a :: k) (c :: j) (p :: i +-> k).
q a c -> (:|||:) p q a (R c)
InjRP ((c ~> a) -> (b ~> b1) -> q a b -> q c b1
forall (c :: j) (a :: j) (b :: j) (d :: j).
(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 c ~> a
l a1 ~> b1
b ~> b1
r q a b
p)
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: COPRODUCT i j) r.
((Ob a, Ob b) => r) -> (:|||:) p q a b -> r
\\ InjLP p a b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: j) (b :: i) 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 a, Ob b) => r
r \\ InjRP q a b
q = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> q a b -> r
forall (a :: j) (b :: j) 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 a b
q
instance (Representable p, Representable q) => Representable (p :|||: q) where
  type (p :|||: q) % L a = p % a
  type (p :|||: q) % R a = q % a
  tabulate :: forall (b :: COPRODUCT i j) (a :: k).
Ob b =>
(a ~> ((p :|||: q) % b)) -> (:|||:) p q a b
tabulate @b a ~> ((p :|||: q) % b)
f = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: COPRODUCT i j).
(CategoryOf (COPRODUCT i j), Ob a) =>
Obj a
obj @b of
    InjL a1 ~> b1
l -> p a b1 -> (:|||:) p q a (L b1)
forall {i} {k} {j} (p :: i +-> k) (a :: k) (c :: i) (q :: j +-> k).
p a c -> (:|||:) p q a (L c)
InjLP (forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: i +-> k) (b :: i) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @p a ~> (p % b1)
a ~> ((p :|||: q) % b)
f) ((Ob a1, Ob b1) => (:|||:) p q a b)
-> (a1 ~> b1) -> (:|||:) p q a b
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
\\ a1 ~> b1
l
    InjR a1 ~> b1
r -> q a b1 -> (:|||:) p q a (R b1)
forall {j} {k} {i} (q :: j +-> k) (a :: k) (c :: j) (p :: i +-> k).
q a c -> (:|||:) p q a (R c)
InjRP (forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @q a ~> (q % b1)
a ~> ((p :|||: q) % b)
f) ((Ob a1, Ob b1) => (:|||:) p q a b)
-> (a1 ~> b1) -> (:|||:) p q a b
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
r
  index :: forall (a :: k) (b :: COPRODUCT i j).
(:|||:) p q a b -> a ~> ((p :|||: q) % b)
index (InjLP p a b
p) = p a b -> a ~> (p % b)
forall (a :: k) (b :: i). 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
  index (InjRP q a b
q) = q a b -> a ~> (q % b)
forall (a :: k) (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 a b
q
  repMap :: forall (a :: COPRODUCT i j) (b :: COPRODUCT i j).
(a ~> b) -> ((p :|||: q) % a) ~> ((p :|||: q) % b)
repMap (InjL a1 ~> b1
f) = forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: i +-> k) (a :: i) (b :: i).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p a1 ~> b1
f
  repMap (InjR a1 ~> b1
f) = forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @q a1 ~> b1
f

instance HasBinaryCoproducts KIND where
  type K l || K r = K (COPRODUCT l r)
  lft :: forall (a :: KIND) (b :: KIND). (Ob a, Ob b) => a ~> (a || b)
lft = forall {c} {a} (p :: c +-> a). Profunctor p => Cat ('K c) ('K a)
forall (p :: UN 'K a +-> COPRODUCT (UN 'K a) (UN 'K b)).
Profunctor p =>
Cat ('K (UN 'K a)) ('K (COPRODUCT (UN 'K a) (UN 'K b)))
Cat @LftCat
  rgt :: forall (a :: KIND) (b :: KIND). (Ob a, Ob b) => b ~> (a || b)
rgt = forall {c} {a} (p :: c +-> a). Profunctor p => Cat ('K c) ('K a)
forall (p :: UN 'K b +-> COPRODUCT (UN 'K a) (UN 'K b)).
Profunctor p =>
Cat ('K (UN 'K b)) ('K (COPRODUCT (UN 'K a) (UN 'K b)))
Cat @RgtCat
  Cat @p ||| :: forall (x :: KIND) (a :: KIND) (y :: KIND).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Cat @q = forall {c} {a} (p :: c +-> a). Profunctor p => Cat ('K c) ('K a)
forall (p :: COPRODUCT j j +-> k).
Profunctor p =>
Cat ('K (COPRODUCT j j)) ('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)

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 {c} {a} (p :: c +-> a). Profunctor p => Cat ('K c) ('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 {c} {a} (p :: c +-> a). Profunctor p => Cat ('K c) ('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) = (Dual ('K (UN 'K b)) ** Dual ('K (UN 'K c)))
~> Dual ('K (UN 'K b) ** 'K (UN 'K c))
Cat
  ('K (UN 'K (Dual ('K (UN 'K b))), UN 'K (Dual ('K (UN 'K c)))))
  ('K (OPPOSITE (UN 'K b, UN 'K c)))
forall {k} (a :: k) (b :: k).
(CompactClosed k, Ob a, Ob b) =>
(Dual a ** Dual b) ~> Dual (a ** b)
combineDual Cat
  ('K (UN 'K (Dual ('K (UN 'K b))), UN 'K (Dual ('K (UN 'K c)))))
  ('K (OPPOSITE (UN 'K b, UN 'K c)))
-> Cat
     ('K (UN 'K a))
     ('K (UN 'K (Dual ('K (UN 'K b))), UN 'K (Dual ('K (UN 'K c)))))
-> Cat ('K (UN 'K a)) ('K (OPPOSITE (UN 'K b, UN 'K c)))
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: KIND) (c :: KIND) (a :: KIND).
Cat b c -> Cat a b -> Cat a c
. ('K (OPPOSITE (UN 'K c)) ** 'K (OPPOSITE (UN 'K b)))
~> ('K (OPPOSITE (UN 'K b)) ** 'K (OPPOSITE (UN 'K c)))
Cat
  ('K (k, OPPOSITE (UN 'K b)))
  ('K (UN 'K (Dual ('K (UN 'K b))), UN 'K (Dual ('K (UN 'K c)))))
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap Cat
  ('K (k, OPPOSITE (UN 'K b)))
  ('K (UN 'K (Dual ('K (UN 'K b))), UN 'K (Dual ('K (UN 'K c)))))
-> Cat ('K (UN 'K a)) ('K (k, OPPOSITE (UN 'K b)))
-> Cat
     ('K (UN 'K a))
     ('K (UN 'K (Dual ('K (UN 'K b))), UN 'K (Dual ('K (UN 'K c)))))
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: KIND) (c :: KIND) (a :: KIND).
Cat b c -> Cat a b -> Cat a c
. forall {c} {a} (p :: c +-> a). Profunctor p => Cat ('K c) ('K a)
forall (p :: UN 'K a +-> (k, OPPOSITE (UN 'K b))).
Profunctor p =>
Cat ('K (UN 'K a)) ('K (k, OPPOSITE (UN 'K b)))
Cat @(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 {c} {a} (p :: c +-> a). Profunctor p => Cat ('K c) ('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 (Swap (~>) (~>) :.: DistribDual :.: p))

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

type DualUnit :: OPPOSITE () +-> ()
data DualUnit a b where
  DualUnit :: DualUnit '() (OP '())
instance Profunctor (DualUnit :: OPPOSITE () +-> ()) where
  dimap :: forall (c :: ()) (a :: ()) (b :: OPPOSITE ()) (d :: OPPOSITE ()).
(c ~> a) -> (b ~> d) -> DualUnit a b -> DualUnit c d
dimap c ~> a
Unit c a
Unit (Op Unit b1 a1
Unit) DualUnit a b
DualUnit = DualUnit c d
DualUnit '() ('OP '())
DualUnit
  (Ob a, Ob b) => r
r \\ :: forall (a :: ()) (b :: OPPOSITE ()) r.
((Ob a, Ob b) => r) -> DualUnit a b -> r
\\ DualUnit a b
DualUnit = r
(Ob a, Ob b) => r
r
instance CompactClosed KIND where
  distribDual :: forall (a :: KIND) (b :: KIND).
(Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual = forall {c} {a} (p :: c +-> a). Profunctor p => Cat ('K c) ('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 @DistribDual
  dualUnit :: Dual Unit ~> Unit
dualUnit = forall {c} {a} (p :: c +-> a). Profunctor p => Cat ('K c) ('K a)
forall (p :: OPPOSITE () +-> ()).
Profunctor p =>
Cat ('K (OPPOSITE ())) ('K ())
Cat @DualUnit

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