Safe Haskell	None
Language	Haskell2010

Proarrow.Adjunction

Contents

Orphan instances

Synopsis

class (Profunctor p, Profunctor q) => Adjunction (p :: PRO k j) (q :: PRO j k) where
- unit :: forall (a :: j). Ob a => (q :.: p) a a
- counit :: (p :.: q) :~> ((~>) :: CAT k)
unit' :: forall {j} {i} (p :: PRO j i) (q :: PRO i j) (a :: i) (b :: i). Adjunction p q => (a ~> b) -> (q :.: p) a b
leftAdjunct :: forall {k} {j} (l :: PRO k j) r (a :: j) (b :: k). (Adjunction l r, Representable l, Representable r, Ob a) => ((l % a) ~> b) -> r a b
rightAdjunct :: forall {k} {j} (l :: PRO k j) r (a :: j) (b :: k). (Adjunction l r, Representable l, Representable r, Ob b) => r a b -> (l % a) ~> b
unitFromRepUnit :: forall {i} {j} (l :: i +-> j) (r :: j +-> i) (a :: i). (Representable l, Representable r, Ob a) => (a ~> (r % (l % a))) -> (r :.: l) a a
counitFromRepCounit :: forall {j} {k1} (l :: j +-> k1) (r :: k1 +-> j). (Representable l, Representable r) => (forall (c :: k1). Ob c => (l % (r % c)) ~> c) -> (l :.: r) :~> ((~>) :: CAT k1)

Documentation

class (Profunctor p, Profunctor q) => Adjunction (p :: PRO k j) (q :: PRO j k) where Source Comments #

Adjunctions between two profunctors.

Methods

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

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

Instances

Instances details

