Safe Haskell	None
Language	GHC2024

Proarrow.Adjunction

Contents

Orphan instances

Synopsis

class (Representable p, Corepresentable p) => Adjunction (p :: j +-> k)
leftAdjunct :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j). (Adjunction p, Ob a) => ((p %% a) ~> b) -> a ~> (p % b)
rightAdjunct :: forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1). (Adjunction p, Ob b) => (a ~> (p % b)) -> (p %% a) ~> b
adjuncted :: forall {k1} {k2} (p :: k1 +-> k2) (a :: k1) (b :: k2) (a' :: k1) (b' :: k2). (Adjunction p, Ob a, Ob b') => Iso (b ~> (p % a)) (b' ~> (p % a')) ((p %% b) ~> a) ((p %% b') ~> a')
type AdjMonad (p :: k +-> i) = p :.: CorepStar p
unitRep :: forall {k} {j} (p :: k +-> j) (a :: j). (Adjunction p, Ob a) => a ~> (AdjMonad p % a)
bindRep :: forall {k} {j} (p :: k +-> j) (a :: j) (b :: j). (Adjunction p, Ob b) => (a ~> (AdjMonad p % b)) -> (AdjMonad p % a) ~> (AdjMonad p % b)
type AdjComonad (p :: i +-> j) = RepCostar p :.: p
counitRep :: forall {k} {j} (p :: k +-> j) (a :: k). (Adjunction p, Ob a) => (AdjComonad p %% a) ~> a
extendRep :: forall {j1} {j2} (p :: j1 +-> j2) (a :: j1) (b :: j1). (Adjunction p, Ob a) => ((AdjComonad p %% a) ~> b) -> (AdjComonad p %% a) ~> (AdjComonad p %% b)
class ((p % a) ~ (p %% a), (p % (p %% a)) ~ (p % (p % a)), (p %% (p % a)) ~ (p % (p % a))) => SelfAdjointPoint (p :: j +-> j) (a :: j)
class (forall (a :: k). Ob a => SelfAdjointPoint p a, Adjunction p) => SelfAdjoint (p :: k +-> k)
class SelfAdjoint p => Involution (p :: j +-> j) where
- involuted :: forall (a :: j) (a' :: j). (Ob a, Ob a') => Iso a a' (p % (p % a)) (p % (p % a'))
class ((p %% a) ~ (RepCostar p % a), (p % (p %% a)) ~ (p % (RepCostar p % a))) => AmbidextrousEqRep (p :: k +-> j) (a :: j)
class ((p % a) ~ (CorepStar p %% a), (p %% (p % a)) ~ (p %% (CorepStar p %% a))) => AmbidextrousEqCorep (p :: k +-> j) (a :: k)
class (Adjunction p, Representable (RepCostar p), Corepresentable (CorepStar p), forall (a :: j). Ob a => AmbidextrousEqRep p a, forall (a :: k). Ob a => AmbidextrousEqCorep p a) => Ambidextrous (p :: k +-> j)
class Ambidextrous p => AdjointEquivalence (p :: j +-> k) where
- unitIso :: forall (a :: k) (a' :: k). (Ob a, Ob a') => Iso a a' (AdjMonad p % a) (AdjMonad p % a')
- counitIso :: forall (a :: j) (a' :: j). (Ob a, Ob a') => Iso (AdjComonad p %% a) (AdjComonad p %% a') a a'
class (Profunctor p, Profunctor q) => Proadjunction (p :: j +-> k) (q :: k +-> j) where
- unit :: forall (a :: j). Ob a => (q :.: p) a a
- counit :: (p :.: q) :~> ((~>) :: CAT k)
data LimitAdj (j :: a +-> b) (c :: COREPK b k) (r :: REPK a k) where
- LimitAdj :: forall {k} {b} {a} (c1 :: k +-> b) (r1 :: a +-> k) (j :: a +-> b). (Corepresentable c1, Representable r1) => (j :~> (c1 :.: r1)) -> LimitAdj j ('SUB ('OP c1) :: SUBCAT (OpCorepresentable :: OPPOSITE (k +-> b) -> Constraint)) ('SUB r1 :: SUBCAT (Representable :: (a +-> k) -> Constraint))
rightAdjointPreservesLimits :: forall {k} {k'} {i} {a} (j :: i +-> a) (p :: k +-> k') (d :: i +-> k). (Adjunction p, Representable d, HasLimits j k, HasLimits j k') => Limit j (p :.: d) :~> (p :.: Limit j d)
rightAdjointPreservesLimitsInv :: forall {k} {k'} {i} {a} (p :: k +-> k') (d :: i +-> k) (j :: i +-> a). (Representable p, Representable d, HasLimits j k, HasLimits j k') => (p :.: Limit j d) :~> Limit j (p :.: d)
leftAdjointPreservesColimits :: forall {k} {k'} {i} {a} (p :: k' +-> k) (d :: k +-> i) (j :: a +-> i). (Adjunction p, Corepresentable d, HasColimits j k, HasColimits j k') => Colimit j (d :.: p) :~> (Colimit j d :.: p)
leftAdjointPreservesColimitsInv :: forall {k} {k'} {i} {a} (p :: k' +-> k) (d :: k +-> i) (j :: a +-> i). (Corepresentable p, Corepresentable d, HasColimits j k, HasColimits j k') => (Colimit j d :.: p) :~> Colimit j (d :.: p)
newtype Adj (p :: k -> k1 -> Type) (a :: k) (b :: k1) = Adj (p a b)
haskAdjIsCurryAdj :: Adjunction p => Iso ((p %% ()) -> a -> b) ((p %% ()) -> a' -> b') (p a b) (p a' b')

Documentation

class (Representable p, Corepresentable p) => Adjunction (p :: j +-> k) Source Github #

Adjunctions as heteromorphisms.

Instances

Instances details

(Representable p, Corepresentable p) => Adjunction (p :: j +-> k) Source Github #
Instance details Defined in Proarrow.Adjunction

leftAdjunct :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j). (Adjunction p, Ob a) => ((p %% a) ~> b) -> a ~> (p % b) Source Github #

rightAdjunct :: forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1). (Adjunction p, Ob b) => (a ~> (p % b)) -> (p %% a) ~> b Source Github #

adjuncted :: forall {k1} {k2} (p :: k1 +-> k2) (a :: k1) (b :: k2) (a' :: k1) (b' :: k2). (Adjunction p, Ob a, Ob b') => Iso (b ~> (p % a)) (b' ~> (p % a')) ((p %% b) ~> a) ((p %% b') ~> a') Source Github #

The isomorphism between leftAdjunct and rightAdjunct.

type AdjMonad (p :: k +-> i) = p :.: CorepStar p Source Github #

The monad induced by an adjunction as a representable promonad.

unitRep :: forall {k} {j} (p :: k +-> j) (a :: j). (Adjunction p, Ob a) => a ~> (AdjMonad p % a) Source Github #

bindRep :: forall {k} {j} (p :: k +-> j) (a :: j) (b :: j). (Adjunction p, Ob b) => (a ~> (AdjMonad p % b)) -> (AdjMonad p % a) ~> (AdjMonad p % b) Source Github #

type AdjComonad (p :: i +-> j) = RepCostar p :.: p Source Github #

The comonad induced by an adjunction as a corepresentable promonad.

counitRep :: forall {k} {j} (p :: k +-> j) (a :: k). (Adjunction p, Ob a) => (AdjComonad p %% a) ~> a Source Github #

extendRep :: forall {j1} {j2} (p :: j1 +-> j2) (a :: j1) (b :: j1). (Adjunction p, Ob a) => ((AdjComonad p %% a) ~> b) -> (AdjComonad p %% a) ~> (AdjComonad p %% b) Source Github #

class ((p % a) ~ (p %% a), (p % (p %% a)) ~ (p % (p % a)), (p %% (p % a)) ~ (p % (p % a))) => SelfAdjointPoint (p :: j +-> j) (a :: j) Source Github #

Instances

Instances details

((p % a) ~ (p %% a), (p % (p %% a)) ~ (p % (p % a)), (p %% (p % a)) ~ (p % (p % a))) => SelfAdjointPoint (p :: j +-> j) (a :: j) Source Github #
Instance details Defined in Proarrow.Adjunction

class (forall (a :: k). Ob a => SelfAdjointPoint p a, Adjunction p) => SelfAdjoint (p :: k +-> k) Source Github #

Self-adjoint functors

Instances

Instances details

(forall (a :: k). Ob a => SelfAdjointPoint p a, Adjunction p) => SelfAdjoint (p :: k +-> k) Source Github #
Instance details Defined in Proarrow.Adjunction

class SelfAdjoint p => Involution (p :: j +-> j) where Source Github #

Involution functors are self-adjoint functors where the unit and counit form an isomorphism.

Minimal complete definition

Nothing

Methods

involuted :: forall (a :: j) (a' :: j). (Ob a, Ob a') => Iso a a' (p % (p % a)) (p % (p % a')) Source Github #

Instances

Instances details

CategoryOf k => Involution (Id :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Adjunction Methods involuted :: forall (a :: k) (a' :: k). (Ob a, Ob a') => Iso a a' ((Id :: k -> k -> Type) % ((Id :: k -> k -> Type) % a)) ((Id :: k -> k -> Type) % ((Id :: k -> k -> Type) % a')) Source Github #
RealFloat a => Involution (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) :: MatK (Complex a) -> MatK (Complex a) -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Mat Methods involuted :: forall (a0 :: MatK (Complex a)) (a' :: MatK (Complex a)). (Ob a0, Ob a') => Iso a0 a' (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) % (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) % a0)) (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) % (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) % a')) Source Github #

