data-category 0.8.2 → 0.9

raw patch · 10 files changed

+236/−72 lines, 10 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Data/Category.hs +4/−2
• Data/Category/Adjunction.hs +12/−39
• Data/Category/Enriched.hs +14/−21
• Data/Category/Functor.hs +19/−1
• Data/Category/KanExtension.hs +157/−0
• Data/Category/Kleisli.hs +1/−1
• Data/Category/Limit.hs +6/−6
• Data/Category/RepresentableFunctor.hs +20/−0
• Data/Category/Yoneda.hs +1/−1
• data-category.cabal +2/−1

@@ -54,5 +54,7 @@    (Op a) . (Op b) = Op (b . a) -type family Kind (cat :: k -> k -> *) :: * where-  Kind (cat :: k -> k -> *) = k++-- | @Kind k@ is the kind of the objects of the category @k@.+type family Kind (k :: o -> o -> *) :: * where+  Kind (k :: o -> o -> *) = o

@@ -14,8 +14,8 @@     Adjunction(..)   , mkAdjunction   , mkAdjunctionUnits-  , mkAdjunctionUnit-  , mkAdjunctionCounit+  , mkAdjunctionInit+  , mkAdjunctionTerm    , leftAdjunct   , rightAdjunct@@ -27,14 +27,6 @@   , composeAdj   , AdjArrow(..) -  -- * Adjunctions from universal morphisms-  , initialPropAdjunction-  , terminalPropAdjunction--  -- * Universal morphisms from adjunctions-  , adjunctionInitialProp-  , adjunctionTerminalProp-   -- * Examples   , precomposeAdj   , postcomposeAdj@@ -46,7 +38,6 @@ import Data.Category.Functor import Data.Category.Product import Data.Category.NaturalTransformation-import Data.Category.RepresentableFunctor  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@@ -56,6 +47,7 @@   , rightAdjunctN :: Profunctors c d (Star g) (Costar f)   } +-- | Make an adjunction from the hom-set isomorphism. 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))@@ -63,6 +55,7 @@   -> Adjunction c d f g mkAdjunction f g l r = Adjunction f g (Nat (Costar f) (Star g) (\(Op a :**: _) -> l a)) (Nat (Star g) (Costar f) (\(_ :**: b) -> r b)) +-- | Make an adjunction from the unit and counit. 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)@@ -70,19 +63,21 @@   -> Adjunction c d f g mkAdjunctionUnits f g un coun = mkAdjunction f g (\a h -> (g % h) . un a) (\b h -> coun b . (f % h)) -mkAdjunctionUnit :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)+-- | Make an adjunction from an initial universal property.+mkAdjunctionInit :: (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 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-mkAdjunctionUnit f g un adj = mkAdjunction f g (\a h -> (g % h) . un a) adj+mkAdjunctionInit f g un adj = mkAdjunction f g (\a h -> (g % h) . un a) adj -mkAdjunctionCounit :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)+-- | Make an adjunction from a terminal 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 a. Obj c a -> Component (f :.: g) (Id c) a)+  -> (forall b. Obj c b -> c (f :% (g :% b)) b)   -> Adjunction c d f g-mkAdjunctionCounit f g adj coun = mkAdjunction f g adj (\b h -> coun b . (f % h))+mkAdjunctionTerm f g adj coun = mkAdjunction f g adj (\b h -> coun b . (f % h))  leftAdjunct :: Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b) leftAdjunct (Adjunction _ _ l _) a h = (l ! (Op a :**: tgt h)) h@@ -93,28 +88,6 @@ adjunctionUnit adj@(Adjunction f g _ _) = Nat Id (g :.: f) (\a -> leftAdjunct adj a (f % a)) adjunctionCounit :: Adjunction c d f g -> Nat c c (f :.: g) (Id c) adjunctionCounit adj@(Adjunction f g _ _) = Nat (f :.: g) Id (\b -> rightAdjunct adj b (g % b))---- Each pair (FY, unit_Y) is an initial morphism from Y to G.-adjunctionInitialProp :: Adjunction c d f g -> Obj d y -> InitialUniversal y g (f :% y)-adjunctionInitialProp adj@(Adjunction f g _ _) y = initialUniversal g (f % y) (adjunctionUnit adj ! y) (rightAdjunct adj)---- Each pair (GX, counit_X) is a terminal morphism from F to X.-adjunctionTerminalProp :: Adjunction c d f g -> Obj c x -> TerminalUniversal x f (g :% x)-adjunctionTerminalProp adj@(Adjunction f g _ _) x = terminalUniversal f (g % x) (adjunctionCounit adj ! x) (leftAdjunct adj)----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-initialPropAdjunction f g univ = mkAdjunctionUnits f g-  (universalElement . univ)-  (\a -> represent (univ (g % a)) a (g % a))--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-terminalPropAdjunction f g univ = mkAdjunctionUnits f g-  (\a -> unOp (represent (univ (f % a)) (Op a) (f % a)))-  (universalElement . univ)   idAdj :: Category k => Adjunction k k (Id k) (Id k)