Adjunction Free Forget Source Comments #
Instance details Defined in Proarrow.Category.Instance.Linear Methods unit :: Ob a => (Forget :.: Free) a a Source Comments # counit :: (Free :.: Forget) :~> ((~>) :: CAT LINEAR) Source Comments #
Representable f => Adjunction (f :: k +-> j) (RepCostar f :: k -> j -> Type) Source Comments #
Instance details Defined in Proarrow.Adjunction Methods unit :: forall (a :: k). Ob a => (RepCostar f :.: f) a a Source Comments # counit :: (f :.: RepCostar f) :~> ((~>) :: CAT j) Source Comments #
CategoryOf k => Adjunction (Id :: k -> k -> Type) (Id :: k -> k -> Type) Source Comments #
Instance details Defined in Proarrow.Adjunction Methods unit :: forall (a :: k). Ob a => ((Id :: k -> k -> Type) :.: (Id :: k -> k -> Type)) a a Source Comments # counit :: ((Id :: k -> k -> Type) :.: (Id :: k -> k -> Type)) :~> ((~>) :: CAT k) Source Comments #
Adjunction (Star ((,) a) :: Type -> Type -> Type) (Star ((->) a) :: Type -> Type -> Type) Source Comments #
Instance details Defined in Proarrow.Adjunction Methods unit :: Ob a0 => (Star ((->) a) :.: Star ((,) a)) a0 a0 Source Comments # counit :: (Star ((,) a) :.: Star ((->) a)) :~> ((~>) :: CAT Type) Source Comments #
(Functor f, Functor g, Adjunction (Star f) (Star g)) => Adjunction (Costar f :: k -> j -> Type) (Costar g :: j -> k -> Type) Source Comments #
Instance details Defined in Proarrow.Adjunction Methods unit :: forall (a :: j). Ob a => (Costar g :.: Costar f) a a Source Comments # counit :: (Costar f :.: Costar g) :~> ((~>) :: CAT k) Source Comments #
Functor f => Adjunction (Star f :: k -> j -> Type) (Costar f :: j -> k -> Type) Source Comments #
Instance details Defined in Proarrow.Adjunction Methods unit :: forall (a :: j). Ob a => (Costar f :.: Star f) a a Source Comments # counit :: (Star f :.: Costar f) :~> ((~>) :: CAT k) Source Comments #
(Adjunction l1 r1, Adjunction l2 r2) => Adjunction (l1 :.: l2 :: i -> k -> Type) (r2 :.: r1 :: k -> i -> Type) Source Comments #
Instance details Defined in Proarrow.Adjunction Methods unit :: forall (a :: k). Ob a => ((r2 :.: r1) :.: (l1 :.: l2)) a a Source Comments # counit :: ((l1 :.: l2) :.: (r2 :.: r1)) :~> ((~>) :: CAT i) Source Comments #
Promonad p => Adjunction (KleisliFree p :: KLEISLI p -> k -> Type) (KleisliForget p :: k -> KLEISLI p -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Kleisli Methods unit :: forall (a :: k). Ob a => (KleisliForget p :.: KleisliFree p) a a Source Comments # counit :: (KleisliFree p :.: KleisliForget p) :~> ((~>) :: CAT (KLEISLI p)) Source Comments #
HasFree ob => Adjunction (FreeSub ob :: SUBCAT ob -> k -> Type) (Forget ob :: k -> SUBCAT ob -> Type) Source Comments #
Instance details Defined in Proarrow.Profunctor.Free Methods unit :: forall (a :: k). Ob a => (Forget ob :.: FreeSub ob) a a Source Comments # counit :: (FreeSub ob :.: Forget ob) :~> ((~>) :: CAT (SUBCAT ob)) Source Comments #
Adjunction q p => Adjunction (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 #
HasCofree ob => Adjunction (Forget ob :: k -> SUBCAT ob -> Type) (CofreeSub ob :: SUBCAT ob -> k -> Type) Source Comments #
Instance details Defined in Proarrow.Profunctor.Cofree Methods unit :: forall (a :: SUBCAT ob). Ob a => (CofreeSub ob :.: Forget ob) a a Source Comments # counit :: (Forget ob :.: CofreeSub ob) :~> ((~>) :: CAT k) Source Comments #
Profunctor j => Adjunction (Star ((:.:) j :: (i2 +-> k) -> i1 -> i2 -> Type) :: (i1 -> i2 -> Type) -> (i2 +-> k) -> Type) (Star (Rift ('OP j) :: (i2 +-> i1) -> k -> i2 -> Type) :: (k -> i2 -> Type) -> (i2 +-> i1) -> Type) Source Comments #
Instance details Defined in Proarrow.Profunctor.Rift Methods unit :: forall (a :: i2 +-> k). Ob a => (Star (Rift ('OP j) :: (i2 +-> i1) -> k -> i2 -> Type) :.: Star ((:.:) j :: (i2 +-> k) -> i1 -> i2 -> Type)) a a Source Comments # counit :: (Star ((:.:) j :: (i2 +-> k) -> i1 -> i2 -> Type) :.: Star (Rift ('OP j) :: (i2 +-> i1) -> k -> i2 -> Type)) :~> ((~>) :: CAT (i1 -> i2 -> Type)) Source Comments #
Profunctor j2 => Adjunction (Star (Precompose j2 :: (j1 +-> k) -> k -> i -> Type) :: (k -> i -> Type) -> (j1 +-> k) -> Type) (Star (Ran ('OP j2) :: (i +-> k) -> k -> j1 -> Type) :: (k -> j1 -> Type) -> (i +-> k) -> Type) Source Comments #
Instance details Defined in Proarrow.Profunctor.Ran Methods unit :: forall (a :: j1 +-> k). Ob a => (Star (Ran ('OP j2) :: (i +-> k) -> k -> j1 -> Type) :.: Star (Precompose j2 :: (j1 +-> k) -> k -> i -> Type)) a a Source Comments # counit :: (Star (Precompose j2 :: (j1 +-> k) -> k -> i -> Type) :.: Star (Ran ('OP j2) :: (i +-> k) -> k -> j1 -> Type)) :~> ((~>) :: CAT (k -> i -> Type)) Source Comments #

unit' :: forall {j} {i} (p :: PRO j i) (q :: PRO i j) (a :: i) (b :: i). Adjunction p q => (a ~> b) -> (q :.: p) a b Source Comments #

leftAdjunct :: forall {k} {j} (l :: PRO k j) r (a :: j) (b :: k). (Adjunction l r, Representable l, Representable r, Ob a) => ((l % a) ~> b) -> r a b Source Comments #

rightAdjunct :: forall {k} {j} (l :: PRO k j) r (a :: j) (b :: k). (Adjunction l r, Representable l, Representable r, Ob b) => r a b -> (l % a) ~> b Source Comments #

unitFromRepUnit :: forall {i} {j} (l :: i +-> j) (r :: j +-> i) (a :: i). (Representable l, Representable r, Ob a) => (a ~> (r % (l % a))) -> (r :.: l) a a Source Comments #

counitFromRepCounit :: forall {j} {k1} (l :: j +-> k1) (r :: k1 +-> j). (Representable l, Representable r) => (forall (c :: k1). Ob c => (l % (r % c)) ~> c) -> (l :.: r) :~> ((~>) :: CAT k1) Source Comments #

Orphan instances

(MonoidalProfunctor r, Adjunction l r, Representable l, Representable r, Monoidal j, Monoidal k) => MonoidalProfunctor (RepCostar l :: k -> j -> Type) Source Comments #
Instance details Methods par0 :: RepCostar l (Unit :: k) (Unit :: j) Source Comments # par :: forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j). RepCostar l x1 x2 -> RepCostar l y1 y2 -> RepCostar l (x1 y1) (x2 y2) Source Comments #
Adjunction p q => Promonad (q :.: p :: k -> k -> Type) Source Comments #
Instance details Methods id :: forall (a :: k). Ob a => (q :.: p) a a Source Comments # (.) :: forall (b :: k) (c :: k) (a :: k). (q :.: p) b c -> (q :.: p) a b -> (q :.: p) a c Source Comments #
Adjunction p q => Procomonad (p :.: q :: i -> i -> Type) Source Comments #
Instance details Methods extract :: (p :.: q) :~> ((~>) :: CAT i) Source Comments # duplicate :: (p :.: q) :~> ((p :.: q) :.: (p :.: q)) Source Comments #