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
bindRep :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: k). (Adjunction p, Ob b) => (a ~> (p % (p %% b))) -> (p % (p %% a)) ~> (p % (p %% b))
extendRep :: forall {j} {k} (p :: j +-> k) (a :: j) (b :: j). (Adjunction p, Ob a) => ((p %% (p % a)) ~> b) -> (p %% (p % a)) ~> (p %% (p % b))
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)

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 #

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

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

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

extendRep :: forall {j} {k} (p :: j +-> k) (a :: j) (b :: j). (Adjunction p, Ob a) => ((p %% (p % a)) ~> b) -> (p %% (p % a)) ~> (p %% (p % b)) 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 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 # (\\) :: 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 #
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 #
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 # (\\) :: 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 #
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 #
(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

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