Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Prof

Contents

Orphan instances

Description

The category of profunctors j +-> k themselves: Prof wraps a natural transformation p :~> q, making the profunctor kind a category with profunctors as objects. This is one hom-category of the bicategory of profunctors; the full bicategorical structure lives in the proarrow-equipment package.

Documentation

data Prof (p :: j +-> k) (q :: j +-> k) where Source Github #

Constructors

Prof
Fields :: forall {j} {k} (p :: j +-> k) (q :: j +-> k). (Profunctor p, Profunctor q) => { unProf :: p :~> q } -> Prof p q

Instances

Instances details

(CategoryOf j, CategoryOf k) => EnrichedProfunctor (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type) :: PROD (j +-> k) -> PROD (j +-> k) -> Type) Source Github #	The category of profunctors is enriched in itself: the hom-object is the internal hom `p :~>: q`, an element of it is a natural transformation, and composition is the internal one. Cartesian closed, hence the `PROD` wrapper (`j +-> k`'s own tensor is Day convolution). This self-enrichment is written the generic way, from `HomSelf` and friends. Those apply to any `Closed` `SymMonoidal` kind that has no enrichment instance of its own covering its hom-profunctor.
Instance details Defined in Proarrow.Category.Enriched Methods withProObj :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) r. (Ob a, Ob b) => (Ob (ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) a b) => r) -> r Source Github # underlying :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)). Prod (Prof :: (j +-> k) -> (j +-> k) -> Type) a b -> (Unit :: PROD (j +-> k)) ~> ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) a b Source Github # enriched :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)). (Ob a, Ob b) => ((Unit :: PROD (j +-> k)) ~> ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) a b) -> Prod (Prof :: (j +-> k) -> (j +-> k) -> Type) a b Source Github # rmap :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) (c :: PROD (j +-> k)). (Ob a, Ob b, Ob c) => (HomObj (PROD (j +-> k)) b c ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) a b) ~> ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) a c Source Github # lmap :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) (c :: PROD (j +-> k)). (Ob a, Ob b, Ob c) => (HomObj (PROD (j +-> k)) c a ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) a b) ~> ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type)) c b Source Github #
(CategoryOf j, CategoryOf k) => Strong (ProdAction :: (j +-> k) -> (PROD (j +-> k), j +-> k) -> Type) (Prof :: (j +-> k) -> (j +-> k) -> Type) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.Strength Methods act :: forall (a :: PROD (j +-> k)) (x :: j +-> k) (y :: j +-> k). Ob a => Prof x y -> Prof (Act (ProdAction :: (j +-> k) -> (PROD (j +-> k), j +-> k) -> Type) a x) (Act (ProdAction :: (j +-> k) -> (PROD (j +-> k), j +-> k) -> Type) a y) Source Github #
Promonad (Prof :: (j +-> k) -> (j +-> k) -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Prof Methods id :: forall (a :: j +-> k). Ob a => Prof a a Source Github # (.) :: forall (b :: j +-> k) (c :: j +-> k) (a :: j +-> k). Prof b c -> Prof a b -> Prof a c Source Github #
(Monoidal j, Monoidal k) => MonoidalProfunctor (Prof :: (j +-> k) -> (j +-> k) -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Day Methods one :: Prof (Unit :: j +-> k) (Unit :: j +-> k) Source Github # () :: forall (x1 :: j +-> k) (x2 :: j +-> k) (y1 :: j +-> k) (y2 :: j +-> k). Prof x1 x2 -> Prof y1 y2 -> Prof (x1 y1) (x2 ** y2) Source Github #
Profunctor (Prof :: (j +-> k) -> (j +-> k) -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Prof Methods dimap :: forall (c :: j +-> k) (a :: j +-> k) (b :: j +-> k) (d :: j +-> k). (c ~> a) -> (b ~> d) -> Prof a b -> Prof c d Source Github # lmap :: forall (c :: j +-> k) (a :: j +-> k) (b :: j +-> k). (c ~> a) -> Prof a b -> Prof c b Source Github # rmap :: forall (b :: j +-> k) (d :: j +-> k) (a :: j +-> k). (b ~> d) -> Prof a b -> Prof a d Source Github # (\\) :: forall (a :: j +-> k) (b :: j +-> k) r. ((Ob a, Ob b) => r) -> Prof a b -> r Source Github #
(FiniteCat j, FiniteCat k, forall (p :: j +-> k). ob p => SubFinitary p) => Finitary (Sub (Prof :: (j +-> k) -> (j +-> k) -> Type) :: SUBCAT ob -> SUBCAT ob -> Type) Source Github #	`FINITARY j k` is locally finite: its own hom-profunctor is finitary, by `natTransformations`, so the numbering is the skeleton of each hom-set and the `Finitary` laws apply to it. (It is not a `FiniteCat`: there are unboundedly many finitary profunctors.) The same holds for any full subcategory whose predicate implies `Finitary`, such as the sheaves of Proarrow.Category.Enriched.Finitary.Sheaf. The premise goes through `SubFinitary` because a bare `forall p. ob p => Finitary p` cannot be discharged for a conjunction such as `Finitary :&&: Sheaf t`: GHC will not solve the head from a superclass that is not smaller.
Instance details Defined in Proarrow.Category.Enriched.Finitary.Topos Methods size :: forall (a :: SUBCAT ob) (b :: SUBCAT ob). (Ob a, Ob b) => Natural Source Github # toIndex :: forall (a :: SUBCAT ob) (b :: SUBCAT ob). (Ob a, Ob b) => Sub (Prof :: (j +-> k) -> (j +-> k) -> Type) a b -> Natural Source Github # fromIndex :: forall (a :: SUBCAT ob) (b :: SUBCAT ob). (Ob a, Ob b) => Natural -> Sub (Prof :: (j +-> k) -> (j +-> k) -> Type) a b Source Github # elements :: forall (a :: SUBCAT ob) (b :: SUBCAT ob). (Ob a, Ob b) => [Sub (Prof :: (j +-> k) -> (j +-> k) -> Type) a b] Source Github #
type ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type) :: PROD (j +-> k) -> PROD (j +-> k) -> Type) (p :: PROD (j +-> k)) (q :: PROD (j +-> k)) Source Github #
Instance details Defined in Proarrow.Category.Enriched type ProObj (PROD (j +-> k)) (Prod (Prof :: (j +-> k) -> (j +-> k) -> Type) :: PROD (j +-> k) -> PROD (j +-> k) -> Type) (p :: PROD (j +-> k)) (q :: PROD (j +-> k)) = HomSelf p q

Orphan instances

CategoryOf (j +-> k) Source Github #

The category of profunctors and natural transformations between them.

Instance details

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.Prof type (~>) = Prof :: (j +-> k) -> (j +-> k) -> Type