proarrow
Safe HaskellNone
LanguageGHC2024

Proarrow.Category.Instance.Opposite

Description

The opposite category: the kind OPPOSITE k wraps k in OP, and an arrow OP a ~> OP b is an arrow b ~> a of k. Op (and its inverse UnOp) also flips profunctors, swapping their two arguments. This is the prototypical use of a newtype wrapper on a kind to give one collection of types a second category structure.

Synopsis

Documentation

data OPPOSITE k Source Github #

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 Github # 
Instance details

Defined in Proarrow.Colimit.Copower

Methods

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

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

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

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

Defined in Proarrow.Colimit.Copower

Methods

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

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

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

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

Defined in Proarrow.Profunctor.Instance.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 Github #

Enumerable k => Enumerable (OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

Methods

withIndex :: forall (a :: OPPOSITE k) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: OPPOSITE k) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb (OPPOSITE k) (At (OPPOSITE k) i) Source Github #

Finite k => Finite (OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

Associated Types

type Objects (OPPOSITE k) 
Instance details

Defined in Proarrow.Category.Instance.Opposite

type Objects (OPPOSITE k) = MapWrap ('OP :: k -> OPPOSITE k) (Objects k)

Methods

finite :: IndexedList (Objects (OPPOSITE k)) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects (OPPOSITE k)) i ~ At (OPPOSITE k) i => r) -> r Source Github #

Indexed k => Indexed (OPPOSITE k) Source Github #

The opposite category has the same objects, numbered the same way.

Instance details

Defined in Proarrow.Category.Instance.Opposite

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

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

Instance details

Defined in Proarrow.Category.Monoidal

Associated Types

type Unit 
Instance details

Defined in Proarrow.Category.Monoidal

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

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

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

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

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

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

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