@@ -9,8 +9,6 @@   , UndecidableInstances   , ScopedTypeVariables   , ConstraintKinds-  , AllowAmbiguousTypes-  , TypeApplications   #-} ----------------------------------------------------------------------------- -- |@@ -33,7 +31,7 @@  -- | An enriched category class CartesianClosed (V k) => ECategory (k :: * -> * -> *) where-  -- | The tensor product of the category V which k is enriched in+  -- | The category V which k is enriched in   type V k :: * -> * -> *    -- | The hom object in V from a to b@@ -44,13 +42,8 @@   comp :: Obj k a -> Obj k b -> Obj k c -> V k (BinaryProduct (V k) (k $ (b, c)) (k $ (a, b))) (k $ (a, c))  --- | The elements of @k@ as a functor from @V k@ to @(->)@ -type Elem k = TerminalObject (V k) :*-: (V k)-elem :: CartesianClosed (V k) => Elem k-elem = HomX_ terminalObject- -- | Arrows as elements of @k@-type Arr k a b = Elem k :% (k $ (a, b))+type Arr k a b = V k (TerminalObject (V k)) (k $ (a, b))  compArr :: ECategory k => Obj k a -> Obj k b -> Obj k c -> Arr k b c -> Arr k a b -> Arr k a c compArr a b c f g = comp a b c . (f &&& g)@@ -76,17 +69,17 @@  data (:<>:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where   (:<>:) :: (V k1 ~ V k2) => Obj k1 a1 -> Obj k2 a2 -> (:<>:) k1 k2 (a1, a2) (a1, a2)-  + -- | The enriched product category of enriched categories @c1@ and @c2@. instance (ECategory k1, ECategory k2, V k1 ~ V k2) => ECategory (k1 :<>: k2) where   type V (k1 :<>: k2) = V k1   type (k1 :<>: k2) $ ((a1, a2), (b1, b2)) = BinaryProduct (V k1) (k1 $ (a1, b1)) (k2 $ (a2, b2))   hom (a1 :<>: a2) (b1 :<>: b2) = hom a1 b1 *** hom a2 b2   id (a1 :<>: a2) = id a1 &&& id a2-  comp (a1 :<>: a2) (b1 :<>: b2) (c1 :<>: c2) = -    comp a1 b1 c1 . (proj1 bc1 bc2 . proj1 l r &&& proj1 ab1 ab2 . proj2 l r) &&& +  comp (a1 :<>: a2) (b1 :<>: b2) (c1 :<>: c2) =+    comp a1 b1 c1 . (proj1 bc1 bc2 . proj1 l r &&& proj1 ab1 ab2 . proj2 l r) &&&     comp a2 b2 c2 . (proj2 bc1 bc2 . proj1 l r &&& proj2 ab1 ab2 . proj2 l r)-    where +    where       ab1 = hom a1 b1       ab2 = hom a2 b2       bc1 = hom b1 c1@@ -209,8 +202,8 @@   type Cod (UnderlyingF f) = Underlying (ECod f)   type UnderlyingF f :% a = f :%% a   UnderlyingF f % Underlying a ab b = Underlying (f %% a) (map f a b . ab) (f %% b)-   + data EHom (k :: * -> * -> *) = EHom instance ECategory k => EFunctor (EHom k) where   type EDom (EHom k) = EOp k :<>: k@@ -259,8 +252,8 @@   end :: (VProfunctor k k t, V k ~ v) => t -> Obj v (End v t)   endCounit :: (VProfunctor k k t, V k ~ v) => t -> Obj k a -> v (End v t) (t :%% (a, a))   endFactorizer :: (VProfunctor k k t, V k ~ v) => t -> (forall a. Obj k a -> v x (t :%% (a, a))) -> v x (End v t)-   + newtype HaskEnd t = HaskEnd { getHaskEnd :: forall k a. VProfunctor k k t => t -> Obj k a -> t :%% (a, a) } type instance End (->) t = HaskEnd t instance HasEnds (->) where@@ -281,7 +274,7 @@   type FunCat a b $ (t, s) = End (V a) (t :->>: s)   hom (FArr t _) (FArr s _) = end (t ->> s)   id (FArr t _) = endFactorizer (t ->> t) (\a -> id (t %% a))-  comp (FArr t _) (FArr s _) (FArr r _) = endFactorizer (t ->> r) +  comp (FArr t _) (FArr s _) (FArr r _) = endFactorizer (t ->> r)     (\a -> comp (t %% a) (s %% a) (r %% a) . (endCounit (s ->> r) a *** endCounit (t ->> s) a))  @@ -291,10 +284,10 @@   type ECod (EndFunctor k) = Self (V k)   type EndFunctor k :%% t = End (V k) t   EndFunctor %% (FArr t _) = Self (end t)-  map EndFunctor (FArr f _) (FArr g _) = curry (end (f ->> g)) (end f) (end g) (endFactorizer g (\a -> +  map EndFunctor (FArr f _) (FArr g _) = curry (end (f ->> g)) (end f) (end g) (endFactorizer g (\a ->     let aa = EOp a :<>: a in apply (getSelf (f %% aa)) (getSelf (g %% aa)) . (endCounit (f ->> g) aa *** endCounit f a)))-     + -- d :: j -> k, w :: j -> Self (V k) type family WeigtedLimit (k :: * -> * -> *) w d :: * type Lim w d = WeigtedLimit (ECod d) w d@@ -312,14 +305,14 @@   colimitObj :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k (Colim w d)   colimit    :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHom_X k e :.: Opposite d))) (k $ (Colim w d, e))   colimitInv :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k e -> V k (k $ (Colim w d, e)) (End (V k) (w :->>: (EHom_X k e :.: Opposite d)))-   + type instance WeigtedLimit (Self v) w d = End v (w :->>: d) instance HasEnds v => HasLimits (Self v) where   limitObj w d = Self (end (w ->> d))-  limit w d (Self e) = let wed = w ->> (EHomX_ (Self e) :.: d) in curry (end wed) e (end (w ->> d)) +  limit w d (Self e) = let wed = w ->> (EHomX_ (Self e) :.: d) in curry (end wed) e (end (w ->> d))     (endFactorizer (w ->> d) (\a -> let { Self wa = w %% a; Self da = d %% a } in apply e (da ^^^ wa) . (flip wa e da . endCounit wed a *** e)))-  limitInv w d (Self e) = let wed = w ->> (EHomX_ (Self e) :.: d) in endFactorizer wed +  limitInv w d (Self e) = let wed = w ->> (EHomX_ (Self e) :.: d) in endFactorizer wed     (\a -> let { Self wa = w %% a; Self da = d %% a } in flip e wa da . (endCounit (w ->> d) a ^^^ e))  

