Safe Haskell | None |
---|---|
Language | Haskell2010 |
Proarrow.Adjunction
Contents
Synopsis
- class (Profunctor p, Profunctor q) => Adjunction (p :: PRO k j) (q :: PRO j k) where
- 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
- 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
- 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
- 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
Documentation
class (Profunctor p, Profunctor q) => Adjunction (p :: PRO k j) (q :: PRO j k) where Source Comments #
Adjunctions between two profunctors.
Instances
Adjunction Free Forget Source Comments # | |
CategoryOf k => Adjunction (Id :: k -> k -> Type) (Id :: k -> k -> Type) Source Comments # | |
Adjunction (Star ((,) a) :: Type -> Type -> Type) (Star ((->) a) :: Type -> Type -> 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 # | |
Functor f => Adjunction (Star f :: k -> j -> Type) (Costar f :: j -> k -> Type) Source Comments # | |
(Adjunction l1 r1, Adjunction l2 r2) => Adjunction (l1 :.: l2 :: k -> i -> Type) (r2 :.: r1 :: i -> k -> Type) Source Comments # | |
Adjunction List (Forget Monoid) Source Comments # | |
Promonad p => Adjunction (KleisliFree p :: KLEISLI p -> k -> Type) (KleisliForget p :: k -> KLEISLI p -> Type) Source Comments # | |
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 # | |
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 # | |
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 #