| Portability | non-portable |
|---|---|
| Stability | experimental |
| Maintainer | sjoerd@w3future.com |
Data.Category.Adjunction
Contents
Description
- 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
- unit :: Nat d d (Id d) (g :.: f)
- counit :: Nat c c (f :.: g) (Id c)
- mkAdjunction :: (Functor f, Functor g, Category c, Category d, 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
- initialPropAdjunction :: forall f g c d. (Functor f, Functor g, Category c, Category d, 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, Category c, Category d, 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)
- data AdjArrow c d where
- limitAdj :: forall j (~>). HasLimits j ~> => LimitFunctor j ~> -> Adjunction (Nat j ~>) ~> (Diag j ~>) (LimitFunctor j ~>)
- colimitAdj :: forall j (~>). HasColimits j ~> => ColimitFunctor j ~> -> Adjunction ~> (Nat j ~>) (ColimitFunctor j ~>) (Diag j ~>)
- adjunctionMonad :: Adjunction c d f g -> Monad (g :.: f)
- adjunctionComonad :: Adjunction c d f g -> Comonad (f :.: g)
- contAdj :: Adjunction (Op (->)) (->) (Cont1 r) (Cont2 r)
Adjunctions
data Adjunction c d f g Source
mkAdjunction :: (Functor f, Functor g, Category c, Category d, 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 gSource
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) bSource
Adjunctions from universal morphisms
initialPropAdjunction :: forall f g c d. (Functor f, Functor g, Category c, Category d, 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 gSource
terminalPropAdjunction :: forall f g c d. (Functor f, Functor g, Category c, Category d, 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 gSource
Adjunctions to universal morphisms
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
Adjunctions as a category
(Co)limitfunctor adjunction
limitAdj :: forall j (~>). HasLimits j ~> => LimitFunctor j ~> -> Adjunction (Nat j ~>) ~> (Diag j ~>) (LimitFunctor j ~>)Source
The limit functor is right adjoint to the diagonal functor.
colimitAdj :: forall j (~>). HasColimits j ~> => ColimitFunctor j ~> -> Adjunction ~> (Nat j ~>) (ColimitFunctor j ~>) (Diag j ~>)Source
The colimit functor is left adjoint to the diagonal functor.
(Co)monad of an adjunction
adjunctionMonad :: Adjunction c d f g -> Monad (g :.: f)Source
adjunctionComonad :: Adjunction c d f g -> Comonad (f :.: g)Source
Examples
contAdj :: Adjunction (Op (->)) (->) (Cont1 r) (Cont2 r)Source