{-# OPTIONS_GHC -Wno-orphans #-}
module Proarrow.Category.Instance.Rep where

import Data.Kind (Constraint)

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

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)
instance (Thin k) => ThinProfunctor (Sub Prof :: CAT (REPK j k)) where
  type HasArrow (Sub Prof :: CAT (REPK j k)) (REP p) (REP q) = HasAllArrows p q
  arr :: forall (a :: REPK j k) (b :: REPK j k).
(Ob a, Ob b, HasArrow (Sub Prof) a b) =>
Sub Prof a b
arr @(REP p) @(REP q) = Prof (UN SUB a) (UN SUB b)
-> Sub Prof (SUB (UN SUB a)) (SUB (UN SUB b))
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 ((UN SUB a :~> UN SUB b) -> Prof (UN SUB a) (UN SUB b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \ @_ @b UN SUB a a b
p -> (a ~> (UN SUB b % b)) -> UN SUB b a b
forall (b :: j) (a :: k).
Ob b =>
(a ~> (UN SUB b % b)) -> UN SUB b a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate ((UN SUB a % b) ~> (UN SUB b % 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 ((UN SUB a % b) ~> (UN SUB b % b))
-> (a ~> (UN SUB a % b)) -> a ~> (UN SUB b % b)
forall (b :: k) (c :: k) (a :: k). (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
. UN SUB a a b -> a ~> (UN SUB a % b)
forall (a :: k) (b :: j). UN SUB a a b -> a ~> (UN SUB a % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index UN SUB a a b
p) ((Ob (UN SUB a % b), Ob (UN SUB a % b)) => UN SUB b a b)
-> ((UN SUB a % b) ~> (UN SUB a % b)) -> UN SUB b 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 (UN SUB b % b), Ob (UN SUB b % b)) => UN SUB b a b)
-> ((UN SUB b % b) ~> (UN SUB b % b)) -> UN SUB b 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) => UN SUB b a b) -> UN SUB a a b -> UN SUB b a b
forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> UN SUB a 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
\\ UN SUB a a b
p)
  withArr :: forall (a :: REPK j k) (b :: REPK j k) r.
Sub Prof a b -> (HasArrow (Sub Prof) a b => r) -> r
withArr = Sub Prof a b -> (HasArrow (Sub Prof) a b => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> (HasArrow p a b => r) -> r
forall (a :: REPK j k) (b :: REPK j k) r.
Sub Prof a b -> (HasArrow (Sub Prof) a b => r) -> r
withArr -- TODO, impossible?
  -- withArr @p @q (Sub (Prof n)) r = withArr @((~>) :: CAT k) (index (n trivialRep)) r