proarrow-0: Category theory with a central role for profunctors
Safe HaskellNone
LanguageHaskell2010

Proarrow.Adjunction

Synopsis

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 :: forall (a :: LINEAR). Ob a => (Forget :.: Free) a a Source Comments #

counit :: (Free :.: Forget) :~> ((~>) :: CAT Type) 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 :: k -> i -> Type) (r2 :.: r1 :: i -> k -> Type) Source Comments # 
Instance details

Defined in Proarrow.Adjunction

Methods

unit :: forall (a :: i). Ob a => ((r2 :.: r1) :.: (l1 :.: l2)) a a Source Comments #

counit :: ((l1 :.: l2) :.: (r2 :.: r1)) :~> ((~>) :: CAT k) Source Comments #

Adjunction List (Forget Monoid) Source Comments # 
Instance details

Defined in Proarrow.Profunctor.Forget

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 #

Profunctor j => Adjunction (Star (Precompose j :: PRO i2 k -> i2 -> i1 -> Type) :: (i2 -> i1 -> Type) -> PRO i2 k -> Type) (Star (Rift ('OP j) :: PRO i2 i1 -> i2 -> k -> Type) :: (i2 -> k -> Type) -> PRO i2 i1 -> Type) Source Comments # 
Instance details

Defined in Proarrow.Profunctor.Rift

Methods

unit :: forall (a :: PRO i2 k). Ob a => (Star (Rift ('OP j) :: PRO i2 i1 -> i2 -> k -> Type) :.: Star (Precompose j :: PRO i2 k -> i2 -> i1 -> Type)) a a Source Comments #

counit :: (Star (Precompose j :: PRO i2 k -> i2 -> i1 -> Type) :.: Star (Rift ('OP j) :: PRO i2 i1 -> i2 -> k -> Type)) :~> ((~>) :: CAT (i2 -> i1 -> Type)) Source Comments #

Profunctor j2 => Adjunction (Star ((:.:) j2 :: PRO j1 k -> i -> k -> Type) :: (i -> k -> Type) -> PRO j1 k -> Type) (Star (Ran ('OP j2) :: PRO i k -> j1 -> k -> Type) :: (j1 -> k -> Type) -> PRO i k -> Type) Source Comments # 
Instance details

Defined in Proarrow.Profunctor.Ran

Methods

unit :: forall (a :: PRO j1 k). Ob a => (Star (Ran ('OP j2) :: PRO i k -> j1 -> k -> Type) :.: Star ((:.:) j2 :: PRO j1 k -> i -> k -> Type)) a a Source Comments #

counit :: (Star ((:.:) j2 :: PRO j1 k -> i -> k -> Type) :.: Star (Ran ('OP j2) :: PRO i k -> j1 -> k -> Type)) :~> ((~>) :: CAT (i -> k -> Type)) Source Comments #

leftAdjunct :: forall {k1} {k2} (l :: k1 -> k2) (r :: k2 -> k1) (a :: k1) (b :: k2). (Adjunction (Star l) (Star r), Functor r, Ob a) => (l a ~> b) -> a ~> r b Source Comments #

rightAdjunct :: forall {k1} {k2} (l :: k1 -> k2) (r :: k2 -> k1) (a :: k1) (b :: k2). (Adjunction (Star l) (Star r), Functor l, Ob b) => (a ~> r b) -> l a ~> b Source Comments #

unitFromStarUnit :: forall {k} {k2} (l :: k -> k2) (r :: k2 -> k) (a :: k). (Functor l, Ob a) => (a ~> r (l a)) -> (Star r :.: Star l) a a Source Comments #

counitFromStarCounit :: forall {j} {k} (l :: j -> k) (r :: k -> j) (a :: k) (b :: k). Functor l => (forall (c :: k). Ob c => l (r c) ~> c) -> (Star l :.: Star r) a b -> a ~> b Source Comments #

Orphan instances

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 #