class ((p %% a) ~ (RepCostar p % a), (p % (p %% a)) ~ (p % (RepCostar p % a))) => AmbidextrousEqRep (p :: k +-> j) (a :: j) Source Github #

Instances

Instances details

((p %% a) ~ (RepCostar p % a), (p % (p %% a)) ~ (p % (RepCostar p % a))) => AmbidextrousEqRep (p :: k +-> j) (a :: j) Source Github #
Instance details Defined in Proarrow.Adjunction

class ((p % a) ~ (CorepStar p %% a), (p %% (p % a)) ~ (p %% (CorepStar p %% a))) => AmbidextrousEqCorep (p :: k +-> j) (a :: k) Source Github #

Instances

Instances details

((p % a) ~ (CorepStar p %% a), (p %% (p % a)) ~ (p %% (CorepStar p %% a))) => AmbidextrousEqCorep (p :: k +-> j) (a :: k) Source Github #
Instance details Defined in Proarrow.Adjunction

class (Adjunction p, Representable (RepCostar p), Corepresentable (CorepStar p), forall (a :: j). Ob a => AmbidextrousEqRep p a, forall (a :: k). Ob a => AmbidextrousEqCorep p a) => Ambidextrous (p :: k +-> j) Source Github #

Instances

Instances details

(Adjunction p, Representable (RepCostar p), Corepresentable (CorepStar p), forall (a :: j). Ob a => AmbidextrousEqRep p a, forall (a :: k). Ob a => AmbidextrousEqCorep p a) => Ambidextrous (p :: k +-> j) Source Github #
Instance details Defined in Proarrow.Adjunction

