Safe Haskell	None
Language	GHC2024

Proarrow.Category.Enriched

Description

Categories and profunctors enriched in a monoidal category v, encoded via their underlying ordinary category/profunctor: EnrichedProfunctor equips a regular profunctor with hom-objects ProObj v p a b in v from which the enriched structure is recovered, and a category is Enriched when its hom-profunctor is. Instances include the self-enrichment of a Closed category.

Synopsis

class (Monoidal v, Profunctor p, Enriched v j, Enriched v k) => EnrichedProfunctor v (p :: j +-> k) where
- type ProObj v (p :: j +-> k) (a :: k) (b :: j) :: v
- withProObj :: forall (a :: k) (b :: j) r. (Ob a, Ob b) => (Ob (ProObj v p a b) => r) -> r
- underlying :: forall (a :: k) (b :: j). p a b -> (Unit :: v) ~> ProObj v p a b
- enriched :: forall (a :: k) (b :: j). (Ob a, Ob b) => ((Unit :: v) ~> ProObj v p a b) -> p a b
- rmap :: forall (a :: k) (b :: j) (c :: j). (Ob a, Ob b, Ob c) => (HomObj v b c ** ProObj v p a b) ~> ProObj v p a c
- lmap :: forall (a :: k) (b :: j) (c :: k). (Ob a, Ob b, Ob c) => (HomObj v c a ** ProObj v p a b) ~> ProObj v p c b
class EnrichedProfunctor v (Hom k) => Enriched v k
type HomObj v (a :: k) (b :: k) = ProObj v (Hom k) a b
comp :: forall {k} v (a :: k) (b :: k) (c :: k). (Enriched v k, Ob a, Ob b, Ob c) => (HomObj v b c ** HomObj v a b) ~> HomObj v a c
type HomSelf (a :: k) (b :: k) = a ~~> b
underlyingSelf :: forall k (a :: k) (b :: k). Closed k => (a ~> b) -> (Unit :: k) ~> HomSelf a b
enrichedSelf :: forall k (a :: k) (b :: k). (Closed k, Ob a, Ob b) => ((Unit :: k) ~> HomSelf a b) -> a ~> b
compSelf :: forall {k} (a :: k) (b :: k) (c :: k). (Closed k, Ob a, Ob b, Ob c) => (HomSelf b c ** HomSelf a b) ~> HomSelf a c
type Clone k = SUBCAT (Any :: k -> Constraint)
fromFls :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (h :: BOOL). Decision p a b h -> Booleans 'FLS h
data GenArrow (n :: OPPOSITE v) (a :: k) (b :: k) where
- GenArrow :: forall {k} (a :: k) (b :: k) v (n1 :: v). (Ob a, Ob b) => (n1 ~> HomObj v a b) -> GenArrow ('OP n1) a b

Documentation

class (Monoidal v, Profunctor p, Enriched v j, Enriched v k) => EnrichedProfunctor v (p :: j +-> k) where Source Github #

Working with enriched categories and profunctors in Haskell is hard. Instead we encode them using the underlying regular category/profunctor, and show that the enriched structure can be recovered.

Call an arrow Unit ~> x an element of x. The laws say that the elements of ProObj v p a b are those of the hom-set p a b, and that its two actions are the profunctor's:

Elements: underlying and enriched are mutually inverse, so underlying is a bijection from p a b onto the elements of ProObj v p a b.
Right action: for f :: b ~> c in j and x :: p a b, where underlying f names f as an element of HomObj v b c:

rmap . (underlying f ** underlying x) . leftUnitorInv == underlying (P.rmap f x)

Left action: dually, for g :: c ~> a in k:

lmap . (underlying g ** underlying x) . leftUnitorInv == underlying (P.lmap g x)

These fix rmap and lmap completely iff v is well-pointed, as Type and the thin vs are. Functoriality follows from the Profunctor instance. At p ~ Hom k the right-action law says that the enriched composition comp is (.).

Associated Types

type ProObj v (p :: j +-> k) (a :: k) (b :: j) :: v Source Github #

Methods

withProObj :: forall (a :: k) (b :: j) r. (Ob a, Ob b) => (Ob (ProObj v p a b) => r) -> r Source Github #

underlying :: forall (a :: k) (b :: j). p a b -> (Unit :: v) ~> ProObj v p a b Source Github #

enriched :: forall (a :: k) (b :: j). (Ob a, Ob b) => ((Unit :: v) ~> ProObj v p a b) -> p a b Source Github #

rmap :: forall (a :: k) (b :: j) (c :: j). (Ob a, Ob b, Ob c) => (HomObj v b c ** ProObj v p a b) ~> ProObj v p a c Source Github #

lmap :: forall (a :: k) (b :: j) (c :: k). (Ob a, Ob b, Ob c) => (HomObj v c a ** ProObj v p a b) ~> ProObj v p c b Source Github #

Instances

Instances details

(DecidableProfunctor p, Decidable j, Decidable k) => EnrichedProfunctor BOOL (p :: j +-> k) Source Github #	A decidable thin profunctor is a profunctor enriched in the walking arrow: its hom-object is the type-level `Holds`, an element of it is an arrow, and composition is conjunction.
Instance details Defined in Proarrow.Category.Enriched Methods withProObj :: forall (a :: k) (b :: j) r. (Ob a, Ob b) => (Ob (ProObj BOOL p a b) => r) -> r Source Github # underlying :: forall (a :: k) (b :: j). p a b -> (Unit :: BOOL) ~> ProObj BOOL p a b Source Github # enriched :: forall (a :: k) (b :: j). (Ob a, Ob b) => ((Unit :: BOOL) ~> ProObj BOOL p a b) -> p a b Source Github # rmap :: forall (a :: k) (b :: j) (c :: j). (Ob a, Ob b, Ob c) => (HomObj BOOL b c ProObj BOOL p a b) ~> ProObj BOOL p a c Source Github # lmap :: forall (a :: k) (b :: j) (c :: k). (Ob a, Ob b, Ob c) => (HomObj BOOL c a ProObj BOOL p a b) ~> ProObj BOOL p c b Source Github #
(ThinProfunctor p, Thin j, Thin k) => EnrichedProfunctor CONSTRAINT (p :: j +-> k) Source Github #
Instance details Defined in Proarrow.Category.Enriched Methods withProObj :: forall (a :: k) (b :: j) r. (Ob a, Ob b) => (Ob (ProObj CONSTRAINT p a b) => r) -> r Source Github # underlying :: forall (a :: k) (b :: j). p a b -> (Unit :: CONSTRAINT) ~> ProObj CONSTRAINT p a b Source Github # enriched :: forall (a :: k) (b :: j). (Ob a, Ob b) => ((Unit :: CONSTRAINT) ~> ProObj CONSTRAINT p a b) -> p a b Source Github # rmap :: forall (a :: k) (b :: j) (c :: j). (Ob a, Ob b, Ob c) => (HomObj CONSTRAINT b c ProObj CONSTRAINT p a b) ~> ProObj CONSTRAINT p a c Source Github # lmap :: forall (a :: k) (b :: j) (c :: k). (Ob a, Ob b, Ob c) => (HomObj CONSTRAINT c a ProObj CONSTRAINT p a b) ~> ProObj CONSTRAINT p c b Source Github #
(Finitary p, LocallyFinite j, LocallyFinite k) => EnrichedProfunctor FINHASK (p :: j +-> k) Source Github #	A finitary profunctor is a profunctor enriched in finite sets. The hom-object is the hom-set itself, which `Elt` makes an object of `FINHASK` out of nothing but the numbering, and the whiskerings are the two `dimap`s.
Instance details Defined in Proarrow.Category.Enriched Methods withProObj :: forall (a :: k) (b :: j) r. (Ob a, Ob b) => (Ob (ProObj FINHASK p a b) => r) -> r Source Github # underlying :: forall (a :: k) (b :: j). p a b -> (Unit :: FINHASK) ~> ProObj FINHASK p a b Source Github # enriched :: forall (a :: k) (b :: j). (Ob a, Ob b) => ((Unit :: FINHASK) ~> ProObj FINHASK p a b) -> p a b Source Github # rmap :: forall (a :: k) (b :: j) (c :: j). (Ob a, Ob b, Ob c) => (HomObj FINHASK b c ProObj FINHASK p a b) ~> ProObj FINHASK p a c Source Github # lmap :: forall (a :: k) (b :: j) (c :: k). (Ob a, Ob b, Ob c) => (HomObj FINHASK c a ProObj FINHASK p a b) ~> ProObj FINHASK p c b Source Github #
CodiscreteProfunctor p => EnrichedProfunctor () (p :: j +-> k) Source Github #
Instance details Defined in Proarrow.Category.Enriched Methods withProObj :: forall (a :: k) (b :: j) r. (Ob a, Ob b) => (Ob (ProObj () p a b) => r) -> r Source Github # underlying :: forall (a :: k) (b :: j). p a b -> (Unit :: ()) ~> ProObj () p a b Source Github # enriched :: forall (a :: k) (b :: j). (Ob a, Ob b) => ((Unit :: ()) ~> ProObj () p a b) -> p a b Source Github # rmap :: forall (a :: k) (b :: j) (c :: j). (Ob a, Ob b, Ob c) => (HomObj () b c ProObj () p a b) ~> ProObj () p a c Source Github # lmap :: forall (a :: k) (b :: j) (c :: k). (Ob a, Ob b, Ob c) => (HomObj () c a ProObj () p a b) ~> ProObj () p c b Source Github #
Profunctor p => EnrichedProfunctor Type (p :: j +-> k) Source Github #
Instance details Defined in Proarrow.Category.Enriched Methods withProObj :: forall (a :: k) (b :: j) r. (Ob a, Ob b) => (Ob (ProObj Type p a b) => r) -> r Source Github # underlying :: forall (a :: k) (b :: j). p a b -> (Unit :: Type) ~> ProObj Type p a b Source Github # enriched :: forall (a :: k) (b :: j). (Ob a, Ob b) => ((Unit :: Type) ~> ProObj Type p a b) -> p a b Source Github # rmap :: forall (a :: k) (b :: j) (c :: j). (Ob a, Ob b, Ob c) => (HomObj Type b c ProObj Type p a b) ~> ProObj Type p a c Source Github # lmap :: forall (a :: k) (b :: j) (c :: k). (Ob a, Ob b, Ob c) => (HomObj Type c a ProObj Type p a b) ~> ProObj Type p c b Source Github #
(SNatI n, EnrichedProfunctor COST p, Enriched COST k, Enumerable k) => EnrichedProfunctor COST (Walk n p :: k -> k -> Type) Source Github #	Walks along a `COST`-weighted graph form the free Lawvere metric space on it: `withProObj` runs the fixed point that computes the shortest distances, `underlying` and `enriched` relate a walk of zero-cost pieces to a zero distance, and the actions of the base are the triangle inequality.
Instance details Defined in Proarrow.Category.Enriched.Thin.Composition Methods withProObj :: forall (a :: k) (b :: k) r. (Ob a, Ob b) => (Ob (ProObj COST (Walk n p) a b) => r) -> r Source Github # underlying :: forall (a :: k) (b :: k). Walk n p a b -> (Unit :: COST) ~> ProObj COST (Walk n p) a b Source Github # enriched :: forall (a :: k) (b :: k). (Ob a, Ob b) => ((Unit :: COST) ~> ProObj COST (Walk n p) a b) -> Walk n p a b Source Github # rmap :: forall (a :: k) (b :: k) (c :: k). (Ob a, Ob b, Ob c) => (HomObj COST b c ProObj COST (Walk n p) a b) ~> ProObj COST (Walk n p) a c Source Github # lmap :: forall (a :: k) (b :: k) (c :: k). (Ob a, Ob b, Ob c) => (HomObj COST c a ProObj COST (Walk n p) a b) ~> ProObj COST (Walk n p) c b Source Github #
DaggerProfunctor p => EnrichedProfunctor (Type, Type) (p :: j +-> j) Source Github #
Instance details Defined in Proarrow.Category.Enriched Methods withProObj :: forall (a :: j) (b :: j) r. (Ob a, Ob b) => (Ob (ProObj (Type, Type) p a b) => r) -> r Source Github # underlying :: forall (a :: j) (b :: j). p a b -> (Unit :: (Type, Type)) ~> ProObj (Type, Type) p a b Source Github # enriched :: forall (a :: j) (b :: j). (Ob a, Ob b) => ((Unit :: (Type, Type)) ~> ProObj (Type, Type) p a b) -> p a b Source Github # rmap :: forall (a :: j) (b :: j) (c :: j). (Ob a, Ob b, Ob c) => (HomObj (Type, Type) b c ProObj (Type, Type) p a b) ~> ProObj (Type, Type) p a c Source Github # lmap :: forall (a :: j) (b :: j) (c :: j). (Ob a, Ob b, Ob c) => (HomObj (Type, Type) c a ProObj (Type, Type) p a b) ~> ProObj (Type, Type) p c b Source Github #
Indexed k => EnrichedProfunctor COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Discrete Methods withProObj :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. (Ob a, Ob b) => (Ob (ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) => r) -> r Source Github # underlying :: forall (a :: DISCRETE k) (b :: DISCRETE k). Discrete a b -> (Unit :: COST) ~> ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b Source Github # enriched :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b) => ((Unit :: COST) ~> ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) -> Discrete a b Source Github # rmap :: forall (a :: DISCRETE k) (b :: DISCRETE k) (c :: DISCRETE k). (Ob a, Ob b, Ob c) => (HomObj COST b c ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) ~> ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a c Source Github # lmap :: forall (a :: DISCRETE k) (b :: DISCRETE k) (c :: DISCRETE k). (Ob a, Ob b, Ob c) => (HomObj COST c a ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) ~> ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) c b Source Github #
(Indexed k, KnownEdges es) => EnrichedProfunctor COST (Edges es :: DISCRETE k -> DISCRETE k -> Type) Source Github #	A graph with `COST` weights: a weighted graph, whose closure is shortest paths.
Instance details Defined in Proarrow.Profunctor.Instance.Edges Methods withProObj :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. (Ob a, Ob b) => (Ob (ProObj COST (Edges es) a b) => r) -> r Source Github # underlying :: forall (a :: DISCRETE k) (b :: DISCRETE k). Edges es a b -> (Unit :: COST) ~> ProObj COST (Edges es) a b Source Github # enriched :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b) => ((Unit :: COST) ~> ProObj COST (Edges es) a b) -> Edges es a b Source Github # rmap :: forall (a :: DISCRETE k) (b :: DISCRETE k) (c :: DISCRETE k). (Ob a, Ob b, Ob c) => (HomObj COST b c ProObj COST (Edges es) a b) ~> ProObj COST (Edges es) a c Source Github # lmap :: forall (a :: DISCRETE k) (b :: DISCRETE k) (c :: DISCRETE k). (Ob a, Ob b, Ob c) => (HomObj COST c a ProObj COST (Edges es) a b) ~> ProObj COST (Edges es) c b Source Github #
EnrichedProfunctor v p => EnrichedProfunctor (Clone v) (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Github #
Instance details Defined in Proarrow.Category.Enriched Methods withProObj :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) r. (Ob a, Ob b) => (Ob (ProObj (Clone v) (Op p) a b) => r) -> r Source Github # underlying :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). Op p a b -> (Unit :: Clone v) ~> ProObj (Clone v) (Op p) a b Source Github # enriched :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). (Ob a, Ob b) => ((Unit :: Clone v) ~> ProObj (Clone v) (Op p) a b) -> Op p a b Source Github # rmap :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) (c :: OPPOSITE k). (Ob a, Ob b, Ob c) => (HomObj (Clone v) b c ProObj (Clone v) (Op p) a b) ~> ProObj (Clone v) (Op p) a c Source Github # lmap :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) (c :: OPPOSITE j). (Ob a, Ob b, Ob c) => (HomObj (Clone v) c a ProObj (Clone v) (Op p) a b) ~> ProObj (Clone v) (Op p) c b Source Github #
(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 #
Monoid m => EnrichedProfunctor (Clone k) (Mon :: MONOID m -> MONOID m -> Type) Source Github #	A monoid is a one object enriched category.
Instance details Defined in Proarrow.Category.Enriched Methods withProObj :: forall (a :: MONOID m) (b :: MONOID m) r. (Ob a, Ob b) => (Ob (ProObj (Clone k) (Mon :: MONOID m -> MONOID m -> Type) a b) => r) -> r Source Github # underlying :: forall (a :: MONOID m) (b :: MONOID m). Mon a b -> (Unit :: Clone k) ~> ProObj (Clone k) (Mon :: MONOID m -> MONOID m -> Type) a b Source Github # enriched :: forall (a :: MONOID m) (b :: MONOID m). (Ob a, Ob b) => ((Unit :: Clone k) ~> ProObj (Clone k) (Mon :: MONOID m -> MONOID m -> Type) a b) -> Mon a b Source Github # rmap :: forall (a :: MONOID m) (b :: MONOID m) (c :: MONOID m). (Ob a, Ob b, Ob c) => (HomObj (Clone k) b c ProObj (Clone k) (Mon :: MONOID m -> MONOID m -> Type) a b) ~> ProObj (Clone k) (Mon :: MONOID m -> MONOID m -> Type) a c Source Github # lmap :: forall (a :: MONOID m) (b :: MONOID m) (c :: MONOID m). (Ob a, Ob b, Ob c) => (HomObj (Clone k) c a ProObj (Clone k) (Mon :: MONOID m -> MONOID m -> Type) a b) ~> ProObj (Clone k) (Mon :: MONOID m -> MONOID m -> Type) c b Source Github #

class EnrichedProfunctor v (Hom k) => Enriched v k Source Github #

Instances

Instances details

EnrichedProfunctor v (Hom k) => Enriched v k Source Github #
Instance details Defined in Proarrow.Category.Enriched

type HomObj v (a :: k) (b :: k) = ProObj v (Hom k) a b Source Github #

comp :: forall {k} v (a :: k) (b :: k) (c :: k). (Enriched v k, Ob a, Ob b, Ob c) => (HomObj v b c ** HomObj v a b) ~> HomObj v a c Source Github #

type HomSelf (a :: k) (b :: k) = a ~~> b Source Github #

Closed monoidal categories are enriched in themselves.

underlyingSelf :: forall k (a :: k) (b :: k). Closed k => (a ~> b) -> (Unit :: k) ~> HomSelf a b Source Github #

enrichedSelf :: forall k (a :: k) (b :: k). (Closed k, Ob a, Ob b) => ((Unit :: k) ~> HomSelf a b) -> a ~> b Source Github #

compSelf :: forall {k} (a :: k) (b :: k) (c :: k). (Closed k, Ob a, Ob b, Ob c) => (HomSelf b c ** HomSelf a b) ~> HomSelf a c Source Github #

type Clone k = SUBCAT (Any :: k -> Constraint) Source Github #

fromFls :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (h :: BOOL). Decision p a b h -> Booleans 'FLS h Source Github #

FLS is initial, and a decision tells us which object we are aiming at.

data GenArrow (n :: OPPOSITE v) (a :: k) (b :: k) where Source Github #

A generalized arrow of an enriched category. If k is both powered and copowered, this is an adjunction.

Constructors

GenArrow :: forall {k} (a :: k) (b :: k) v (n1 :: v). (Ob a, Ob b) => (n1 ~> HomObj v a b) -> GenArrow ('OP n1) a b

Instances

Instances details

(Ob n, Enriched v k, CategoryOf k) => Profunctor (GenArrow ('OP n) :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Category.Enriched Methods dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> GenArrow ('OP n) a b -> GenArrow ('OP n) c d Source Github # lmap :: forall (c :: k) (a :: k) (b :: k). (c ~> a) -> GenArrow ('OP n) a b -> GenArrow ('OP n) c b Source Github # rmap :: forall (b :: k) (d :: k) (a :: k). (b ~> d) -> GenArrow ('OP n) a b -> GenArrow ('OP n) a d Source Github # (\\) :: forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> GenArrow ('OP n) a b -> r Source Github #
(Copowered v k, Ob n) => Corepresentable (GenArrow ('OP n) :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Colimit.Copower Methods coindex :: forall (a :: k) (b :: k). GenArrow ('OP n) a b -> ((GenArrow ('OP n) :: k -> k -> Type) %% a) ~> b Source Github # cotabulate :: forall (a :: k) (b :: k). Ob a => (((GenArrow ('OP n) :: k -> k -> Type) %% a) ~> b) -> GenArrow ('OP n) a b Source Github # corepMap :: forall (a :: k) (b :: k). (a ~> b) -> ((GenArrow ('OP n) :: k -> k -> Type) %% a) ~> ((GenArrow ('OP n) :: k -> k -> Type) %% b) Source Github # corepUniv :: forall (a :: k). Ob a => GenArrow ('OP n) a ((GenArrow ('OP n) :: k -> k -> Type) %% a) Source Github #
(Powered v k, Ob n) => Representable (GenArrow ('OP n) :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Limit.Power Methods index :: forall (a :: k) (b :: k). GenArrow ('OP n) a b -> a ~> ((GenArrow ('OP n) :: k -> k -> Type) % b) Source Github # tabulate :: forall (b :: k) (a :: k). Ob b => (a ~> ((GenArrow ('OP n) :: k -> k -> Type) % b)) -> GenArrow ('OP n) a b Source Github # repMap :: forall (a :: k) (b :: k). (a ~> b) -> ((GenArrow ('OP n) :: k -> k -> Type) % a) ~> ((GenArrow ('OP n) :: k -> k -> Type) % b) Source Github # repUniv :: forall (a :: k). Ob a => GenArrow ('OP n) ((GenArrow ('OP n) :: k -> k -> Type) % a) a Source Github #
type (GenArrow ('OP n) :: k -> k -> Type) %% (a :: k) Source Github #
Instance details Defined in Proarrow.Colimit.Copower type (GenArrow ('OP n) :: k -> k -> Type) %% (a :: k) = n *. a
type (GenArrow ('OP n) :: k -> k -> Type) % (a :: k) Source Github #
Instance details Defined in Proarrow.Limit.Power type (GenArrow ('OP n) :: k -> k -> Type) % (a :: k) = a ^ n