License | BSD-style (see the file LICENSE) |
---|---|
Maintainer | sjoerd@w3future.com |
Stability | experimental |
Portability | non-portable |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
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
- mkAdjunctionInit :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall a. Obj d a -> d a (g :% (f :% a))) -> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b) -> Adjunction c d f g
- mkAdjunctionTerm :: (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 b. Obj c b -> c (f :% (g :% b)) b) -> 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 c d
- 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 #
(Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => Adjunction | |
|
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 #
Make an adjunction from the hom-set isomorphism.
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 #
Make an adjunction from the unit and counit.
mkAdjunctionInit :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall a. Obj d a -> d a (g :% (f :% a))) -> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b) -> Adjunction c d f g Source #
Make an adjunction from an initial universal property.
mkAdjunctionTerm :: (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 b. Obj c b -> c (f :% (g :% b)) b) -> Adjunction c d f g Source #
Make an adjunction from a terminal universal property.
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
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 #
AdjArrow :: (Category c, Category d) => Adjunction c d f g -> AdjArrow c d |
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 #