Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Rep

Description

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.

Synopsis

type REPK j k = SUBCAT (Representable :: (j +-> k) -> Constraint)
type REP (f :: j +-> k) = 'SUB f :: SUBCAT (Representable :: (j +-> k) -> Constraint)
class Corepresentable (UN ('OP :: (j +-> k) -> OPPOSITE (j +-> k)) p) => OpCorepresentable (p :: OPPOSITE (j +-> k))
type COREPK j k = SUBCAT (OpCorepresentable :: OPPOSITE (k +-> j) -> Constraint)
type COREP (f :: k +-> j) = 'SUB ('OP f) :: SUBCAT (OpCorepresentable :: OPPOSITE (k +-> j) -> Constraint)
class HasArrow ((~>) :: CAT j1) (p % a) (q % a) => HasArrowRep (p :: j +-> j1) (q :: j +-> j1) (a :: j)
class (forall (a :: j). Ob a => HasArrowRep p q a) => HasAllArrows (p :: j +-> k) (q :: j +-> k)
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

Documentation

type REPK j k = SUBCAT (Representable :: (j +-> k) -> Constraint) Source Github #

type REP (f :: j +-> k) = 'SUB f :: SUBCAT (Representable :: (j +-> k) -> Constraint) Source Github #

class Corepresentable (UN ('OP :: (j +-> k) -> OPPOSITE (j +-> k)) p) => OpCorepresentable (p :: OPPOSITE (j +-> k)) Source Github #

Instances

Instances details

Corepresentable (UN ('OP :: (j +-> k) -> OPPOSITE (j +-> k)) p) => OpCorepresentable (p :: OPPOSITE (j +-> k)) Source Github #
Instance details Defined in Proarrow.Category.Instance.Rep

type COREPK j k = SUBCAT (OpCorepresentable :: OPPOSITE (k +-> j) -> Constraint) Source Github #

type COREP (f :: k +-> j) = 'SUB ('OP f) :: SUBCAT (OpCorepresentable :: OPPOSITE (k +-> j) -> Constraint) Source Github #

class HasArrow ((~>) :: CAT j1) (p % a) (q % a) => HasArrowRep (p :: j +-> j1) (q :: j +-> j1) (a :: j) Source Github #

Instances

Instances details

HasArrow ((~>) :: CAT j2) (p % a) (q % a) => HasArrowRep (p :: j1 +-> j2) (q :: j1 +-> j2) (a :: j1) Source Github #
Instance details Defined in Proarrow.Category.Instance.Rep

class (forall (a :: j). Ob a => HasArrowRep p q a) => HasAllArrows (p :: j +-> k) (q :: j +-> k) Source Github #

Instances

Instances details

(forall (a :: j). Ob a => HasArrowRep p q a) => HasAllArrows (p :: j +-> k) (q :: j +-> k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Rep

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 Source Github #

The natural transformation p :~> q obtained from a thin arrow p % a ~> q % a at every object, i.e. the arr of a thin structure on REPK j k.

It is no ThinProfunctor (Sub Prof) instance, because the converse withArr would have to build the quantified HasAllArrows p q from per-a evidence, which GHC cannot (cf. GHC issue #16502).