License	BSD-style (see the file LICENSE)
Maintainer	sjoerd@w3future.com
Stability	experimental
Portability	non-portable
Safe Haskell	Safe
Language	Haskell2010

Data.Category.Adjunction

Contents

Adjunctions
Adjunctions as a category
Adjunctions from universal morphisms
Universal morphisms from adjunctions
Examples

Description

Synopsis

data Adjunction c d f g = (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => Adjunction {
- leftAdjoint :: f
- rightAdjoint :: g
- leftAdjunctN :: Profunctors c d (Costar f) (Star g)
- rightAdjunctN :: Profunctors c d (Star g) (Costar f)
}
mkAdjunction :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b)) -> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b) -> Adjunction c d f g
mkAdjunctionUnits :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall a. Obj d a -> Component (Id d) (g :.: f) a) -> (forall a. Obj c a -> Component (f :.: g) (Id c) a) -> Adjunction c d f g
leftAdjunct :: Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
rightAdjunct :: Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b
adjunctionUnit :: Adjunction c d f g -> Nat d d (Id d) (g :.: f)
adjunctionCounit :: Adjunction c d f g -> Nat c c (f :.: g) (Id c)
idAdj :: Category k => Adjunction k k (Id k) (Id k)
composeAdj :: Adjunction d e f g -> Adjunction c d f' g' -> Adjunction c e (f' :.: f) (g :.: g')
data AdjArrow c d where
- AdjArrow :: (Category c, Category d) => Adjunction c d f g -> AdjArrow (CatW c) (CatW d)
initialPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall y. Obj d y -> InitialUniversal y g (f :% y)) -> Adjunction c d f g
terminalPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall x. Obj c x -> TerminalUniversal x f (g :% x)) -> Adjunction c d f g
adjunctionInitialProp :: Adjunction c d f g -> Obj d y -> InitialUniversal y g (f :% y)
adjunctionTerminalProp :: Adjunction c d f g -> Obj c x -> TerminalUniversal x f (g :% x)
precomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat c e) (Nat d e) (Precompose g e) (Precompose f e)
postcomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat e c) (Nat e d) (Postcompose f e) (Postcompose g e)
contAdj :: Adjunction (Op (->)) (->) (Opposite ((->) :-*: r) :.: OpOpInv (->)) ((->) :-*: r)

Adjunctions

data Adjunction c d f g Source #

Constructors

(Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => Adjunction
Fields leftAdjoint :: f rightAdjoint :: g leftAdjunctN :: Profunctors c d (Costar f) (Star g) rightAdjunctN :: Profunctors c d (Star g) (Costar f)

mkAdjunction :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b)) -> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b) -> Adjunction c d f g Source #

mkAdjunctionUnits :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall a. Obj d a -> Component (Id d) (g :.: f) a) -> (forall a. Obj c a -> Component (f :.: g) (Id c) a) -> Adjunction c d f g Source #

leftAdjunct :: Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b) Source #

rightAdjunct :: Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b Source #

adjunctionUnit :: Adjunction c d f g -> Nat d d (Id d) (g :.: f) Source #

adjunctionCounit :: Adjunction c d f g -> Nat c c (f :.: g) (Id c) Source #

Adjunctions as a category

idAdj :: Category k => Adjunction k k (Id k) (Id k) Source #

composeAdj :: Adjunction d e f g -> Adjunction c d f' g' -> Adjunction c e (f' :.: f) (g :.: g') Source #

data AdjArrow c d where Source #

Constructors

AdjArrow :: (Category c, Category d) => Adjunction c d f g -> AdjArrow (CatW c) (CatW d)

Instances

Category AdjArrow Source #	The category with categories as objects and adjunctions as arrows.
Instance details Defined in Data.Category.Adjunction Methods src :: AdjArrow a b -> Obj AdjArrow a Source # tgt :: AdjArrow a b -> Obj AdjArrow b Source # (.) :: AdjArrow b c -> AdjArrow a b -> AdjArrow a c Source #

Adjunctions from universal morphisms

initialPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall y. Obj d y -> InitialUniversal y g (f :% y)) -> Adjunction c d f g Source #

terminalPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall x. Obj c x -> TerminalUniversal x f (g :% x)) -> Adjunction c d f g Source #

Universal morphisms from adjunctions

adjunctionInitialProp :: Adjunction c d f g -> Obj d y -> InitialUniversal y g (f :% y) Source #

adjunctionTerminalProp :: Adjunction c d f g -> Obj c x -> TerminalUniversal x f (g :% x) Source #

Examples

precomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat c e) (Nat d e) (Precompose g e) (Precompose f e) Source #

postcomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat e c) (Nat e d) (Postcompose f e) (Postcompose g e) Source #

contAdj :: Adjunction (Op (->)) (->) (Opposite ((->) :-*: r) :.: OpOpInv (->)) ((->) :-*: r) Source #