data-category-0.10: Category theory

Description

Synopsis

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 FieldsleftAdjoint :: 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 #

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 #

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