@@ -1,4 +1,17 @@-{-# LANGUAGE PolyKinds, TypeOperators, TypeFamilies, PatternSynonyms, FlexibleContexts, FlexibleInstances, UndecidableInstances, GADTs, RankNTypes, ConstraintKinds, NoImplicitPrelude #-}+{-# LANGUAGE+    GADTs+  , PolyKinds+  , RankNTypes+  , ConstraintKinds+  , NoImplicitPrelude+  , TypeOperators+  , TypeFamilies+  , PatternSynonyms+  , FlexibleContexts+  , FlexibleInstances+  , UndecidableInstances+  , GeneralizedNewtypeDeriving+  #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Functor@@ -24,6 +37,7 @@   , Opposite(..)   , OpOp(..)   , OpOpInv(..)+  , Any(..)    -- *** Related to the product category   , Proj1(..)@@ -155,6 +169,10 @@   type OpOpInv k :% a = a    OpOpInv % f = Op (Op f)+++-- | A functor wrapper in case of conflicting family instance declarations+newtype Any f = Any f deriving Functor   data Proj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj1

@@ -0,0 +1,157 @@+{-# LANGUAGE+    FlexibleInstances+  , GADTs+  , MultiParamTypeClasses+  , RankNTypes+  , TypeOperators+  , TypeFamilies+  , UndecidableInstances+  , NoImplicitPrelude+  #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.KanExtension+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category.KanExtension where++import Data.Category+import Data.Category.Functor+import Data.Category.NaturalTransformation+import Data.Category.Adjunction+import Data.Category.Limit+import Data.Category.Unit++-- | The right Kan extension of a functor @p@ for functors @f@ with codomain @k@.+type family RanFam (p :: *) (k :: * -> * -> *) (f :: *) :: *++type Ran p f = RanFam p (Cod f) f++-- | An instance of @HasRightKan p k@ says there are right Kan extensions for all functors with codomain @k@.+class (Functor p, Category k) => HasRightKan p k where+  -- | 'ran' gives the defining natural transformation of the right Kan extension of @f@ along @p@.+  ran           :: p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k (RanFam p k f :.: p) f+  -- | 'ranFactorizer' shows that this extension is universal.+  ranFactorizer :: Nat (Dom p) k (h :.: p) f -> Nat (Cod p) k h (RanFam p k f)++ranF :: HasRightKan p k => p -> Obj (Nat (Dom p) k) f -> Obj (Nat (Cod p) k) (RanFam p k f)+ranF p f = ranF' (ran p f)++ranF' :: Nat (Dom p) k (RanFam p k f :.: p) f -> Obj (Nat (Cod p) k) (RanFam p k f)+ranF' (Nat (r :.: _) _ _) = natId r++data RanFunctor (p :: *) (k :: * -> * -> *) = RanFunctor p+instance HasRightKan p k => Functor (RanFunctor p k) where+  type Dom (RanFunctor p k) = Nat (Dom p) k+  type Cod (RanFunctor p k) = Nat (Cod p) k+  type RanFunctor p k :% f = RanFam p k f++  RanFunctor p % n = ranFactorizer (n . ran p (src n))++-- | The right Kan extension along @p@ is right adjoint to precomposition with @p@.+ranAdj :: forall p k. HasRightKan p k => p -> Adjunction (Nat (Dom p) k) (Nat (Cod p) k) (Precompose p k) (RanFunctor p k)+ranAdj p = mkAdjunctionTerm (Precompose p) (RanFunctor p) (\_ -> ranFactorizer) (ran p)+++-- | The left Kan extension of a functor @p@ for functors @f@ with codomain @k@.+type family LanFam (p :: *) (k :: * -> * -> *) (f :: *) :: *++type Lan p f = LanFam p (Cod f) f++-- | An instance of @HasLeftKan p k@ says there are left Kan extensions for all functors with codomain @k@.+class (Functor p, Category k) => HasLeftKan p k where+  -- | 'lan' gives the defining natural transformation of the left Kan extension of @f@ along @p@.+  lan           :: p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k f (LanFam p k f :.: p)+  -- | 'lanFactorizer' shows that this extension is universal.+  lanFactorizer :: Nat (Dom p) k f (h :.: p) -> Nat (Cod p) k (LanFam p k f) h++lanF :: HasLeftKan p k => p -> Obj (Nat (Dom p) k) f -> Obj (Nat (Cod p) k) (LanFam p k f)+lanF p f = lanF' (lan p f)++lanF' :: Nat (Dom p) k f (LanFam p k f :.: p) -> Obj (Nat (Cod p) k) (LanFam p k f)+lanF' (Nat _ (r :.: _) _) = natId r++data LanFunctor (p :: *) (k :: * -> * -> *) = LanFunctor p+instance HasLeftKan p k => Functor (LanFunctor p k) where+  type Dom (LanFunctor p k) = Nat (Dom p) k+  type Cod (LanFunctor p k) = Nat (Cod p) k+  type LanFunctor p k :% f = LanFam p k f++  LanFunctor p % n = lanFactorizer (lan p (tgt n) . n)++-- | The left Kan extension along @p@ is left adjoint to precomposition with @p@.+lanAdj :: forall p k. HasLeftKan p k => p -> Adjunction (Nat (Cod p) k) (Nat (Dom p) k) (LanFunctor p k) (Precompose p k)+lanAdj p = mkAdjunctionInit (LanFunctor p) (Precompose p) (lan p) (\_ -> lanFactorizer)+++type instance RanFam (Const j Unit ()) k f = Const Unit k (LimitFam j k f)+-- | The right Kan extension of @f@ along a functor to the unit category is the limit of @f@.+instance HasLimits j k => HasRightKan (Const j Unit ()) k where+  ran p f@Nat{} = let cone = limit f in Nat (Const (coneVertex cone) :.: p) (srcF f) (cone !)+  ranFactorizer n@(Nat (h :.: _) f _) = let fact = limitFactorizer (constPrecompIn n) in Nat h (Const (tgt fact)) (\Unit -> fact)++type instance LanFam (Const j Unit ()) k f = Const Unit k (ColimitFam j k f)+-- | The left Kan extension of @f@ along a functor to the unit category is the colimit of @f@.+instance HasColimits j k => HasLeftKan (Const j Unit ()) k where+  lan p f@Nat{} = let cocone = colimit f in Nat (srcF f) (Const (coconeVertex cocone) :.: p) (cocone !)+  lanFactorizer n@(Nat f (h :.: _) _) = let fact = colimitFactorizer (constPrecompOut n) in Nat (Const (src fact)) h (\Unit -> fact)+++type instance RanFam (Id j) k f = f+-- | Ran id = id+instance (Category j, Category k) => HasRightKan (Id j) k where+  ran Id (Nat f _ _) = idPrecomp f+  ranFactorizer n@(Nat (h :.: Id) _ _) = n . idPrecompInv h++type instance LanFam (Id j) k f = f+-- | Lan id = id+instance (Category j, Category k) => HasLeftKan (Id j) k where+  lan Id (Nat f _ _) = idPrecompInv f+  lanFactorizer n@(Nat _ (h :.: Id) _) = idPrecomp h . n+++type instance RanFam (q :.: p) k f = RanFam q k (RanFam p k f)+-- | Ran (q . p) = Ran q . Ran p+instance (HasRightKan q k, HasRightKan p k) => HasRightKan (q :.: p) k where+  ran (q :.: p) f = let ranp = ran p f in case ran q (ranF' ranp) of+      ranq@(Nat (r :.: _) _ _) -> ranp . (ranq `o` natId p) . compAssocInv r q p+  ranFactorizer n@(Nat (h :.: (q :.: p)) _ _) = ranFactorizer (ranFactorizer (n . compAssoc h q p))++type instance LanFam (q :.: p) k f = LanFam q k (LanFam p k f)+-- | Lan (q . p) = Lan q . Lan p+instance (HasLeftKan q k, HasLeftKan p k) => HasLeftKan (q :.: p) k where+  lan (q :.: p) f = let lanp = lan p f in case lan q (lanF' lanp) of+      lanq@(Nat _ (l :.: _) _) -> compAssoc l q p . (lanq `o` natId p) . lanp+  lanFactorizer n@(Nat _ (h :.: (q :.: p)) _) = lanFactorizer (lanFactorizer (compAssocInv h q p . n))+++newtype RanHask p f a = RanHask (forall c. Obj (Dom p) c -> Cod p a (p :% c) -> f :% c)+data RanHaskF p f = RanHaskF+instance Functor p => Functor (RanHaskF p f) where+  type Dom (RanHaskF p f) = Cod p+  type Cod (RanHaskF p f) = (->)+  type RanHaskF p f :% a = RanHask p f a+  RanHaskF % ab = \(RanHask r) -> RanHask (\c bpc -> r c (bpc . ab))++type instance RanFam (Any p) (->) f = RanHaskF p f+instance Functor p => HasRightKan (Any p) (->) where+  ran (Any p) (Nat f _ _) = Nat (RanHaskF :.: Any p) f (\z (RanHask r) -> r z (p % z))+  ranFactorizer (Nat (h :.: Any p) f n) = Nat h RanHaskF (\z hz -> RanHask (\c zpc -> n c ((h % zpc) hz)))++data LanHask p f a where+  LanHask :: Obj (Dom p) c -> Cod p (p :% c) a -> f :% c -> LanHask p f a+data LanHaskF p f = LanHaskF+instance Functor p => Functor (LanHaskF p f) where+  type Dom (LanHaskF p f) = Cod p+  type Cod (LanHaskF p f) = (->)+  type LanHaskF p f :% a = LanHask p f a+  LanHaskF % ab = \(LanHask c pca fc) -> LanHask c (ab . pca) fc++type instance LanFam (Any p) (->) f = LanHaskF p f+instance Functor p => HasLeftKan (Any p) (->) where+  lan (Any p) (Nat f _ _) = Nat f (LanHaskF :.: Any p) (\z fz -> LanHask z (p % z) fz)+  lanFactorizer (Nat f (h :.: Any p) n) = Nat LanHaskF h (\z (LanHask c pcz fc) -> (h % pcz) (n c fc))

@@ -52,4 +52,4 @@  kleisliAdj :: (Functor m, Dom m ~ k, Cod m ~ k)   => Monad m -> A.Adjunction (Kleisli m) k (KleisliFree m) (KleisliForget m)-kleisliAdj m = A.mkAdjunctionUnit (KleisliFree m) KleisliForget (unit m !) (\(Kleisli _ x _) f -> Kleisli m x f)+kleisliAdj m = A.mkAdjunctionInit (KleisliFree m) KleisliForget (unit m !) (\(Kleisli _ x _) f -> Kleisli m x f)

@@ -136,7 +136,7 @@   --   by returning the morphism between the vertices of the cones.   limitFactorizer :: Cone j k f n -> k n (LimitFam j k f) -data LimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = LimitFunctor+data LimitFunctor (j :: * -> * -> *) (k :: * -> * -> *) = LimitFunctor -- | If every diagram of type @j@ has a limit in @k@ there exists a limit functor. --   It can be seen as a generalisation of @(***)@. instance HasLimits j k => Functor (LimitFunctor j k) where@@ -148,7 +148,7 @@  -- | The limit functor is right adjoint to the diagonal functor. limitAdj :: forall j k. HasLimits j k => Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k)-limitAdj = mkAdjunctionCounit Diag LimitFunctor (\_ -> limitFactorizer) limit+limitAdj = mkAdjunctionTerm Diag LimitFunctor (\_ -> limitFactorizer) limit  adjLimit :: Category k => Adjunction (Nat j k) k (Diag j k) r -> Obj (Nat j k) f -> Cone j k f (r :% f) adjLimit adj f = adjunctionCounit adj ! f@@ -195,7 +195,7 @@   --   by returning the morphism between the vertices of the cones.   colimitFactorizer :: Cocone j k f n -> k (ColimitFam j k f) n -data ColimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = ColimitFunctor+data ColimitFunctor (j :: * -> * -> *) (k :: * -> * -> *) = ColimitFunctor -- | If every diagram of type @j@ has a colimit in @k@ there exists a colimit functor. --   It can be seen as a generalisation of @(+++)@. instance HasColimits j k => Functor (ColimitFunctor j k) where@@ -207,7 +207,7 @@  -- | The colimit functor is left adjoint to the diagonal functor. colimitAdj :: forall j k. HasColimits j k => Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)-colimitAdj = mkAdjunctionUnit ColimitFunctor Diag colimit (\_ -> colimitFactorizer)+colimitAdj = mkAdjunctionInit ColimitFunctor Diag colimit (\_ -> colimitFactorizer)  adjColimit :: Category k => Adjunction k (Nat j k) l (Diag j k) -> Obj (Nat j k) f -> Cocone j k f (l :% f) adjColimit adj f = adjunctionUnit adj ! f@@ -482,7 +482,7 @@  -- | A specialisation of the limit adjunction to products. prodAdj :: HasBinaryProducts k => Adjunction (k :**: k) k (DiagProd k) (ProductFunctor k)-prodAdj = mkAdjunctionUnits DiagProd ProductFunctor (\x -> x &&& x) (\(l :**: r) -> proj1 l r :**: proj2 l r)+prodAdj = mkAdjunctionTerm DiagProd ProductFunctor (\_ (l :**: r) -> l &&& r) (\(l :**: r) -> proj1 l r :**: proj2 l r)  data p :*: q where   (:*:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryProducts k) => p -> q -> p :*: q@@ -608,7 +608,7 @@  -- | A specialisation of the colimit adjunction to coproducts. coprodAdj :: HasBinaryCoproducts k => Adjunction k (k :**: k) (CoproductFunctor k) (DiagProd k)-coprodAdj = mkAdjunctionUnits CoproductFunctor DiagProd (\(l :**: r) -> inj1 l r :**: inj2 l r) (\x -> x ||| x)+coprodAdj = mkAdjunctionInit CoproductFunctor DiagProd (\(l :**: r) -> inj1 l r :**: inj2 l r) (\_ (l :**: r) -> l ||| r)  data p :+: q where   (:+:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryCoproducts k) => p -> q -> p :+: q

