{-# OPTIONS_GHC -Wno-orphans #-}

-- | Categories of __representable profunctors__: @'REPK' j k@ is the full subcategory of the
-- profunctor category on the 'Representable' profunctors, and @'COREPK' j k@ its counterpart of
-- (opposed) corepresentable ones. A representable profunctor is a functor in profunctor clothing,
-- so these play the role of functor categories between arbitrary kinds.
module Proarrow.Category.Instance.Rep where

import Data.Kind (Constraint)

import Proarrow.Category.Enriched.Thin (Thin, ThinProfunctor (..))
import Proarrow.Category.Instance.Opposite (OPPOSITE (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Sub (SUBCAT (..), Sub (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), UN, type (+->))
import Proarrow.Profunctor.Corepresentable (Corepresentable)
import Proarrow.Profunctor.Representable (Representable (..), repObj)

type REPK j k = SUBCAT (Representable :: j +-> k -> Constraint)
type REP (f :: j +-> k) = SUB f :: REPK j k

type OpCorepresentable :: OPPOSITE (j +-> k) -> Constraint
class (Corepresentable (UN OP p)) => OpCorepresentable p
instance (Corepresentable (UN OP p)) => OpCorepresentable p
type COREPK j k = SUBCAT (OpCorepresentable :: OPPOSITE (k +-> j) -> Constraint)
type COREP (f :: k +-> j) = SUB (OP f) :: COREPK j k

class (HasArrow (~>) (p % a) (q % a)) => HasArrowRep p q a
instance (HasArrow (~>) (p % a) (q % a)) => HasArrowRep p q a
class (forall a. (Ob a) => HasArrowRep p q a) => HasAllArrows (p :: j +-> k) (q :: j +-> k)
instance (forall a. (Ob a) => HasArrowRep p q a) => HasAllArrows (p :: j +-> k) (q :: j +-> k)

-- | The natural transformation @p ':~>' q@ obtained from a thin arrow @p % a '~>' q % a@ at every
-- object, i.e. the 'Proarrow.Category.Enriched.Thin.arr' of a thin structure on @'REPK' j k@.
--
-- It is no @'Proarrow.Category.Enriched.Thin.ThinProfunctor' ('Sub' 'Prof')@ instance, because the
-- converse 'Proarrow.Category.Enriched.Thin.withArr' would have to build the quantified
-- @'HasAllArrows' p q@ from per-@a@ evidence, which GHC cannot (cf. GHC issue #16502).
repArr
  :: forall {j} {k} (p :: j +-> k) q
   . (Thin k, Ob (REP p), Ob (REP q), HasAllArrows p q)
  => REP p ~> REP q
repArr :: forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Thin k, Ob (REP p), Ob (REP q), HasAllArrows p q) =>
REP p ~> REP q
repArr = Prof p q -> Sub Prof (REP p) (REP q)
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub ((p :~> q) -> Prof p q
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \ @_ @b p a b
p -> (a ~> (q % b)) -> q a b
forall (b :: j) (a :: k). 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 ((p % b) ~> (q % b)
forall (a :: k) (b :: k).
(Ob a, Ob b, HasArrow (Hom k) a b) =>
a ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr ((p % b) ~> (q % b)) -> (a ~> (p % b)) -> a ~> (q % b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a b -> a ~> (p % b)
forall (a :: k) (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) ((Ob (p % b), Ob (p % b)) => q a b)
-> ((p % b) ~> (p % b)) -> q a b
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
\\ forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
forall (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
repObj @p @b ((Ob (q % b), Ob (q % b)) => q a b)
-> ((q % b) ~> (q % b)) -> q a b
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
\\ forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
forall (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
repObj @q @b ((Ob a, Ob b) => q a b) -> p a b -> q a b
forall (a :: k) (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)