SymMonoidal k => SymMonoidal (OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal

Methods

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

HasBinaryProducts k => HasBinaryCoproducts (OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

Methods

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

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

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

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

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

HasEqualizers k => HasCoequalizers (OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Colimit.Coequalizer

Methods

coequalize :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) r. (a ~> b) -> (a ~> b) -> (forall (c :: OPPOSITE k). (b ~> c) -> r) -> r Source Github #

factorCoequalizer :: forall (c :: OPPOSITE k) (x :: OPPOSITE k) (c' :: OPPOSITE k). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #

HasTerminalObject k => HasInitialObject (OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Colimit.Initial

Associated Types

type InitialObject 
Instance details

Defined in Proarrow.Colimit.Initial

type InitialObject = 'OP (TerminalObject :: k)

Methods

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

HasPullbacks k => HasPushouts (OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Colimit.Pushout

Methods

pushout :: forall (o :: OPPOSITE k) (a :: OPPOSITE k) (b :: OPPOSITE k) r. (o ~> a) -> (o ~> b) -> (forall (p :: OPPOSITE k). (a ~> p) -> (b ~> p) -> r) -> r Source Github #

factorPushout :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (p :: OPPOSITE k) (q :: OPPOSITE k). (a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q Source Github #

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

The opposite category of the category of k.

Instance details

Defined in Proarrow.Category.Instance.Opposite

Associated Types

type (~>) 
Instance details

Defined in Proarrow.Category.Instance.Opposite

type (~>) = Op ((~>) :: CAT k)
HasBinaryCoproducts k => HasBinaryProducts (OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

Methods

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

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

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

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

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

HasCoequalizers k => HasEqualizers (OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Colimit.Coequalizer

Methods

equalize :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) r. (a ~> b) -> (a ~> b) -> (forall (e :: OPPOSITE k). (e ~> a) -> r) -> r Source Github #

factorEqualizer :: forall (e :: OPPOSITE k) (x :: OPPOSITE k) (e' :: OPPOSITE k). (e ~> x) -> (e' ~> x) -> e' ~> e Source Github #

HasPushouts k => HasPullbacks (OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Colimit.Pushout

Methods

pullback :: forall (o :: OPPOSITE k) (a :: OPPOSITE k) (b :: OPPOSITE k) r. (a ~> o) -> (b ~> o) -> (forall (p :: OPPOSITE k). (p ~> a) -> (p ~> b) -> r) -> r Source Github #

factorPullback :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (p :: OPPOSITE k) (q :: OPPOSITE k). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p Source Github #

HasInitialObject k => HasTerminalObject (OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Colimit.Initial

Associated Types

type TerminalObject 
Instance details

Defined in Proarrow.Colimit.Initial

type TerminalObject = 'OP (InitialObject :: k)

Methods

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

FunctorForRep (Pick a :: OPPOSITE Nat +-> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Simplex

Methods

fmap :: forall (a0 :: OPPOSITE Nat) (b :: OPPOSITE Nat). (a0 ~> b) -> (Pick a @ a0) ~> (Pick a @ b) Source Github #

(Closed k, Ob r) => FunctorForRep (Not r :: OPPOSITE k +-> k) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Closed

Methods

fmap :: forall (a :: OPPOSITE k) (b :: OPPOSITE k). (a ~> b) -> (Not r @ a) ~> (Not r @ b) Source Github #

(Closed k, SymMonoidal k, Ob r) => Corepresentable (Rep (Not r) :: k -> OPPOSITE k -> Type) Source Github #

The Op-Op adjunction, giving rise to the continuation monad.

Instance details

Defined in Proarrow.Category.Monoidal.Closed

Methods

coindex :: forall (a :: k) (b :: OPPOSITE k). Rep (Not r) a b -> (Rep (Not r) %% a) ~> b Source Github #

cotabulate :: forall (a :: k) (b :: OPPOSITE k). Ob a => ((Rep (Not r) %% a) ~> b) -> Rep (Not r) a b Source Github #

corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (Rep (Not r) %% a) ~> (Rep (Not r) %% b) Source Github #

corepUniv :: forall (a :: k). Ob a => Rep (Not r) a (Rep (Not r) %% a) Source Github #

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

Defined in Proarrow.Category.Instance.Opposite

Methods

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

(Prostrong w p, CategoryOf j, CategoryOf k) => Prostrong (w :: FLAVOR (OPPOSITE k) (OPPOSITE j)) (Op (UnOp p) :: OPPOSITE j -> OPPOSITE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Optic

Methods

proact :: forall (f :: OPPOSITE j +-> OPPOSITE j) (g :: OPPOSITE k +-> OPPOSITE k). (w f g, Profunctor f, Profunctor g) => ((f :.: Op (UnOp p)) :.: g) :~> Op (UnOp p) 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 #

TermUniversal b l => InitUniversal ('OP b :: OPPOSITE j) (Op l :: OPPOSITE j -> OPPOSITE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Universal

Associated Types

type InitUnivTgt (Op l :: OPPOSITE j -> OPPOSITE k -> Type) ('OP b :: OPPOSITE j) 
Instance details

Defined in Proarrow.Universal

type InitUnivTgt (Op l :: OPPOSITE j -> OPPOSITE k -> Type) ('OP b :: OPPOSITE j) = 'OP (TermUnivSrc l b)

Methods

initUnivArr :: Op l ('OP b) (InitUnivTgt (Op l) ('OP b)) Source Github #

initUnivProp :: forall (b0 :: OPPOSITE k). Op l ('OP b) b0 -> InitUnivTgt (Op l) ('OP b) ~> b0 Source Github #

InitUniversal a r => TermUniversal ('OP a :: OPPOSITE k) (Op r :: OPPOSITE j -> OPPOSITE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Universal

Associated Types

type TermUnivSrc (Op r :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE k) 
Instance details

Defined in Proarrow.Universal

type TermUnivSrc (Op r :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE k) = 'OP (InitUnivTgt r a)

Methods

termUnivArr :: Op r (TermUnivSrc (Op r) ('OP a)) ('OP a) Source Github #

termUnivProp :: forall (a0 :: OPPOSITE j). Op r a0 ('OP a) -> a0 ~> TermUnivSrc (Op r) ('OP a) Source Github #

Finitary p => Finitary (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Github #

The opposite of a finitary profunctor is finitary, at the same sizes read the other way round. Taking p = Hom k this makes OPPOSITE k a FiniteCat whenever k is one, so everything computed for a finite site is available on the opposite category too. (This instance lives here rather than with Op because Proarrow.Category.Instance.Opposite sits below this module in the import graph.)

Instance details

Defined in Proarrow.Category.Enriched.Finitary

Methods

size :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). (Ob a, Ob b) => Natural Source Github #

toIndex :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). (Ob a, Ob b) => Op p a b -> Natural Source Github #

fromIndex :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). (Ob a, Ob b) => Natural -> Op p a b Source Github #

elements :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). (Ob a, Ob b) => [Op p a b] Source Github #

DecidableProfunctor p => DecidableProfunctor (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

Methods

decide :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). (Ob a, Ob b) => Decision (Op p) a b (Holds (Op p) a b) Source Github #

toHolds :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) r. Op p a b -> ((Holds (Op p) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

ThinProfunctor p => ThinProfunctor (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

Methods

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

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

MonoidalProfunctor p => MonoidalProfunctor (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal

Methods

one :: Op p (Unit :: OPPOSITE j) (Unit :: OPPOSITE k) Source Github #

(**) :: 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 Github #

MonoidalAction t => MonoidalAction (Rep (OpAction t) :: OPPOSITE k -> (OPPOSITE m, OPPOSITE k) -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Action

Methods

unitor :: forall (x :: OPPOSITE k). Ob x => Act (Rep (OpAction t)) (Unit :: OPPOSITE m) x ~> x Source Github #

unitorInv :: forall (x :: OPPOSITE k). Ob x => x ~> Act (Rep (OpAction t)) (Unit :: OPPOSITE m) x Source Github #

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

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

Profunctor p => Profunctor (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.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 Github #

lmap :: forall (c :: OPPOSITE j) (a :: OPPOSITE j) (b :: OPPOSITE k). (c ~> a) -> Op p a b -> Op p c b Source Github #

rmap :: forall (b :: OPPOSITE k) (d :: OPPOSITE k) (a :: OPPOSITE j). (b ~> d) -> Op p a b -> Op p a d Source Github #

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

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

Defined in Proarrow.Profunctor.Representable

Methods

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

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

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

corepUniv :: forall (a :: OPPOSITE j). Ob a => Op p a (Op p %% a) Source Github #

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

Defined in Proarrow.Profunctor.Representable

Methods

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

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

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

repUniv :: forall (a :: OPPOSITE k). Ob a => Op p (Op p % a) a Source Github #

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

Defined in Proarrow.Adjunction

Methods

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

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

CommutativeMonoid c => CocommutativeComonoid ('OP c :: OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Monoid

CocommutativeComonoid c => CommutativeMonoid ('OP c :: OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Monoid

Monoid c => Comonoid ('OP c :: OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Monoid

Methods

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

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

Comonoid c => Monoid ('OP c :: OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Monoid

Methods

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

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

Monoidal k => Functor (Reader :: OPPOSITE k -> k -> k -> Type) Source Github # 
Instance details

Defined in Proarrow.Promonad.Reader

Methods

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

Monoidal k => Functor (ReaderT :: OPPOSITE k -> (k +-> k) -> k -> k -> Type) Source Github # 
Instance details

Defined in Proarrow.Promonad.Reader

Methods

map :: forall (a :: OPPOSITE k) (b :: OPPOSITE k). (a ~> b) -> ReaderT a ~> ReaderT b Source Github #

Functor (Costar' :: OPPOSITE (j .-> k) -> j -> k -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Costar

Methods

map :: forall (a :: OPPOSITE (j .-> k)) (b :: OPPOSITE (j .-> k)). (a ~> b) -> Costar' a ~> Costar' b Source Github #

Functor (Ran :: OPPOSITE (i +-> j) -> (i +-> k) -> k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.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 Github #

Functor (Rift :: OPPOSITE (k +-> i) -> (j +-> i) -> k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.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 Github #

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

Defined in Proarrow.Profunctor.Instance.Yoneda

Methods

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

Promonad c => Promonad (Op c :: OPPOSITE j -> OPPOSITE j -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

Methods

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

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

Closed k => FunctorForRep (ExpRep :: (OPPOSITE k, k) +-> k) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Closed

Methods

fmap :: forall (a :: (OPPOSITE k, k)) (b :: (OPPOSITE k, k)). (a ~> b) -> ((ExpRep :: (OPPOSITE k, k) +-> k) @ a) ~> ((ExpRep :: (OPPOSITE k, k) +-> k) @ b) Source Github #

(Representable t, CategoryOf m) => FunctorForRep (OpAction t :: (OPPOSITE m, OPPOSITE k) +-> OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Action

Methods

fmap :: forall (a :: (OPPOSITE m, OPPOSITE k)) (b :: (OPPOSITE m, OPPOSITE k)). (a ~> b) -> (OpAction t @ a) ~> (OpAction t @ b) Source Github #

Functor (Op :: (j +-> k) -> OPPOSITE j -> OPPOSITE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

Methods

map :: forall (a :: j +-> k) (b :: j +-> k). (a ~> b) -> Op a ~> Op b Source Github #

Profunctor j => Profunctor (LimitAdj j :: COREPK b k -> REPK a k -> Type) Source Github # 
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 Github #

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

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

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

HasColimits j k => Corepresentable (LimitAdj j :: COREPK b k -> REPK a k -> Type) Source Github # 
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 Github #

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

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

corepUniv :: forall (a0 :: COREPK b k). Ob a0 => LimitAdj j a0 ((LimitAdj j :: COREPK b k -> REPK a k -> Type) %% a0) Source Github #

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

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

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

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

repUniv :: forall (a0 :: REPK a k). Ob a0 => LimitAdj j ((LimitAdj j :: COREPK b k -> REPK a k -> Type) % a0) a0 Source Github #

type (n :: v) *. ('OP a :: OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Colimit.Copower

type (n :: v) *. ('OP a :: OPPOSITE k) = 'OP (a ^ n)
type (Rep (Not r) :: k -> OPPOSITE k -> Type) %% (a :: k) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Closed

type (Rep (Not r) :: k -> OPPOSITE k -> Type) %% (a :: k) = 'OP (a ~~> r)
type Objects (OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

type Objects (OPPOSITE k) = MapWrap ('OP :: k -> OPPOSITE k) (Objects k)
type Unit Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal

type Unit = 'OP (Unit :: k)
type InitialObject Source Github # 
Instance details

Defined in Proarrow.Colimit.Initial

type InitialObject = 'OP (TerminalObject :: k)
type (~>) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

type (~>) = Op ((~>) :: CAT k)
type TerminalObject Source Github # 
Instance details

Defined in Proarrow.Colimit.Initial

type TerminalObject = 'OP (InitialObject :: k)
type At (OPPOSITE k) i Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

type At (OPPOSITE k) i = FmapWrap ('OP :: k -> OPPOSITE k) (At k i)
type Index (a :: OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

type Index (a :: OPPOSITE k) = Index (UN ('OP :: k -> OPPOSITE k) a)
type Ob (a :: OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

type Ob (a :: OPPOSITE k) = WrappedOb ('OP :: k -> OPPOSITE k) a
type (a :: OPPOSITE k) ** (b :: OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal

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 Github # 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

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 Github # 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

type (a :: OPPOSITE k) && (b :: OPPOSITE k) = 'OP (UN ('OP :: k -> OPPOSITE k) a || UN ('OP :: k -> OPPOSITE k) b)
type (Pick a :: OPPOSITE Nat +-> Type) @ ('OP n :: OPPOSITE Nat) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Simplex

type (Pick a :: OPPOSITE Nat +-> Type) @ ('OP n :: OPPOSITE Nat) = Vec n a
type ('OP a :: OPPOSITE k) ^ (n :: v) Source Github # 
Instance details

Defined in Proarrow.Colimit.Copower

type ('OP a :: OPPOSITE k) ^ (n :: v) = 'OP (n *. a)
type (Not r :: OPPOSITE k +-> k) @ ('OP a :: OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Closed

type (Not r :: OPPOSITE k +-> k) @ ('OP a :: OPPOSITE k) = a ~~> r
type ProObj (Clone v) (Op p :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE j) ('OP b :: OPPOSITE k) Source Github # 
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 Github # 
Instance details

Defined in Proarrow.Profunctor.Representable

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 Github # 
Instance details

Defined in Proarrow.Profunctor.Representable

type (Op p :: OPPOSITE j -> OPPOSITE k -> Type) % ('OP a :: OPPOSITE k) = 'OP (p %% a)
type InitUnivTgt (Op l :: OPPOSITE j -> OPPOSITE k -> Type) ('OP b :: OPPOSITE j) Source Github # 
Instance details

Defined in Proarrow.Universal

type InitUnivTgt (Op l :: OPPOSITE j -> OPPOSITE k -> Type) ('OP b :: OPPOSITE j) = 'OP (TermUnivSrc l b)
type TermUnivSrc (Op r :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Universal

type TermUnivSrc (Op r :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE k) = 'OP (InitUnivTgt r a)
type HasArrow (Op p :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE j) ('OP b :: OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

type HasArrow (Op p :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE j) ('OP b :: OPPOSITE k) = HasArrow p b a
type Holds (Op p :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE j) ('OP b :: OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

type Holds (Op p :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE j) ('OP b :: OPPOSITE k) = Holds p b a
type (ExpRep :: (OPPOSITE k, k) +-> k) @ ('('OP a, b) :: (OPPOSITE k, k)) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Closed

type (ExpRep :: (OPPOSITE k, k) +-> k) @ ('('OP a, b) :: (OPPOSITE k, k)) = a ~~> b
type (OpAction t :: (OPPOSITE m, OPPOSITE k) +-> OPPOSITE k) @ ('('OP a, 'OP x) :: (OPPOSITE m, OPPOSITE k)) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Action

type (OpAction t :: (OPPOSITE m, OPPOSITE k) +-> OPPOSITE k) @ ('('OP a, 'OP x) :: (OPPOSITE m, OPPOSITE k)) = 'OP (t % '(a, x))
type (LimitAdj j :: COREPK b k -> REPK a k -> Type) %% (c :: COREPK b k) Source Github # 
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 Github # 
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 Github #

Flips the two arguments of a profunctor, giving a profunctor between the OPPOSITE categories; at p = (~>) this is the hom of the opposite category.

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 Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

Methods

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

(Prostrong w p, CategoryOf j, CategoryOf k) => Prostrong (w :: FLAVOR (OPPOSITE k) (OPPOSITE j)) (Op (UnOp p) :: OPPOSITE j -> OPPOSITE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Optic

Methods

proact :: forall (f :: OPPOSITE j +-> OPPOSITE j) (g :: OPPOSITE k +-> OPPOSITE k). (w f g, Profunctor f, Profunctor g) => ((f :.: Op (UnOp p)) :.: g) :~> Op (UnOp p) 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 #

TermUniversal b l => InitUniversal ('OP b :: OPPOSITE j) (Op l :: OPPOSITE j -> OPPOSITE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Universal

Associated Types

type InitUnivTgt (Op l :: OPPOSITE j -> OPPOSITE k -> Type) ('OP b :: OPPOSITE j) 
Instance details

Defined in Proarrow.Universal

type InitUnivTgt (Op l :: OPPOSITE j -> OPPOSITE k -> Type) ('OP b :: OPPOSITE j) = 'OP (TermUnivSrc l b)

Methods

initUnivArr :: Op l ('OP b) (InitUnivTgt (Op l) ('OP b)) Source Github #

initUnivProp :: forall (b0 :: OPPOSITE k). Op l ('OP b) b0 -> InitUnivTgt (Op l) ('OP b) ~> b0 Source Github #

InitUniversal a r => TermUniversal ('OP a :: OPPOSITE k) (Op r :: OPPOSITE j -> OPPOSITE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Universal

Associated Types

type TermUnivSrc (Op r :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE k) 
Instance details

Defined in Proarrow.Universal

type TermUnivSrc (Op r :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE k) = 'OP (InitUnivTgt r a)

Methods

termUnivArr :: Op r (TermUnivSrc (Op r) ('OP a)) ('OP a) Source Github #

termUnivProp :: forall (a0 :: OPPOSITE j). Op r a0 ('OP a) -> a0 ~> TermUnivSrc (Op r) ('OP a) Source Github #

Finitary p => Finitary (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Github #

The opposite of a finitary profunctor is finitary, at the same sizes read the other way round. Taking p = Hom k this makes OPPOSITE k a FiniteCat whenever k is one, so everything computed for a finite site is available on the opposite category too. (This instance lives here rather than with Op because Proarrow.Category.Instance.Opposite sits below this module in the import graph.)

Instance details

Defined in Proarrow.Category.Enriched.Finitary

Methods

size :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). (Ob a, Ob b) => Natural Source Github #

toIndex :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). (Ob a, Ob b) => Op p a b -> Natural Source Github #

fromIndex :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). (Ob a, Ob b) => Natural -> Op p a b Source Github #

elements :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). (Ob a, Ob b) => [Op p a b] Source Github #

DecidableProfunctor p => DecidableProfunctor (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

Methods

decide :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). (Ob a, Ob b) => Decision (Op p) a b (Holds (Op p) a b) Source Github #

toHolds :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) r. Op p a b -> ((Holds (Op p) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

ThinProfunctor p => ThinProfunctor (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

Methods

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

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

MonoidalProfunctor p => MonoidalProfunctor (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal

Methods

one :: Op p (Unit :: OPPOSITE j) (Unit :: OPPOSITE k) Source Github #

(**) :: 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 Github #

Profunctor p => Profunctor (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.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 Github #

lmap :: forall (c :: OPPOSITE j) (a :: OPPOSITE j) (b :: OPPOSITE k). (c ~> a) -> Op p a b -> Op p c b Source Github #

rmap :: forall (b :: OPPOSITE k) (d :: OPPOSITE k) (a :: OPPOSITE j). (b ~> d) -> Op p a b -> Op p a d Source Github #

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

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

Defined in Proarrow.Profunctor.Representable

Methods

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

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

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

corepUniv :: forall (a :: OPPOSITE j). Ob a => Op p a (Op p %% a) Source Github #

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

Defined in Proarrow.Profunctor.Representable

Methods

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

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

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

repUniv :: forall (a :: OPPOSITE k). Ob a => Op p (Op p % a) a Source Github #

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

Defined in Proarrow.Adjunction

Methods

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

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

Promonad c => Promonad (Op c :: OPPOSITE j -> OPPOSITE j -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

Methods

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

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

Functor (Op :: (j +-> k) -> OPPOSITE j -> OPPOSITE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

Methods

map :: forall (a :: j +-> k) (b :: j +-> k). (a ~> b) -> Op a ~> Op b Source Github #

type ProObj (Clone v) (Op p :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE j) ('OP b :: OPPOSITE k) Source Github # 
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 Github # 
Instance details

Defined in Proarrow.Profunctor.Representable

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 Github # 
Instance details

Defined in Proarrow.Profunctor.Representable

type (Op p :: OPPOSITE j -> OPPOSITE k -> Type) % ('OP a :: OPPOSITE k) = 'OP (p %% a)
type InitUnivTgt (Op l :: OPPOSITE j -> OPPOSITE k -> Type) ('OP b :: OPPOSITE j) Source Github # 
Instance details

Defined in Proarrow.Universal

type InitUnivTgt (Op l :: OPPOSITE j -> OPPOSITE k -> Type) ('OP b :: OPPOSITE j) = 'OP (TermUnivSrc l b)
type TermUnivSrc (Op r :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Universal

type TermUnivSrc (Op r :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE k) = 'OP (InitUnivTgt r a)
type HasArrow (Op p :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE j) ('OP b :: OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

type HasArrow (Op p :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE j) ('OP b :: OPPOSITE k) = HasArrow p b a
type Holds (Op p :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE j) ('OP b :: OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

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

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

Inverse to Op: unwraps a profunctor between OPPOSITE categories to one between the underlying kinds.

Constructors

UnOp 

Fields

Instances

Instances details
(Thin j, Thin k, DecidableProfunctor p) => DecidableProfunctor (UnOp p :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

Methods

decide :: forall (a :: k) (b :: j). (Ob a, Ob b) => Decision (UnOp p) a b (Holds (UnOp p) a b) Source Github #

toHolds :: forall (a :: k) (b :: j) r. UnOp p a b -> ((Holds (UnOp p) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(Thin j, Thin k, ThinProfunctor p) => ThinProfunctor (UnOp p :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

Methods

arr :: forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow (UnOp p) a b) => UnOp p a b Source Github #

withArr :: forall (a :: k) (b :: j) r. UnOp p a b -> ((HasArrow (UnOp p) a b, Ob a, Ob b) => r) -> r Source Github #

(CategoryOf j, CategoryOf k, Profunctor p) => Profunctor (UnOp p :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.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 Github #

lmap :: forall (c :: k) (a :: k) (b :: j). (c ~> a) -> UnOp p a b -> UnOp p c b Source Github #

rmap :: forall (b :: j) (d :: j) (a :: k). (b ~> d) -> UnOp p a b -> UnOp p a d Source Github #

(\\) :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> UnOp p a b -> r Source Github #

(Prostrong w p, CategoryOf j, CategoryOf k) => Prostrong (OpFlavor w :: (k +-> k) -> (j +-> j) -> Constraint) (UnOp p :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Optic

Methods

proact :: forall (f :: k +-> k) (g :: j +-> j). (OpFlavor w f g, Profunctor f, Profunctor g) => ((f :.: UnOp p) :.: g) :~> UnOp p Source Github #

(Prostrong w p, CategoryOf j, CategoryOf k) => Prostrong (w :: FLAVOR (OPPOSITE k) (OPPOSITE j)) (Op (UnOp p) :: OPPOSITE j -> OPPOSITE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Optic

Methods

proact :: forall (f :: OPPOSITE j +-> OPPOSITE j) (g :: OPPOSITE k +-> OPPOSITE k). (w f g, Profunctor f, Profunctor g) => ((f :.: Op (UnOp p)) :.: g) :~> Op (UnOp p) Source Github #

type HasArrow (UnOp p :: k -> j -> Type) (a :: k) (b :: j) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

type HasArrow (UnOp p :: k -> j -> Type) (a :: k) (b :: j) = HasArrow p ('OP b) ('OP a)
type Holds (UnOp p :: k -> j -> Type) (a :: k) (b :: j) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

type Holds (UnOp p :: k -> j -> Type) (a :: k) (b :: j) = Holds p ('OP b) ('OP a)