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
unitRep :: forall {j} {k} (p :: j +-> k) (a :: k). (Adjunction p, Ob a) => a ~> (p % (p %% a))
counitRep :: forall {k1} {k2} (p :: k1 +-> k2) (a :: k1). (Adjunction p, Ob a) => (p %% (p % 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)

Documentation

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

Adjunctions as heteromorphisms.

Instances

Instances details

(Representable p, Corepresentable p) => Adjunction (p :: j +-> k) Source Comments #
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 Comments #

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

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

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

class (Profunctor p, Profunctor q) => Proadjunction (p :: j +-> k) (q :: k +-> j) 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

Representable f => Proadjunction (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 => Proadjunction (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 #
Corepresentable f => Proadjunction (CorepStar f :: k -> j -> Type) (f :: k +-> j) Source Comments #
Instance details Defined in Proarrow.Adjunction Methods unit :: forall (a :: j). Ob a => (f :.: CorepStar f) a a Source Comments # counit :: (CorepStar f :.: f) :~> ((~>) :: CAT k) Source Comments #
(Ob r, MonoidalAction m k) => Proadjunction (Writer r :: k -> k -> Type) (Reader ('OP r) :: k -> k -> Type) Source Comments #
Instance details Defined in Proarrow.Promonad.Reader Methods unit :: forall (a :: k). Ob a => ((Reader ('OP r) :: k -> k -> Type) :.: (Writer r :: k -> k -> Type)) a a Source Comments # counit :: ((Writer r :: k -> k -> Type) :.: (Reader ('OP r) :: k -> k -> Type)) :~> ((~>) :: CAT k) Source Comments #
(Proadjunction l1 r1, Proadjunction l2 r2) => Proadjunction (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 => Proadjunction (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 #
Proadjunction q p => Proadjunction (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 #

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

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 Comments #
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 Comments # (\\) :: forall (a0 :: COREPK b k) (b0 :: REPK a k) r. ((Ob a0, Ob b0) => r) -> LimitAdj j a0 b0 -> r Source Comments #
HasColimits j k => Corepresentable (LimitAdj j :: COREPK b k -> REPK a k -> Type) Source Comments #
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 Comments # 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 Comments # 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 Comments #
HasLimits j k => Representable (LimitAdj j :: COREPK b k -> REPK a k -> Type) Source Comments #	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 Comments # 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 Comments # 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 Comments #
type (LimitAdj j :: COREPK b k -> REPK a k -> Type) %% (c :: COREPK b k) Source Comments #
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 Comments #
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 Comments #

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 Comments #

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 Comments #

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 Comments #

Orphan instances

Corepresentable (Star ((->) a) :: Type -> Type -> Type) Source Comments #	The left adjoint of `((->) a)` is `(,) a`.
Instance details Methods coindex :: Star ((->) a) a0 b -> (Star ((->) a) %% a0) ~> b Source Comments # cotabulate :: Ob a0 => ((Star ((->) a) %% a0) ~> b) -> Star ((->) a) a0 b Source Comments # corepMap :: (a0 ~> b) -> (Star ((->) a) %% a0) ~> (Star ((->) a) %% b) Source Comments #
Representable (Costar ((,) a) :: Type -> Type -> Type) Source Comments #	The right adjoint of `(,) a` is `((->) a)`.
Instance details Methods index :: Costar ((,) a) a0 b -> a0 ~> (Costar ((,) a) % b) Source Comments # tabulate :: Ob b => (a0 ~> (Costar ((,) a) % b)) -> Costar ((,) a) a0 b Source Comments # repMap :: (a0 ~> b) -> (Costar ((,) a) % a0) ~> (Costar ((,) a) % b) Source Comments #
Proadjunction 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 #
Proadjunction 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 #