class Ambidextrous p => AdjointEquivalence (p :: j +-> k) where Source Github #

Minimal complete definition

Nothing

Methods

unitIso :: forall (a :: k) (a' :: k). (Ob a, Ob a') => Iso a a' (AdjMonad p % a) (AdjMonad p % a') Source Github #

counitIso :: forall (a :: j) (a' :: j). (Ob a, Ob a') => Iso (AdjComonad p %% a) (AdjComonad p %% a') a a' Source Github #

class (Profunctor p, Profunctor q) => Proadjunction (p :: j +-> k) (q :: k +-> j) where Source Github #

Adjunctions between two profunctors.

Methods

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

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

Instances

Instances details

Representable p => Proadjunction (p :: k +-> j) (RepCostar p :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Adjunction Methods unit :: forall (a :: k). Ob a => (RepCostar p :.: p) a a Source Github # counit :: (p :.: RepCostar p) :~> ((~>) :: CAT j) Source Github #
CategoryOf k => Proadjunction (Id :: k -> k -> Type) (Id :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Adjunction Methods unit :: forall (a :: k). Ob a => ((Id :: k -> k -> Type) :.: (Id :: k -> k -> Type)) a a Source Github # counit :: ((Id :: k -> k -> Type) :.: (Id :: k -> k -> Type)) :~> ((~>) :: CAT k) Source Github #
(Ob r, Monoidal k) => Proadjunction (Writer r :: k -> k -> Type) (Reader ('OP r) :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Promonad.Reader Methods unit :: forall (a :: k). Ob a => (Reader ('OP r) :.: Writer r) a a Source Github # counit :: (Writer r :.: Reader ('OP r)) :~> ((~>) :: CAT k) Source Github #
Corepresentable p => Proadjunction (CorepStar p :: k -> j -> Type) (p :: k +-> j) Source Github #
Instance details Defined in Proarrow.Adjunction Methods unit :: forall (a :: j). Ob a => (p :.: CorepStar p) a a Source Github # counit :: (CorepStar p :.: p) :~> ((~>) :: CAT k) Source Github #
FunctorForRep f => Proadjunction (Rep f :: k -> j -> Type) (Corep f :: j -> k -> Type) Source Github #
Instance details Defined in Proarrow.Adjunction Methods unit :: forall (a :: j). Ob a => (Corep f :.: Rep f) a a Source Github # counit :: (Rep f :.: Corep f) :~> ((~>) :: CAT k) Source Github #
Functor f => Proadjunction (Star f :: k -> j -> Type) (Costar f :: j -> k -> Type) Source Github #
Instance details Defined in Proarrow.Adjunction Methods unit :: forall (a :: j). Ob a => (Costar f :.: Star f) a a Source Github # counit :: (Star f :.: Costar f) :~> ((~>) :: CAT k) Source Github #
(Proadjunction p q, Ob r, Monoidal k) => Proadjunction (WriterT r p :: k -> k -> Type) (ReaderT ('OP r) q :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Promonad.Reader Methods unit :: forall (a :: k). Ob a => (ReaderT ('OP r) q :.: WriterT r p) a a Source Github # counit :: (WriterT r p :.: ReaderT ('OP r) q) :~> ((~>) :: CAT k) Source Github #
(Proadjunction l1 r1, Proadjunction l2 r2) => Proadjunction (l1 :.: l2 :: i -> k -> Type) (r2 :.: r1 :: k -> i -> Type) Source Github #
Instance details Defined in Proarrow.Adjunction Methods unit :: forall (a :: k). Ob a => ((r2 :.: r1) :.: (l1 :.: l2)) a a Source Github # counit :: ((l1 :.: l2) :.: (r2 :.: r1)) :~> ((~>) :: CAT i) Source Github #
Promonad p => Proadjunction (KleisliFree p :: KLEISLI p -> k -> Type) (KleisliForget p :: k -> KLEISLI p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Kleisli Methods unit :: forall (a :: k). Ob a => (KleisliForget p :.: KleisliFree p) a a Source Github # counit :: (KleisliFree p :.: KleisliForget p) :~> ((~>) :: CAT (KLEISLI p)) 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 #

data LimitAdj (j :: a +-> b) (c :: COREPK b k) (r :: REPK a k) where Source Github #

Constructors

LimitAdj :: forall {k} {b} {a} (c1 :: k +-> b) (r1 :: a +-> k) (j :: a +-> b). (Corepresentable c1, Representable r1) => (j :~> (c1 :.: r1)) -> LimitAdj j ('SUB ('OP c1) :: SUBCAT (OpCorepresentable :: OPPOSITE (k +-> b) -> Constraint)) ('SUB r1 :: SUBCAT (Representable :: (a +-> k) -> Constraint))

Instances

Instances details

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 # trivialCorep :: 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 # trivialRep :: forall (a0 :: REPK a k). Ob a0 => LimitAdj j ((LimitAdj j :: COREPK b k -> REPK a k -> Type) % a0) a0 Source Github #
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)))

rightAdjointPreservesLimits :: forall {k} {k'} {i} {a} (j :: i +-> a) (p :: k +-> k') (d :: i +-> k). (Adjunction p, Representable d, HasLimits j k, HasLimits j k') => Limit j (p :.: d) :~> (p :.: Limit j d) Source Github #

rightAdjointPreservesLimitsInv :: forall {k} {k'} {i} {a} (p :: k +-> k') (d :: i +-> k) (j :: i +-> a). (Representable p, Representable d, HasLimits j k, HasLimits j k') => (p :.: Limit j d) :~> Limit j (p :.: d) Source Github #

leftAdjointPreservesColimits :: forall {k} {k'} {i} {a} (p :: k' +-> k) (d :: k +-> i) (j :: a +-> i). (Adjunction p, Corepresentable d, HasColimits j k, HasColimits j k') => Colimit j (d :.: p) :~> (Colimit j d :.: p) Source Github #

leftAdjointPreservesColimitsInv :: forall {k} {k'} {i} {a} (p :: k' +-> k) (d :: k +-> i) (j :: a +-> i). (Corepresentable p, Corepresentable d, HasColimits j k, HasColimits j k') => (Colimit j d :.: p) :~> Colimit j (d :.: p) Source Github #

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, Adjunction p) => MonoidalProfunctor (Adj p :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Adjunction Methods par0 :: Adj p (Unit :: k) (Unit :: j) Source Github # par :: 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.Adjunction 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.Adjunction 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 # trivialCorep :: 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.Adjunction 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 # trivialRep :: 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.Adjunction Methods id :: Ob a => Adj p a a Source Github # (.) :: Adj p b c -> Adj p a b -> Adj p a c Source Github #
(Cocartesian j, Cocartesian k, Adjunction p) => MonoidalProfunctor (Coprod (Adj p) :: COPROD k -> COPROD j -> Type) Source Github #
Instance details Defined in Proarrow.Adjunction Methods par0 :: Coprod (Adj p) (Unit :: COPROD k) (Unit :: COPROD j) Source Github # par :: 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.Adjunction 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.Adjunction type (Adj p :: k -> j -> Type) % (a :: j) = p % a

haskAdjIsCurryAdj :: Adjunction p => Iso ((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.

Orphan instances

Corepresentable (Star ((->) a) :: Type -> Type -> Type) Source Github #	The left adjoint of `((->) a)` is `(,) a`.
Instance details Methods coindex :: Star ((->) a) a0 b -> (Star ((->) a) %% a0) ~> b Source Github # cotabulate :: Ob a0 => ((Star ((->) a) %% a0) ~> b) -> Star ((->) a) a0 b Source Github # corepMap :: (a0 ~> b) -> (Star ((->) a) %% a0) ~> (Star ((->) a) %% b) Source Github # trivialCorep :: Ob a0 => Star ((->) a) a0 (Star ((->) a) %% a0) Source Github #
Representable (Costar ((,) a) :: Type -> Type -> Type) Source Github #	The right adjoint of `(,) a` is `((->) a)`.
Instance details Methods index :: Costar ((,) a) a0 b -> a0 ~> (Costar ((,) a) % b) Source Github # tabulate :: Ob b => (a0 ~> (Costar ((,) a) % b)) -> Costar ((,) a) a0 b Source Github # repMap :: (a0 ~> b) -> (Costar ((,) a) % a0) ~> (Costar ((,) a) % b) Source Github # trivialRep :: Ob a0 => Costar ((,) a) (Costar ((,) a) % a0) a0 Source Github #
Proadjunction p q => Promonad (q :.: p :: k -> k -> Type) Source Github #
Instance details Methods id :: forall (a :: k). Ob a => (q :.: p) a a Source Github # (.) :: forall (b :: k) (c :: k) (a :: k). (q :.: p) b c -> (q :.: p) a b -> (q :.: p) a c Source Github #
Proadjunction p q => Procomonad (p :.: q :: i -> i -> Type) Source Github #
Instance details Methods extract :: (p :.: q) :~> ((~>) :: CAT i) Source Github # duplicate :: (p :.: q) :~> ((p :.: q) :.: (p :.: q)) Source Github #