Safe Haskell	None
Language	GHC2024

Proarrow.Category.Opposite

Documentation

newtype OPPOSITE k Source Comments #

Constructors

OP k

Instances

Instances details

(Powered v k, Enriched v (OPPOSITE k), forall (a :: k) (b :: k). HomObjOp v a b) => Copowered v (OPPOSITE k) Source Comments #

Instance details

Defined in Proarrow.Object.Copower

Methods

withObCopower :: forall (a :: OPPOSITE k) (n :: v) r. (Ob a, Ob n) => (Ob (n *. a) => r) -> r Source Comments #

copower :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (n :: v). (Ob a, Ob b) => (n ~> HomObj v a b) -> (n *. a) ~> b Source Comments #

uncopower :: forall (a :: OPPOSITE k) (n :: v) (b :: OPPOSITE k). (Ob a, Ob n) => ((n *. a) ~> b) -> n ~> HomObj v a b Source Comments #

(Copowered v k, Enriched v (OPPOSITE k), forall (a :: k) (b :: k). HomObjOp v a b) => Powered v (OPPOSITE k) Source Comments #

Instance details

Defined in Proarrow.Object.Copower

Methods

withObPower :: forall (a :: OPPOSITE k) (n :: v) r. (Ob a, Ob n) => (Ob (a ^ n) => r) -> r Source Comments #

power :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (n :: v). (Ob a, Ob b) => (n ~> HomObj v a b) -> a ~> (b ^ n) Source Comments #

unpower :: forall (b :: OPPOSITE k) (n :: v) (a :: OPPOSITE k). (Ob b, Ob n) => (a ~> (b ^ n)) -> n ~> HomObj v a b Source Comments #

CategoryOf k => Profunctor (Hom :: (OPPOSITE k, k) -> () -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Colimit

Methods

dimap :: forall (c :: (OPPOSITE k, k)) (a :: (OPPOSITE k, k)) (b :: ()) (d :: ()). (c ~> a) -> (b ~> d) -> Hom a b -> Hom c d Source Comments #

(\\) :: forall (a :: (OPPOSITE k, k)) (b :: ()) r. ((Ob a, Ob b) => r) -> Hom a b -> r Source Comments #

CategoryOf k => HasLimits (Hom :: () -> (OPPOSITE k, k) -> Type) Type Source Comments #

Instance details

Defined in Proarrow.Category.Limit

Methods

limit :: forall (d :: (OPPOSITE k, k) +-> Type). Representable d => (Limit (Hom :: () -> (OPPOSITE k, k) -> Type) d :.: (Hom :: () -> (OPPOSITE k, k) -> Type)) :~> d Source Comments #

limitUniv :: forall (d :: (OPPOSITE k, k) +-> Type) (p :: () +-> Type). (Representable d, Profunctor p) => ((p :.: (Hom :: () -> (OPPOSITE k, k) -> Type)) :~> d) -> p :~> Limit (Hom :: () -> (OPPOSITE k, k) -> Type) d Source Comments #

(CategoryOf j, CategoryOf k) => Functor (Yo :: k -> OPPOSITE j -> k -> j -> Type) Source Comments #

Instance details

Defined in Proarrow.Profunctor.Yoneda

Methods

map :: forall (a :: k) (b :: k). (a ~> b) -> (Yo a :: OPPOSITE j -> k -> j -> Type) ~> (Yo b :: OPPOSITE j -> k -> j -> Type) Source Comments #

(Profunctor p, CategoryOf i, CategoryOf j) => Profunctor (Curry p :: (OPPOSITE j, k) -> i -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Cat

Methods

dimap :: forall (c :: (OPPOSITE j, k)) (a :: (OPPOSITE j, k)) (b :: i) (d :: i). (c ~> a) -> (b ~> d) -> Curry p a b -> Curry p c d Source Comments #

(\\) :: forall (a :: (OPPOSITE j, k)) (b :: i) r. ((Ob a, Ob b) => r) -> Curry p a b -> r Source Comments #

Monoidal k => Monoidal (OPPOSITE k) Source Comments #

The opposite of a monoidal category is also monoidal, with the same tensor product.

Instance details

Defined in Proarrow.Category.Opposite

Associated Types

type Unit
Instance details Defined in Proarrow.Category.Opposite type Unit = 'OP (Unit :: k)

Methods

withOb2 :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) r. (Ob a, Ob b) => (Ob (a ** b) => r) -> r Source Comments #

leftUnitor :: forall (a :: OPPOSITE k). Ob a => ((Unit :: OPPOSITE k) ** a) ~> a Source Comments #

leftUnitorInv :: forall (a :: OPPOSITE k). Ob a => a ~> ((Unit :: OPPOSITE k) ** a) Source Comments #

rightUnitor :: forall (a :: OPPOSITE k). Ob a => (a ** (Unit :: OPPOSITE k)) ~> a Source Comments #

rightUnitorInv :: forall (a :: OPPOSITE k). Ob a => a ~> (a ** (Unit :: OPPOSITE k)) Source Comments #

associator :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (c :: OPPOSITE k). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Comments #

associatorInv :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (c :: OPPOSITE k). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Comments #

SymMonoidal k => SymMonoidal (OPPOSITE k) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

Methods

swap :: forall (a :: OPPOSITE k) (b :: OPPOSITE k). (Ob a, Ob b) => (a ** b) ~> (b ** a) Source Comments #

CategoryOf k => CategoryOf (OPPOSITE k) Source Comments #

The opposite category of the category of k.

Instance details

Defined in Proarrow.Category.Opposite

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Opposite type (~>) = Op ((~>) :: CAT k)

HasBinaryProducts k => HasBinaryCoproducts (OPPOSITE k) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

Methods

withObCoprod :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) r. (Ob a, Ob b) => (Ob (a || b) => r) -> r Source Comments #

