| Portability | non-portable |
|---|---|
| Stability | experimental |
| Maintainer | sjoerd@w3future.com |
Data.Category.Adjunction
Description
- data Adjunction c d f g where
- 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
- unit :: Adjunction c d f g -> Id d :~> (g :.: f)
- counit :: Adjunction c d f g -> (f :.: g) :~> Id c
- 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
- 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)
- initialPropAdjunction :: (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 :: (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
- data AdjArrow c d where
- wrap :: (Functor g, Functor f, Dom g ~ Dom f', Dom g ~ Cod f) => g -> f -> Nat (Dom f') (Dom f') (Id (Dom f')) (g' :.: f') -> (g :.: f) :~> ((g :.: g') :.: (f' :.: f))
- cowrap :: (Functor f', Functor g', Dom f' ~ Dom g, Dom f' ~ Cod g') => f' -> g' -> Nat (Dom g) (Dom g) (f :.: g) (Id (Dom g)) -> ((f' :.: f) :.: (g :.: g')) :~> (f' :.: g')
- curryAdj :: Adjunction (->) (->) (EndoHask ((,) e)) (EndoHask ((->) e))
- 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 ~>)
Documentation
data Adjunction c d f g whereSource
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
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
initialPropAdjunction :: (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 :: (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
wrap :: (Functor g, Functor f, Dom g ~ Dom f', Dom g ~ Cod f) => g -> f -> Nat (Dom f') (Dom f') (Id (Dom f')) (g' :.: f') -> (g :.: f) :~> ((g :.: g') :.: (f' :.: f))Source
cowrap :: (Functor f', Functor g', Dom f' ~ Dom g, Dom f' ~ Cod g') => f' -> g' -> Nat (Dom g) (Dom g) (f :.: g) (Id (Dom g)) -> ((f' :.: f) :.: (g :.: g')) :~> (f' :.: g')Source
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.