{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Category.Instance.Cat where

import Proarrow.Category.Instance.Product ((:**:)(..))
import Proarrow.Category.Instance.Unit (UNIT(..), Unit(..))
import Proarrow.Core (CAT, PRO, UN, Is, CategoryOf(..), Promonad(..), Profunctor(..), dimapDefault, Kind)
import Proarrow.Profunctor.Identity (Id)
import Proarrow.Profunctor.Composition ((:.:))
import Proarrow.Object.Terminal (HasTerminalObject(..))
import Proarrow.Object.BinaryProduct (HasBinaryProducts(..))


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

type Cat :: CAT KIND
data Cat a b where
  Cat :: Profunctor (p :: PRO j k) => Cat (K k) (K j)

-- | 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 b (p :: PRO a b). Profunctor p => Cat ('K b) ('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 b (p :: PRO a b). Profunctor p => Cat ('K b) ('K a)
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 :: PRO UNIT k
data Terminate a b where
  Terminate :: Ob b => Terminate U b
instance CategoryOf k => Profunctor (Terminate :: PRO UNIT k) where
  dimap :: forall (c :: UNIT) (a :: UNIT) (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 U d
(Ob b, Ob d) => Terminate c d
forall {k} (b :: k). Ob b => Terminate U 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 :: UNIT) (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 UNIT
  terminate' :: forall (a :: KIND). Obj a -> a ~> TerminalObject
terminate' (Cat @a) = forall a b (p :: PRO a b). Profunctor p => Cat ('K b) ('K a)
Cat @_ @_ @Terminate


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