Safe Haskell	None
Language	GHC2024

Proarrow.Adjunction

Contents

Orphan instances

Description

Adjunctions as heteromorphisms: an Adjunction is a profunctor that is both Representable (by the right adjoint) and Corepresentable (by the left adjoint), giving unitRep/counitRep and leftAdjunct/rightAdjunct. Also the profunctor-level notion Proadjunction, and the interaction of adjoints with (co)limits.

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') => PIso (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') => PIso 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') => PIso a a' (AdjMonad p % a) (AdjMonad p % a')
- counitIso :: forall (a :: j) (a' :: j). (Ob a, Ob a') => PIso (AdjComonad p %% a) (AdjComonad p %% a') a a'
type GaloisConnection (p :: j +-> k) = (ThinProfunctor p, Thin j, Thin k, Adjunction p)
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)
class Proadjunction p q => LeftProadjoint (q :: k +-> j) (p :: j +-> k)
unit' :: forall {k1} {j} (p :: k1 +-> j) (q :: j +-> k1). Proadjunction p q => ((~>) :: CAT k1) :~> (q :.: p)
flipMate :: forall {k1} (p :: k1 +-> k1) (q :: k1 +-> k1). Proadjunction p q => (((~>) :: CAT k1) :~> p) -> q :~> ((~>) :: CAT k1)
unflipMate :: forall {k1} (p :: k1 +-> k1) (q :: k1 +-> k1). Proadjunction p q => (q :~> ((~>) :: CAT k1)) -> ((~>) :: CAT k1) :~> p
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 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 #

One direction of the adjunction isomorphism: transpose an arrow out of the left adjoint, p %% a ~> b, to an arrow into the right adjoint, a ~> p % b.

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

The other direction of the adjunction isomorphism, inverse to leftAdjunct.

adjuncted :: forall {k1} {k2} (p :: k1 +-> k2) (a :: k1) (b :: k2) (a' :: k1) (b' :: k2). (Adjunction p, Ob a, Ob b') => PIso (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') => PIso 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') => PIso 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') => PIso 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') => PIso a a' (AdjMonad p % a) (AdjMonad p % a') Source Github #

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

type GaloisConnection (p :: j +-> k) = (ThinProfunctor p, Thin j, Thin k, Adjunction p) 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 #
Monoidal k => Proadjunction (UnitW :: k -> k -> Type) (CoUnitW :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.Traversal Methods unit :: forall (a :: k). Ob a => ((CoUnitW :: k -> k -> Type) :.: (UnitW :: k -> k -> Type)) a a Source Github # counit :: ((UnitW :: k -> k -> Type) :.: (CoUnitW :: k -> k -> Type)) :~> ((~>) :: CAT k) Source Github #
HasInitialObject k => Proadjunction (ZeroW :: k -> k -> Type) (CoZeroW :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.Traversal Methods unit :: forall (a :: k). Ob a => ((CoZeroW :: k -> k -> Type) :.: (ZeroW :: k -> k -> Type)) a a Source Github # counit :: ((ZeroW :: k -> k -> Type) :.: (CoZeroW :: k -> k -> Type)) :~> ((~>) :: CAT k) 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 #
(Monoidal k, SNatI n) => Proadjunction (Pow n :: k -> k -> Type) (CoPow n :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.PowerGrate Methods unit :: forall (a :: k). Ob a => ((CoPow n :: k -> k -> Type) :.: (Pow n :: k -> k -> Type)) a a Source Github # counit :: ((Pow n :: k -> k -> Type) :.: (CoPow n :: 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 #
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 #
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 #
(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 #
(Proadjunction p1 q1, Proadjunction p2 q2) => Proadjunction (p1 :: p2 :: (j1, j2) -> (k1, k2) -> Type) (q1 :: q2 :: (k1, k2) -> (j1, j2) -> Type) Source Github #	Adjunctions pair up over the product category.
Instance details Defined in Proarrow.Adjunction Methods unit :: forall (a :: (k1, k2)). Ob a => ((q1 :: q2) :.: (p1 :: p2)) a a Source Github # counit :: ((p1 :: p2) :.: (q1 :: q2)) :~> ((~>) :: CAT (j1, j2)) Source Github #

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

Proadjunction with the right adjoint first, so that the laws about elements of the left adjoint can be indexed by it.

Instances

Instances details

Proadjunction p q => LeftProadjoint (q :: k +-> j) (p :: j +-> k) Source Github #
Instance details Defined in Proarrow.Adjunction

unit' :: forall {k1} {j} (p :: k1 +-> j) (q :: j +-> k1). Proadjunction p q => ((~>) :: CAT k1) :~> (q :.: p) Source Github #

flipMate :: forall {k1} (p :: k1 +-> k1) (q :: k1 +-> k1). Proadjunction p q => (((~>) :: CAT k1) :~> p) -> q :~> ((~>) :: CAT k1) Source Github #

unflipMate :: forall {k1} (p :: k1 +-> k1) (q :: k1 +-> k1). Proadjunction p q => (q :~> ((~>) :: CAT k1)) -> ((~>) :: CAT k1) :~> p Source Github #

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

The heteromorphisms witnessing the Colimit j ⊣ Limit j adjunction: a natural transformation j :~> c :.: r, read as an arrow from the corepresentable c to the representable r.

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 # corepUniv :: 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 # repUniv :: 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 #

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 # corepUniv :: 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 # repUniv :: 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 :: k -> k -> Type) Source Github #
Instance details Methods proextract :: (p :.: q) :~> ((~>) :: CAT k) Source Github # produplicate :: (p :.: q) :~> ((p :.: q) :.: (p :.: q)) Source Github #