lft :: forall (a :: OPPOSITE k) (b :: OPPOSITE k). (Ob a, Ob b) => a ~> (a || b) Source Comments #

rgt :: forall (a :: OPPOSITE k) (b :: OPPOSITE k). (Ob a, Ob b) => b ~> (a || b) Source Comments #

(|||) :: forall (x :: OPPOSITE k) (a :: OPPOSITE k) (y :: OPPOSITE k). (x ~> a) -> (y ~> a) -> (x || y) ~> a Source Comments #

(+++) :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (x :: OPPOSITE k) (y :: OPPOSITE k). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) Source Comments #

HasBinaryCoproducts k => HasBinaryProducts (OPPOSITE k) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

Methods

withObProd :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) r. (Ob a, Ob b) => (Ob (a && b) => r) -> r Source Comments #

fst :: forall (a :: OPPOSITE k) (b :: OPPOSITE k). (Ob a, Ob b) => (a && b) ~> a Source Comments #

snd :: forall (a :: OPPOSITE k) (b :: OPPOSITE k). (Ob a, Ob b) => (a && b) ~> b Source Comments #

(&&&) :: forall (a :: OPPOSITE k) (x :: OPPOSITE k) (y :: OPPOSITE k). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments #

(***) :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (x :: OPPOSITE k) (y :: OPPOSITE k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments #

HasTerminalObject k => HasInitialObject (OPPOSITE k) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Opposite type InitialObject = 'OP (TerminalObject :: k)

Methods

initiate :: forall (a :: OPPOSITE k). Ob a => (InitialObject :: OPPOSITE k) ~> a Source Comments #

HasInitialObject k => HasTerminalObject (OPPOSITE k) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Opposite type TerminalObject = 'OP (InitialObject :: k)

Methods

terminate :: forall (a :: OPPOSITE k). Ob a => a ~> (TerminalObject :: OPPOSITE k) Source Comments #

FunctorForRep DualUnit Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Cat

Associated Types

type DualUnit @ ('OP '())
Instance details Defined in Proarrow.Category.Instance.Cat type DualUnit @ ('OP '()) = '()

Methods

fmap :: forall (a :: OPPOSITE ()) (b :: OPPOSITE ()). (a ~> b) -> (DualUnit @ a) ~> (DualUnit @ b) Source Comments #

Profunctor p => Functor (Op p a :: OPPOSITE k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

Methods

map :: forall (a0 :: OPPOSITE k) (b :: OPPOSITE k). (a0 ~> b) -> Op p a a0 ~> Op p a b Source Comments #

MonoidalAction m k => MonoidalAction (OPPOSITE m) (OPPOSITE k) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

Methods

withObAct :: forall (a :: OPPOSITE m) (x :: OPPOSITE k) r. (Ob a, Ob x) => (Ob (Act a x) => r) -> r Source Comments #

unitor :: forall (x :: OPPOSITE k). Ob x => Act (Unit :: OPPOSITE m) x ~> x Source Comments #

unitorInv :: forall (x :: OPPOSITE k). Ob x => x ~> Act (Unit :: OPPOSITE m) x Source Comments #

multiplicator :: forall (a :: OPPOSITE m) (b :: OPPOSITE m) (x :: OPPOSITE k). (Ob a, Ob b, Ob x) => Act a (Act b x) ~> Act (a ** b) x Source Comments #

multiplicatorInv :: forall (a :: OPPOSITE m) (b :: OPPOSITE m) (x :: OPPOSITE k). (Ob a, Ob b, Ob x) => Act (a ** b) x ~> Act a (Act b x) Source Comments #

EnrichedProfunctor v p => EnrichedProfunctor (Clone v) (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Comments #

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 Comments #

underlying :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). Op p a b -> (Unit :: Clone v) ~> ProObj (Clone v) (Op p) a b Source Comments #

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 Comments #

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 Comments #

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 Comments #

Strong k2 p => Strong (OPPOSITE k2) (Op p :: OPPOSITE j -> OPPOSITE k1 -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

Methods

act :: forall (a :: OPPOSITE k2) (b :: OPPOSITE k2) (x :: OPPOSITE j) (y :: OPPOSITE k1). (a ~> b) -> Op p x y -> Op p (Act a x) (Act b y) Source Comments #

ThinProfunctor p => ThinProfunctor (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

Methods

arr :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). (Ob a, Ob b, HasArrow (Op p) a b) => Op p a b Source Comments #

withArr :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) r. Op p a b -> (HasArrow (Op p) a b => r) -> r Source Comments #

MonoidalProfunctor p => MonoidalProfunctor (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

Methods

par0 :: Op p (Unit :: OPPOSITE j) (Unit :: OPPOSITE k) Source Comments #

par :: forall (x1 :: OPPOSITE j) (x2 :: OPPOSITE k) (y1 :: OPPOSITE j) (y2 :: OPPOSITE k). Op p x1 x2 -> Op p y1 y2 -> Op p (x1 ** y1) (x2 ** y2) Source Comments #

Profunctor p => Profunctor (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

Methods

dimap :: forall (c :: OPPOSITE j) (a :: OPPOSITE j) (b :: OPPOSITE k) (d :: OPPOSITE k). (c ~> a) -> (b ~> d) -> Op p a b -> Op p c d Source Comments #

(\\) :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) r. ((Ob a, Ob b) => r) -> Op p a b -> r Source Comments #

Representable p => Corepresentable (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

Methods

coindex :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). Op p a b -> (Op p %% a) ~> b Source Comments #

cotabulate :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). Ob a => ((Op p %% a) ~> b) -> Op p a b Source Comments #

corepMap :: forall (a :: OPPOSITE j) (b :: OPPOSITE j). (a ~> b) -> (Op p %% a) ~> (Op p %% b) Source Comments #

Corepresentable p => Representable (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

Methods

index :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). Op p a b -> a ~> (Op p % b) Source Comments #

tabulate :: forall (b :: OPPOSITE k) (a :: OPPOSITE j). Ob b => (a ~> (Op p % b)) -> Op p a b Source Comments #

repMap :: forall (a :: OPPOSITE k) (b :: OPPOSITE k). (a ~> b) -> (Op p % a) ~> (Op p % b) Source Comments #

Proadjunction q p => Proadjunction (Op p :: OPPOSITE k -> OPPOSITE j -> Type) (Op q :: OPPOSITE j -> OPPOSITE k -> Type) Source Comments #

Instance details

Defined in Proarrow.Adjunction

Methods

unit :: forall (a :: OPPOSITE j). Ob a => (Op q :.: Op p) a a Source Comments #

counit :: (Op p :.: Op q) :~> ((~>) :: CAT (OPPOSITE k)) Source Comments #

Monoid c => Comonoid ('OP c :: OPPOSITE k) Source Comments #

Instance details

Defined in Proarrow.Monoid

Methods

counit :: 'OP c ~> (Unit :: OPPOSITE k) Source Comments #

comult :: 'OP c ~> ('OP c ** 'OP c) Source Comments #

Comonoid c => Monoid ('OP c :: OPPOSITE k) Source Comments #

Instance details

Defined in Proarrow.Monoid

Methods

mempty :: (Unit :: OPPOSITE k) ~> 'OP c Source Comments #

mappend :: ('OP c ** 'OP c) ~> 'OP c Source Comments #

MonoidalAction m k => Functor (Reader :: OPPOSITE m -> k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Promonad.Reader

Methods

map :: forall (a :: OPPOSITE m) (b :: OPPOSITE m). (a ~> b) -> (Reader a :: k -> k -> Type) ~> (Reader b :: k -> k -> Type) Source Comments #

(CategoryOf j, CategoryOf k) => FunctorForRep (DistribDual :: OPPOSITE (j, k) +-> (OPPOSITE j, OPPOSITE k)) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Cat

Methods

fmap :: forall (a :: OPPOSITE (j, k)) (b :: OPPOSITE (j, k)). (a ~> b) -> ((DistribDual :: OPPOSITE (j, k) +-> (OPPOSITE j, OPPOSITE k)) @ a) ~> ((DistribDual :: OPPOSITE (j, k) +-> (OPPOSITE j, OPPOSITE k)) @ b) Source Comments #

Functor (Ran :: OPPOSITE (i +-> j) -> (i +-> k) -> k -> j -> Type) Source Comments #

Instance details

Defined in Proarrow.Profunctor.Ran

Methods

map :: forall (a :: OPPOSITE (i +-> j)) (b :: OPPOSITE (i +-> j)). (a ~> b) -> (Ran a :: (i +-> k) -> k -> j -> Type) ~> (Ran b :: (i +-> k) -> k -> j -> Type) Source Comments #

Functor (Rift :: OPPOSITE (k +-> i) -> (j +-> i) -> k -> j -> Type) Source Comments #

Instance details

Defined in Proarrow.Profunctor.Rift

Methods

map :: forall (a :: OPPOSITE (k +-> i)) (b :: OPPOSITE (k +-> i)). (a ~> b) -> (Rift a :: (j +-> i) -> k -> j -> Type) ~> (Rift b :: (j +-> i) -> k -> j -> Type) Source Comments #

(CategoryOf j, CategoryOf k) => Functor (Yo a :: OPPOSITE j -> k -> j -> Type) Source Comments #

Instance details

Defined in Proarrow.Profunctor.Yoneda

Methods

map :: forall (a0 :: OPPOSITE j) (b :: OPPOSITE j). (a0 ~> b) -> Yo a a0 ~> Yo a b Source Comments #

Promonad c => Promonad (Op c :: OPPOSITE j -> OPPOSITE j -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

Methods

id :: forall (a :: OPPOSITE j). Ob a => Op c a a Source Comments #

(.) :: forall (b :: OPPOSITE j) (c0 :: OPPOSITE j) (a :: OPPOSITE j). Op c b c0 -> Op c a b -> Op c a c0 Source Comments #

CategoryOf k => Profunctor (Hom :: () -> (OPPOSITE k, k) -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Limit

Methods

dimap :: forall (c :: ()) (a :: ()) (b :: (OPPOSITE k, k)) (d :: (OPPOSITE k, k)). (c ~> a) -> (b ~> d) -> Hom a b -> Hom c d Source Comments #

(\\) :: forall (a :: ()) (b :: (OPPOSITE k, k)) r. ((Ob a, Ob b) => r) -> Hom a b -> r Source Comments #

CategoryOf k => HasColimits (Hom :: (OPPOSITE k, k) -> () -> Type) Type Source Comments #

Instance details

Defined in Proarrow.Category.Colimit

Methods

colimit :: forall (d :: Type +-> (OPPOSITE k, k)). Corepresentable d => ((Hom :: (OPPOSITE k, k) -> () -> Type) :.: Colimit (Hom :: (OPPOSITE k, k) -> () -> Type) d) :~> d Source Comments #

colimitUniv :: forall (d :: Type +-> (OPPOSITE k, k)) (p :: Type +-> ()). (Corepresentable d, Profunctor p) => (((Hom :: (OPPOSITE k, k) -> () -> Type) :.: p) :~> d) -> p :~> Colimit (Hom :: (OPPOSITE k, k) -> () -> Type) d Source Comments #

(CategoryOf j, CategoryOf k) => FunctorForRep (CombineDual :: (OPPOSITE j, OPPOSITE k) +-> OPPOSITE (j, k)) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Cat

Methods

fmap :: forall (a :: (OPPOSITE j, OPPOSITE k)) (b :: (OPPOSITE j, OPPOSITE k)). (a ~> b) -> ((CombineDual :: (OPPOSITE j, OPPOSITE k) +-> OPPOSITE (j, k)) @ a) ~> ((CombineDual :: (OPPOSITE j, OPPOSITE k) +-> OPPOSITE (j, k)) @ b) Source Comments #

Profunctor j => Profunctor (LimitAdj j :: COREPK b k -> REPK a k -> Type) Source Comments #

Instance details

Defined in Proarrow.Adjunction

Methods

dimap :: forall (c :: COREPK b k) (a0 :: COREPK b k) (b0 :: REPK a k) (d :: REPK a k). (c ~> a0) -> (b0 ~> d) -> LimitAdj j a0 b0 -> LimitAdj j c d Source Comments #

(\\) :: forall (a0 :: COREPK b k) (b0 :: REPK a k) r. ((Ob a0, Ob b0) => r) -> LimitAdj j a0 b0 -> r Source Comments #

HasColimits j k => Corepresentable (LimitAdj j :: COREPK b k -> REPK a k -> Type) Source Comments #

Instance details

Defined in Proarrow.Adjunction

Methods

coindex :: forall (a0 :: COREPK b k) (b0 :: REPK a k). LimitAdj j a0 b0 -> ((LimitAdj j :: COREPK b k -> REPK a k -> Type) %% a0) ~> b0 Source Comments #

cotabulate :: forall (a0 :: COREPK b k) (b0 :: REPK a k). Ob a0 => (((LimitAdj j :: COREPK b k -> REPK a k -> Type) %% a0) ~> b0) -> LimitAdj j a0 b0 Source Comments #

corepMap :: forall (a0 :: COREPK b k) (b0 :: COREPK b k). (a0 ~> b0) -> ((LimitAdj j :: COREPK b k -> REPK a k -> Type) %% a0) ~> ((LimitAdj j :: COREPK b k -> REPK a k -> Type) %% b0) Source Comments #

HasLimits j k => Representable (LimitAdj j :: COREPK b k -> REPK a k -> Type) Source Comments #

Colimit j -| Limit j

Instance details

Defined in Proarrow.Adjunction

Methods

index :: forall (a0 :: COREPK b k) (b0 :: REPK a k). LimitAdj j a0 b0 -> a0 ~> ((LimitAdj j :: COREPK b k -> REPK a k -> Type) % b0) Source Comments #

tabulate :: forall (b0 :: REPK a k) (a0 :: COREPK b k). Ob b0 => (a0 ~> ((LimitAdj j :: COREPK b k -> REPK a k -> Type) % b0)) -> LimitAdj j a0 b0 Source Comments #

repMap :: forall (a0 :: REPK a k) (b0 :: REPK a k). (a0 ~> b0) -> ((LimitAdj j :: COREPK b k -> REPK a k -> Type) % a0) ~> ((LimitAdj j :: COREPK b k -> REPK a k -> Type) % b0) Source Comments #

type (n :: v) *. ('OP a :: OPPOSITE k) Source Comments #

Instance details

Defined in Proarrow.Object.Copower

type (n :: v) *. ('OP a :: OPPOSITE k) = 'OP (a ^ n)

type UN ('OP :: j -> OPPOSITE j) ('OP k :: OPPOSITE j) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

type UN ('OP :: j -> OPPOSITE j) ('OP k :: OPPOSITE j) = k

type Colimit (Hom :: (OPPOSITE k, k) -> () -> Type) (d :: Type +-> (OPPOSITE k, k)) Source Comments #

Instance details

Defined in Proarrow.Category.Colimit

type Colimit (Hom :: (OPPOSITE k, k) -> () -> Type) (d :: Type +-> (OPPOSITE k, k)) = CoendLimit d

type Unit Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

type Unit = 'OP (Unit :: k)

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

type (~>) = Op ((~>) :: CAT k)

type InitialObject Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

type InitialObject = 'OP (TerminalObject :: k)

type TerminalObject Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

type TerminalObject = 'OP (InitialObject :: k)

type Ob (a :: OPPOSITE k) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

type Ob (a :: OPPOSITE k) = (Is ('OP :: k -> OPPOSITE k) a, Ob (UN ('OP :: k -> OPPOSITE k) a))

type (a :: OPPOSITE k) ** (b :: OPPOSITE k) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

type (a :: OPPOSITE k) ** (b :: OPPOSITE k) = 'OP (UN ('OP :: k -> OPPOSITE k) a ** UN ('OP :: k -> OPPOSITE k) b)

type (a :: OPPOSITE k) || (b :: OPPOSITE k) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

type (a :: OPPOSITE k) || (b :: OPPOSITE k) = 'OP (UN ('OP :: k -> OPPOSITE k) a && UN ('OP :: k -> OPPOSITE k) b)

type (a :: OPPOSITE k) && (b :: OPPOSITE k) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

type (a :: OPPOSITE k) && (b :: OPPOSITE k) = 'OP (UN ('OP :: k -> OPPOSITE k) a || UN ('OP :: k -> OPPOSITE k) b)

type DualUnit @ ('OP '()) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Cat

type DualUnit @ ('OP '()) = '()

type ('OP a :: OPPOSITE k) ^ (n :: v) Source Comments #

Instance details

Defined in Proarrow.Object.Copower

type ('OP a :: OPPOSITE k) ^ (n :: v) = 'OP (n *. a)

type ProObj (Clone v) (Op p :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE j) ('OP b :: OPPOSITE k) Source Comments #

Instance details

Defined in Proarrow.Category.Enriched

type ProObj (Clone v) (Op p :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE j) ('OP b :: OPPOSITE k) = 'SUB (ProObj v p b a) :: SUBCAT (Any :: v -> Constraint)

type Act ('OP a :: OPPOSITE m) ('OP b :: OPPOSITE k) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

type Act ('OP a :: OPPOSITE m) ('OP b :: OPPOSITE k) = 'OP (Act a b)

type (Op p :: OPPOSITE j -> OPPOSITE k -> Type) %% ('OP a :: OPPOSITE j) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

type (Op p :: OPPOSITE j -> OPPOSITE k -> Type) %% ('OP a :: OPPOSITE j) = 'OP (p % a)

type (Op p :: OPPOSITE j -> OPPOSITE k -> Type) % ('OP a :: OPPOSITE k) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

type (Op p :: OPPOSITE j -> OPPOSITE k -> Type) % ('OP a :: OPPOSITE k) = 'OP (p %% a)

type HasArrow (Op p :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE j) ('OP b :: OPPOSITE k) Source Comments #

Instance details

Defined in Proarrow.Category.Opposite

type HasArrow (Op p :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE j) ('OP b :: OPPOSITE k) = HasArrow p b a

type (DistribDual :: OPPOSITE (j, k) +-> (OPPOSITE j, OPPOSITE k)) @ ('OP '(a, b) :: OPPOSITE (j, k)) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Cat

type (DistribDual :: OPPOSITE (j, k) +-> (OPPOSITE j, OPPOSITE k)) @ ('OP '(a, b) :: OPPOSITE (j, k)) = '('OP a, 'OP b)

type Limit (Hom :: () -> (OPPOSITE k, k) -> Type) (d :: (OPPOSITE k, k) +-> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Limit

type Limit (Hom :: () -> (OPPOSITE k, k) -> Type) (d :: (OPPOSITE k, k) +-> Type) = Rep (EndLimit d)

type (CombineDual :: (OPPOSITE j, OPPOSITE k) +-> OPPOSITE (j, k)) @ ('('OP a, 'OP b) :: (OPPOSITE j, OPPOSITE k)) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Cat

type (CombineDual :: (OPPOSITE j, OPPOSITE k) +-> OPPOSITE (j, k)) @ ('('OP a, 'OP b) :: (OPPOSITE j, OPPOSITE k)) = 'OP '(a, b)

type (LimitAdj j :: COREPK b k -> REPK a k -> Type) %% (c :: COREPK b k) Source Comments #

Instance details

Defined in Proarrow.Adjunction

type (LimitAdj j :: COREPK b k -> REPK a k -> Type) %% (c :: COREPK b k) = REP (CorepStar (Colimit j (UN ('OP :: (k +-> b) -> OPPOSITE (k +-> b)) (UN ('SUB :: OPPOSITE (k +-> b) -> SUBCAT (OpCorepresentable :: OPPOSITE (k +-> b) -> Constraint)) c))))

type (LimitAdj j :: COREPK b k -> REPK a k -> Type) % (r :: REPK a k) Source Comments #

Instance details

Defined in Proarrow.Adjunction

type (LimitAdj j :: COREPK b k -> REPK a k -> Type) % (r :: REPK a k) = COREP (RepCostar (Limit j (UN ('SUB :: (a +-> k) -> SUBCAT (Representable :: (a +-> k) -> Constraint)) r)))

data Op (p :: j +-> k) (a :: OPPOSITE j) (b :: OPPOSITE k) where Source Comments #

Constructors

Op
Fields :: forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j). { unOp :: p b1 a1 } -> Op p ('OP a1) ('OP b1)

Instances

Instances details

Profunctor p => Functor (Op p a :: OPPOSITE k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Opposite Methods map :: forall (a0 :: OPPOSITE k) (b :: OPPOSITE k). (a0 ~> b) -> Op p a a0 ~> Op p a b Source Comments #
EnrichedProfunctor v p => EnrichedProfunctor (Clone v) (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Comments #
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 Comments # underlying :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). Op p a b -> (Unit :: Clone v) ~> ProObj (Clone v) (Op p) a b Source Comments # 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 Comments # 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 Comments # 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 Comments #
Strong k2 p => Strong (OPPOSITE k2) (Op p :: OPPOSITE j -> OPPOSITE k1 -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Opposite Methods act :: forall (a :: OPPOSITE k2) (b :: OPPOSITE k2) (x :: OPPOSITE j) (y :: OPPOSITE k1). (a ~> b) -> Op p x y -> Op p (Act a x) (Act b y) Source Comments #
ThinProfunctor p => ThinProfunctor (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Opposite Methods arr :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). (Ob a, Ob b, HasArrow (Op p) a b) => Op p a b Source Comments # withArr :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) r. Op p a b -> (HasArrow (Op p) a b => r) -> r Source Comments #
MonoidalProfunctor p => MonoidalProfunctor (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Opposite Methods par0 :: Op p (Unit :: OPPOSITE j) (Unit :: OPPOSITE k) Source Comments # par :: forall (x1 :: OPPOSITE j) (x2 :: OPPOSITE k) (y1 :: OPPOSITE j) (y2 :: OPPOSITE k). Op p x1 x2 -> Op p y1 y2 -> Op p (x1 y1) (x2 y2) Source Comments #
Profunctor p => Profunctor (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Opposite Methods dimap :: forall (c :: OPPOSITE j) (a :: OPPOSITE j) (b :: OPPOSITE k) (d :: OPPOSITE k). (c ~> a) -> (b ~> d) -> Op p a b -> Op p c d Source Comments # (\\) :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) r. ((Ob a, Ob b) => r) -> Op p a b -> r Source Comments #
Representable p => Corepresentable (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Opposite Methods coindex :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). Op p a b -> (Op p %% a) ~> b Source Comments # cotabulate :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). Ob a => ((Op p %% a) ~> b) -> Op p a b Source Comments # corepMap :: forall (a :: OPPOSITE j) (b :: OPPOSITE j). (a ~> b) -> (Op p %% a) ~> (Op p %% b) Source Comments #
Corepresentable p => Representable (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Opposite Methods index :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). Op p a b -> a ~> (Op p % b) Source Comments # tabulate :: forall (b :: OPPOSITE k) (a :: OPPOSITE j). Ob b => (a ~> (Op p % b)) -> Op p a b Source Comments # repMap :: forall (a :: OPPOSITE k) (b :: OPPOSITE k). (a ~> b) -> (Op p % a) ~> (Op p % b) Source Comments #
Proadjunction q p => Proadjunction (Op p :: OPPOSITE k -> OPPOSITE j -> Type) (Op q :: OPPOSITE j -> OPPOSITE k -> Type) Source Comments #
Instance details Defined in Proarrow.Adjunction Methods unit :: forall (a :: OPPOSITE j). Ob a => (Op q :.: Op p) a a Source Comments # counit :: (Op p :.: Op q) :~> ((~>) :: CAT (OPPOSITE k)) Source Comments #
Promonad c => Promonad (Op c :: OPPOSITE j -> OPPOSITE j -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Opposite Methods id :: forall (a :: OPPOSITE j). Ob a => Op c a a Source Comments # (.) :: forall (b :: OPPOSITE j) (c0 :: OPPOSITE j) (a :: OPPOSITE j). Op c b c0 -> Op c a b -> Op c a c0 Source Comments #
type ProObj (Clone v) (Op p :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE j) ('OP b :: OPPOSITE k) Source Comments #
Instance details Defined in Proarrow.Category.Enriched type ProObj (Clone v) (Op p :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE j) ('OP b :: OPPOSITE k) = 'SUB (ProObj v p b a) :: SUBCAT (Any :: v -> Constraint)
type (Op p :: OPPOSITE j -> OPPOSITE k -> Type) %% ('OP a :: OPPOSITE j) Source Comments #
Instance details Defined in Proarrow.Category.Opposite type (Op p :: OPPOSITE j -> OPPOSITE k -> Type) %% ('OP a :: OPPOSITE j) = 'OP (p % a)
type (Op p :: OPPOSITE j -> OPPOSITE k -> Type) % ('OP a :: OPPOSITE k) Source Comments #
Instance details Defined in Proarrow.Category.Opposite type (Op p :: OPPOSITE j -> OPPOSITE k -> Type) % ('OP a :: OPPOSITE k) = 'OP (p %% a)
type HasArrow (Op p :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE j) ('OP b :: OPPOSITE k) Source Comments #
Instance details Defined in Proarrow.Category.Opposite type HasArrow (Op p :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE j) ('OP b :: OPPOSITE k) = HasArrow p b a

data UnOp (p :: OPPOSITE k +-> OPPOSITE j) (a :: k) (b :: j) where Source Comments #

Constructors

UnOp
Fields :: forall {k} {j} (p :: OPPOSITE k +-> OPPOSITE j) (b :: j) (a :: k). { unUnOp :: p ('OP b) ('OP a) } -> UnOp p a b

Instances

Instances details

(CategoryOf j, CategoryOf k, Profunctor p) => Profunctor (UnOp p :: k -> j -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Opposite Methods dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> UnOp p a b -> UnOp p c d Source Comments # (\\) :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> UnOp p a b -> r Source Comments #