@@ -12,6 +12,8 @@  import Data.Category import Data.Category.Functor+import Data.Category.NaturalTransformation+import Data.Category.Adjunction   data Representable f repObj = Representable@@ -69,3 +71,21 @@   , represent          = \(Op y) f -> Op (factorizer y f)   , universalElement   = mor   }+++-- | For an adjunction F -| G, each pair (FY, unit_Y) is an initial morphism from Y to G.+adjunctionInitialProp :: Adjunction c d f g -> Obj d y -> InitialUniversal y g (f :% y)+adjunctionInitialProp adj@(Adjunction f g _ _) y = initialUniversal g (f % y) (adjunctionUnit adj ! y) (rightAdjunct adj)++-- | For an adjunction F -| G, each pair (GX, counit_X) is a terminal morphism from F to X.+adjunctionTerminalProp :: Adjunction c d f g -> Obj c x -> TerminalUniversal x f (g :% x)+adjunctionTerminalProp adj@(Adjunction f g _ _) x = terminalUniversal f (g % x) (adjunctionCounit adj ! x) (leftAdjunct adj)+++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. InitialUniversal y g (f :% y)) -> Adjunction c d f g+initialPropAdjunction f g univ = mkAdjunctionInit f g (\_ -> universalElement univ) (represent univ)++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. TerminalUniversal x f (g :% x)) -> Adjunction c d f g+terminalPropAdjunction f g univ = mkAdjunctionTerm f g ((unOp .) . represent univ . Op) (\_ -> universalElement univ)

@@ -51,6 +51,6 @@   M1 % n = n ! Op haskUnit  haskIsTotal :: Adjunction (->) (Nat (Op (->)) (->)) M1 (YonedaEmbedding (->))-haskIsTotal = mkAdjunctionUnit M1 YonedaEmbedding+haskIsTotal = mkAdjunctionInit M1 YonedaEmbedding   (\(Nat f _ _) -> Nat f (Hom_X (f % Op haskUnit)) (\_ fz z -> (f % Op (\() -> z)) fz))   (\_ n@(Nat f _ _) fu -> (n ! Op haskUnit) fu ())

@@ -1,5 +1,5 @@ name:                data-category-version:             0.8.2+version:             0.9 synopsis:            Category theory  description:         Data-category is a collection of categories, and some categorical constructions on them.@@ -38,6 +38,7 @@     Data.Category.RepresentableFunctor,     Data.Category.Adjunction,     Data.Category.Limit,+    Data.Category.KanExtension,     Data.Category.Monoidal,     Data.Category.CartesianClosed,     Data.Category.Enriched,