Safe Haskell	None
Language	GHC2024

Proarrow.Profunctor.Instance.Adj

Description

The Adj newtype marks a profunctor as the heteromorphism profunctor of an adjunction: because left adjoints preserve colimits and right adjoints preserve limits, Adj p is a distributive monoidal profunctor. Also proves that every adjunction between Hask endofunctors is equivalent to the curry/uncurry adjunction (haskAdjIsCurryAdj).

Synopsis

newtype Adj (p :: k -> k1 -> Type) (a :: k) (b :: k1) = Adj (p a b)
haskAdjIsCurryAdj :: Adjunction p => PIso ((p %% ()) -> a -> b) ((p %% ()) -> a' -> b') (p a b) (p a' b')

Documentation

newtype Adj (p :: k -> k1 -> Type) (a :: k) (b :: k1) Source Github #

Preservation of limits and colimits makes the adjunction heteromorphism a distributive profunctor.

Constructors

Adj (p a b)

Instances

Instances details

(Cartesian j, Cartesian k, Corepresentable p) => MonoidalProfunctor (Adj p :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Adj Methods one :: Adj p (Unit :: k) (Unit :: j) Source Github # () :: forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j). Adj p x1 x2 -> Adj p y1 y2 -> Adj p (x1 y1) (x2 ** y2) Source Github #
Profunctor p => Profunctor (Adj p :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Adj Methods dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> Adj p a b -> Adj p c d Source Github # lmap :: forall (c :: k) (a :: k) (b :: j). (c ~> a) -> Adj p a b -> Adj p c b Source Github # rmap :: forall (b :: j) (d :: j) (a :: k). (b ~> d) -> Adj p a b -> Adj p a d Source Github # (\\) :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> Adj p a b -> r Source Github #
Corepresentable p => Corepresentable (Adj p :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Adj Methods coindex :: forall (a :: k) (b :: j). Adj p a b -> (Adj p %% a) ~> b Source Github # cotabulate :: forall (a :: k) (b :: j). Ob a => ((Adj p %% a) ~> b) -> Adj p a b Source Github # corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (Adj p %% a) ~> (Adj p %% b) Source Github # corepUniv :: forall (a :: k). Ob a => Adj p a (Adj p %% a) Source Github #
Representable p => Representable (Adj p :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Adj Methods index :: forall (a :: k) (b :: j). Adj p a b -> a ~> (Adj p % b) Source Github # tabulate :: forall (b :: j) (a :: k). Ob b => (a ~> (Adj p % b)) -> Adj p a b Source Github # repMap :: forall (a :: j) (b :: j). (a ~> b) -> (Adj p % a) ~> (Adj p % b) Source Github # repUniv :: forall (a :: j). Ob a => Adj p (Adj p % a) a Source Github #
Adjunction p => Promonad (Adj p :: Type -> Type -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Adj Methods id :: Ob a => Adj p a a Source Github # (.) :: Adj p b c -> Adj p a b -> Adj p a c Source Github #
(HasCoproducts j, HasCoproducts k, Representable p) => MonoidalProfunctor (Coprod (Adj p) :: COPROD k -> COPROD j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Adj Methods one :: Coprod (Adj p) (Unit :: COPROD k) (Unit :: COPROD j) Source Github # () :: forall (x1 :: COPROD k) (x2 :: COPROD j) (y1 :: COPROD k) (y2 :: COPROD j). Coprod (Adj p) x1 x2 -> Coprod (Adj p) y1 y2 -> Coprod (Adj p) (x1 y1) (x2 ** y2) Source Github #
type (Adj p :: k -> j -> Type) %% (a :: k) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Adj type (Adj p :: k -> j -> Type) %% (a :: k) = p %% a
type (Adj p :: k -> j -> Type) % (a :: j) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Adj type (Adj p :: k -> j -> Type) % (a :: j) = p % a

haskAdjIsCurryAdj :: Adjunction p => PIso ((p %% ()) -> a -> b) ((p %% ()) -> a' -> b') (p a b) (p a' b') Source Github #

Every adjunction between Hask endofunctors is equivalent to the curry-uncurry adjunction.