data-category 0.6.2 → 0.7

raw patch · 10 files changed

+206/−105 lines, 10 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Data/Category/Adjunction.hs +35/−22
• Data/Category/CartesianClosed.hs +1/−1
• Data/Category/Dialg.hs +1/−1
• Data/Category/Functor.hs +46/−30
• Data/Category/Kleisli.hs +1/−1
• Data/Category/Limit.hs +78/−21
• Data/Category/Monoidal.hs +25/−3
• Data/Category/NNO.hs +1/−2
• Data/Category/NaturalTransformation.hs +17/−23
• data-category.cabal +1/−1

@@ -13,9 +13,12 @@   -- * Adjunctions     Adjunction(..)   , mkAdjunction+  , mkAdjunctionUnits    , leftAdjunct   , rightAdjunct+  , adjunctionUnit+  , adjunctionCounit    -- * Adjunctions as a category   , idAdj@@ -39,6 +42,7 @@  import Data.Category import Data.Category.Functor+import Data.Category.Product import Data.Category.NaturalTransformation import Data.Category.RepresentableFunctor @@ -46,54 +50,63 @@   => Adjunction   { leftAdjoint  :: f   , rightAdjoint :: g-  , unit         :: Nat d d (Id d) (g :.: f)-  , counit       :: Nat c c (f :.: g) (Id c)+  , 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+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))++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-mkAdjunction f g un coun = Adjunction f g (Nat Id (g :.: f) un) (Nat (f :.: g) Id coun)+mkAdjunctionUnits f g un coun = mkAdjunction f g (\a h -> (g % h) . un a) (\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 _ g un _) i h = (g % h) . (un ! i)+leftAdjunct (Adjunction _ _ l _) a h = (l ! (Op a :**: tgt h)) h rightAdjunct :: Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b-rightAdjunct (Adjunction f _ _ coun) i h = (coun ! i) . (f % h)-+rightAdjunct (Adjunction _ _ _ r) b h = (r ! (Op (src h) :**: b)) h +adjunctionUnit :: Adjunction c d f g -> Nat d d (Id d) (g :.: f)+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 un _) y = initialUniversal g (f % y) (un ! y) (rightAdjunct adj)+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 _ coun) x = terminalUniversal f (g % x) (coun ! x) (leftAdjunct adj)+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 = mkAdjunction 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 = mkAdjunction 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)-idAdj = mkAdjunction Id Id (\x -> x) (\x -> x)+idAdj = mkAdjunction Id Id (\_ f -> f) (\_ f -> f)  composeAdj :: Adjunction d e f g -> Adjunction c d f' g' -> Adjunction c e (f' :.: f) (g :.: g')-composeAdj (Adjunction f g u c) (Adjunction f' g' u' c') = Adjunction (f' :.: f) (g :.: g')-  (compAssoc (g :.: g') f' f . precompose f % (compAssocInv g g' f' . postcompose g % u' . idPrecompInv g) . u)-  (c' . precompose g' % (idPrecomp f' . postcompose f' % c . compAssoc f' f g) . compAssocInv (f' :.: f) g g')+composeAdj l@(Adjunction f g _ _) r@(Adjunction f' g' _ _) = mkAdjunction (f' :.: f) (g :.: g')+  (\a -> leftAdjunct l a . leftAdjunct r (f % a)) (\b -> rightAdjunct r b . rightAdjunct l (g' % b))   data AdjArrow c d where@@ -110,22 +123,22 @@   precomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat c e) (Nat d e) (Precompose g e) (Precompose f e)-precomposeAdj (Adjunction f g un coun) = mkAdjunction+precomposeAdj adj@(Adjunction f g _ _) = mkAdjunctionUnits   (precompose g)   (precompose f)-  (\nh@(Nat h _ _) -> compAssocInv h g f . (nh `o` un) . idPrecompInv h)-  (\nh@(Nat h _ _) -> idPrecomp h . (nh `o` coun) . compAssoc h f g)+  (\nh@(Nat h _ _) -> compAssocInv h g f . (nh `o` adjunctionUnit adj) . idPrecompInv h)+  (\nh@(Nat h _ _) -> idPrecomp h . (nh `o` adjunctionCounit adj) . compAssoc h f g)  postcomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat e c) (Nat e d) (Postcompose f e) (Postcompose g e)-postcomposeAdj (Adjunction f g un coun) = mkAdjunction+postcomposeAdj adj@(Adjunction f g _ _) = mkAdjunctionUnits   (postcompose f)   (postcompose g)-  (\nh@(Nat h _ _) -> compAssoc g f h . (un `o` nh) . idPostcompInv h)-  (\nh@(Nat h _ _) -> idPostcomp h . (coun `o` nh) . compAssocInv f g h)+  (\nh@(Nat h _ _) -> compAssoc g f h . (adjunctionUnit adj `o` nh) . idPostcompInv h)+  (\nh@(Nat h _ _) -> idPostcomp h . (adjunctionCounit adj `o` nh) . compAssocInv f g h)  contAdj :: Adjunction (Op (->)) (->) (Opposite ((->) :-*: r) :.: OpOpInv (->)) ((->) :-*: r) contAdj = mkAdjunction   (Opposite (hom_X (\x -> x)) :.: OpOpInv)   (hom_X (\x -> x))-  (\_ x f -> f x)-  (\_ -> Op (\x f -> f x))+  (\_ -> \(Op f) -> \b a -> f a b)+  (\_ -> \f -> Op (\b a -> f a b))

@@ -91,7 +91,7 @@          -> Adjunction k k               (ProductFunctor k :.: Tuple2 k k y)               (ExpFunctor k :.: Tuple1 (Op k) k y)-curryAdj y = mkAdjunction (ProductFunctor :.: tuple2 y) (ExpFunctor :.: Tuple1 (Op y)) (tuple y) (apply y)+curryAdj y = mkAdjunctionUnits (ProductFunctor :.: tuple2 y) (ExpFunctor :.: tuple1 (Op y)) (tuple y) (apply y)  -- | From the adjunction between the product functor and the exponential functor we get the curry and uncurry functions, --   generalized to any cartesian closed category.

@@ -106,6 +106,6 @@  eilenbergMooreAdj :: (Functor m, Dom m ~ k, Cod m ~ k)   => Monad m -> A.Adjunction (Alg m) k (FreeAlg m) (ForgetAlg m)-eilenbergMooreAdj m = A.mkAdjunction (FreeAlg m) ForgetAlg+eilenbergMooreAdj m = A.mkAdjunctionUnits (FreeAlg m) ForgetAlg   (\x -> unit m ! x)   (\(DialgA (Dialgebra _ h) _ _) -> DialgA (Dialgebra (src h) (monadFunctor m % h)) (Dialgebra (tgt h) h) h)

@@ -30,19 +30,20 @@   , Proj2(..)   , (:***:)(..)   , DiagProd(..)-  , Tuple1(..)-  , Swap, swap+  , Tuple1, tuple1   , Tuple2, tuple2+  , Swap, swap    -- *** Hom functors   , Hom(..)-  , (:*-:)-  , homX_-  , (:-*:)-  , hom_X+  , (:*-:), homX_+  , (:-*:), hom_X+  , HomF, homF+  , Star, star+  , Costar, costar  ) where-  + import Data.Category import Data.Category.Product @@ -53,7 +54,7 @@  -- | Functors map objects and arrows. class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where-  +   -- | The domain, or source category, of the functor.   type Dom ftag :: * -> * -> *   -- | The codomain, or target category, of the functor.@@ -61,7 +62,7 @@    -- | @:%@ maps objects.   type ftag :% a :: *-  +   -- | @%@ maps arrows.   (%)  :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b) @@ -78,10 +79,10 @@  -- | @Cat@ is the category with categories as objects and funtors as arrows. instance Category Cat where-  +   src (CatA _)      = CatA Id   tgt (CatA _)      = CatA Id-  +   CatA f1 . CatA f2 = CatA (f1 :.: f2)  @@ -107,9 +108,9 @@   type (g :.: h) :% a = g :% (h :% a)    (g :.: h) % f = g % (h % f)-    + data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where   Const :: Obj c2 x -> Const c1 c2 x @@ -118,7 +119,7 @@   type Dom (Const c1 c2 x) = c1   type Cod (Const c1 c2 x) = c2   type Const c1 c2 x :% a = x-  +   Const x % _ = x  -- | The constant functor with the same domain and codomain as f.@@ -133,7 +134,7 @@   type Dom (Opposite f) = Op (Dom f)   type Cod (Opposite f) = Op (Cod f)   type Opposite f :% a = f :% a-  +   Opposite f % Op a = Op (f % a)  @@ -144,7 +145,7 @@   type Dom (OpOp k) = Op (Op k)   type Cod (OpOp k) = k   type OpOp k :% a = a-  +   OpOp % Op (Op f) = f  @@ -155,7 +156,7 @@   type Dom (OpOpInv k) = k   type Cod (OpOpInv k) = Op (Op k)   type OpOpInv k :% a = a-  +   OpOpInv % f = Op (Op f)  @@ -166,7 +167,7 @@   type Dom (Proj1 c1 c2) = c1 :**: c2   type Cod (Proj1 c1 c2) = c1   type Proj1 c1 c2 :% (a1, a2) = a1-  +   Proj1 % (f1 :**: _) = f1  @@ -177,7 +178,7 @@   type Dom (Proj2 c1 c2) = c1 :**: c2   type Cod (Proj2 c1 c2) = c2   type Proj2 c1 c2 :% (a1, a2) = a2-  +   Proj2 % (_ :**: f2) = f2  @@ -188,7 +189,7 @@   type Dom (f1 :***: f2) = Dom f1 :**: Dom f2   type Cod (f1 :***: f2) = Cod f1 :**: Cod f2   type (f1 :***: f2) :% (a1, a2) = (f1 :% a1, f2 :% a2)-  +   (g1 :***: g2) % (f1 :**: f2) = (g1 % f1) :**: (g2 % f2)  @@ -199,20 +200,22 @@   type Dom (DiagProd k) = k   type Cod (DiagProd k) = k :**: k   type DiagProd k :% a = (a, a)-  +   DiagProd % f = f :**: f  -data Tuple1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Tuple1 (Obj c1 a)+type Tuple1 c1 c2 a = (Const c2 c1 a :***: Id c2) :.: DiagProd c2  -- | 'Tuple1' tuples with a fixed object on the left.-instance (Category c1, Category c2) => Functor (Tuple1 c1 c2 a1) where-  type Dom (Tuple1 c1 c2 a1) = c2-  type Cod (Tuple1 c1 c2 a1) = c1 :**: c2-  type Tuple1 c1 c2 a1 :% a2 = (a1, a2)-  -  Tuple1 a % f = a :**: f+tuple1 :: (Category c1, Category c2) => Obj c1 a -> Tuple1 c1 c2 a+tuple1 a = (Const a :***: Id) :.: DiagProd +-- type Tuple2 c1 c2 a = (Id c1 :***: Const c1 c2 a) :.: DiagProd c1+--+-- -- | 'Tuple2' tuples with a fixed object on the right.+-- tuple2 :: (Category c1, Category c2) => Obj c2 a -> Tuple2 c1 c2 a+-- tuple2 a = (Id :***: Const a) :.: DiagProd+ type Swap (c1 :: * -> * -> *) (c2 :: * -> * -> *) = (Proj2 c1 c2 :***: Proj1 c1 c2) :.: DiagProd (c1 :**: c2) -- | 'swap' swaps the 2 categories of the product of categories. swap :: (Category c1, Category c2) => Swap c1 c2@@ -221,7 +224,7 @@ type Tuple2 c1 c2 a = Swap c2 c1 :.: Tuple1 c2 c1 a -- | 'Tuple2' tuples with a fixed object on the right. tuple2 :: (Category c1, Category c2) => Obj c2 a -> Tuple2 c1 c2 a-tuple2 a = swap :.: Tuple1 a+tuple2 a = swap :.: tuple1 a   @@ -232,16 +235,29 @@   type Dom (Hom k) = Op k :**: k   type Cod (Hom k) = (->)   type (Hom k) :% (a1, a2) = k a1 a2-  +   Hom % (Op f1 :**: f2) = \g -> f2 . g . f1   type x :*-: k = Hom k :.: Tuple1 (Op k) k x -- | The covariant functor Hom(X,--) homX_ :: Category k => Obj k x -> x :*-: k-homX_ x = Hom :.: Tuple1 (Op x)+homX_ x = Hom :.: tuple1 (Op x)  type k :-*: x = Hom k :.: Tuple2 (Op k) k x -- | The contravariant functor Hom(--,X) hom_X :: Category k => Obj k x -> k :-*: x hom_X x = Hom :.: tuple2 x+++type HomF f g = Hom (Cod f) :.: (Opposite f :***: g)+homF :: (Functor f, Functor g, Cod f ~ Cod g) => f -> g -> HomF f g+homF f g = Hom :.: (Opposite f :***: g)++type Star f = HomF (Id (Cod f)) f+star :: Functor f => f -> Star f+star f = homF Id f++type Costar f = HomF f (Id (Cod f))+costar :: Functor f => f -> Costar f+costar f = homF f Id

@@ -52,6 +52,6 @@  kleisliAdj :: (Functor m, Dom m ~ k, Cod m ~ k)   => Monad m -> A.Adjunction (Kleisli m) k (KleisliAdjF m) (KleisliAdjG m)-kleisliAdj m = A.mkAdjunction (KleisliAdjF m) (KleisliAdjG m)+kleisliAdj m = A.mkAdjunctionUnits (KleisliAdjF m) (KleisliAdjG m)   (\x -> unit m ! x)   (\(Kleisli _ x _) -> Kleisli m x (monadFunctor m % x))

@@ -39,6 +39,8 @@   , HasLimits(..)   , LimitFunctor(..)   , limitAdj+  , rightAdjointPreservesLimits+  , rightAdjointPreservesLimitsInv    -- * Colimits   , ColimitFam@@ -46,6 +48,8 @@   , HasColimits(..)   , ColimitFunctor(..)   , colimitAdj+  , leftAdjointPreservesColimits+  , leftAdjointPreservesColimitsInv    -- ** Limits of type Void   , HasTerminalObject(..)@@ -138,10 +142,33 @@  -- | 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 = mkAdjunction diag LimitFunctor (\a -> limitFactorizer (diag % a) (diag % a)) (\f @ Nat{} -> limit f)+limitAdj = mkAdjunctionUnits diag LimitFunctor (\a -> limitFactorizer (diag % a) (diag % a)) (\f @ Nat{} -> limit f)   where diag = Diag :: Diag j k -- Forces the type of all Diags to be the same. -+-- Cone (g :.: t) (Limit (g :.: t))+-- Obj j z -> d (Limit (g :.: t)) ((g :.: t) :% z)+-- Obj j z -> d (f :% Limit (g :.: t)) (t :% z)+-- Cone t (f :% Limit (g :.: t))+-- d (f :% Limit (g :.: t)) (Limit t)+-- d (Limit (g :.: t)) (g :% Limit t)+rightAdjointPreservesLimits+  :: (HasLimits j c, HasLimits j d) +  => Adjunction c d f g -> Obj (Nat j c) t -> d (Limit (g :.: t)) (g :% Limit t)+rightAdjointPreservesLimits adj@(Adjunction f g _ _) (Nat t _ _) = +  leftAdjunct adj x (limitFactorizer (natId t) cone)+    where+      l = limit (natId (g :.: t))+      x = coneVertex l+      -- cone :: Cone t (f :% Limit (g :.: t))+      cone = Nat (Const (f % x)) t (\z -> rightAdjunct adj (t % z) (l ! z))+      +-- Cone t (Limit t)+-- Cone (g :.: t) (g :% Limit t)+-- d (g :% Limit t) (Limit (g :.: t))+rightAdjointPreservesLimitsInv+  :: (HasLimits j c, HasLimits j d)+  => Obj (Nat c d) g -> Obj (Nat j c) t -> d (g :% Limit t) (Limit (g :.: t))+rightAdjointPreservesLimitsInv g@Nat{} t@Nat{} = limitFactorizer (g `o` t) (constPrecompIn (g `o` limit t))  -- | Colimits in a category @k@ by means of a diagram of type @j@, which is a functor from @j@ to @k@. type family ColimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *@@ -168,11 +195,26 @@  -- | 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 = mkAdjunction ColimitFunctor diag (\f @ Nat{} -> colimit f) (\a -> colimitFactorizer (diag % a) (diag % a))+colimitAdj = mkAdjunctionUnits ColimitFunctor diag (\f @ Nat{} -> colimit f) (\a -> colimitFactorizer (diag % a) (diag % a))   where diag = Diag :: Diag j k -- Forces the type of all Diags to be the same.  +leftAdjointPreservesColimits+  :: (HasColimits j c, HasColimits j d) +  => Adjunction c d f g -> Obj (Nat j d) t -> c (f :% Colimit t) (Colimit (f :.: t))+leftAdjointPreservesColimits adj@(Adjunction f g _ _) (Nat t _ _) = +  rightAdjunct adj x (colimitFactorizer (natId t) cocone)+    where+      l = colimit (natId (f :.: t))+      x = coconeVertex l+      cocone = Nat t (Const (g % x)) (\z -> leftAdjunct adj (t % z) (l ! z)) +leftAdjointPreservesColimitsInv+  :: (HasColimits j c, HasColimits j d) +  => Obj (Nat d c) f -> Obj (Nat j d) t -> c (Colimit (f :.: t)) (f :% Colimit t)+leftAdjointPreservesColimitsInv f@Nat{} t@Nat{} = colimitFactorizer (f `o` t) (constPrecompOut (f `o` colimit t))++ class Category k => HasTerminalObject k where    type TerminalObject k :: *@@ -317,9 +359,9 @@   proj1 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) x   proj2 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) y -  (&&&) :: (k a x) -> (k a y) -> (k a (BinaryProduct k x y))+  (&&&) :: k a x -> k a y -> k a (BinaryProduct k x y) -  (***) :: (k a1 b1) -> (k a2 b2) -> (k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2))+  (***) :: k a1 b1 -> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)   l *** r = (l . proj1 (src l) (src r)) &&& (r . proj2 (src l) (src r))  @@ -333,20 +375,20 @@   limit = limit'     where       limit' :: forall f. Obj (Nat (i :++: j) k) f -> Cone f (Limit f)-      limit' l@Nat{} = Nat (Const (x *** y)) (srcF l) (\z -> unCom (h z))+      limit' l@Nat{} = Nat (Const (x *** y)) (srcF l) h         where           x = coneVertex lim1           y = coneVertex lim2           lim1 = limit (l `o` natId Inj1)           lim2 = limit (l `o` natId Inj2)-          h :: Obj (i :++: j) z -> Com (ConstF f (LimitFam (i :++: j) k f)) f z-          h (I1 n) = Com (lim1 ! n . proj1 x y)-          h (I2 n) = Com (lim2 ! n . proj2 x y)+          h :: Obj (i :++: j) z -> Component (ConstF f (LimitFam (i :++: j) k f)) f z+          h (I1 n) = lim1 ! n . proj1 x y+          h (I2 n) = lim2 ! n . proj2 x y    limitFactorizer l@Nat{} c =-    limitFactorizer (l `o` natId Inj1) ((c `o` natId Inj1) . constPostcompInv (srcF c) Inj1)+    limitFactorizer (l `o` natId Inj1) (constPostcompIn (c `o` natId Inj1))     &&&-    limitFactorizer (l `o` natId Inj2) ((c `o` natId Inj2) . constPostcompInv (srcF c) Inj2)+    limitFactorizer (l `o` natId Inj2) (constPostcompIn (c `o` natId Inj2))   -- | The tuple is the binary product in @Hask@.@@ -423,7 +465,7 @@  -- | A specialisation of the limit adjunction to products. prodAdj :: HasBinaryProducts k => Adjunction (k :**: k) k (DiagProd k) (ProductFunctor k)-prodAdj = mkAdjunction DiagProd ProductFunctor (\x -> x &&& x) (\(l :**: r) -> proj1 l r :**: proj2 l r)+prodAdj = mkAdjunctionUnits DiagProd ProductFunctor (\x -> x &&& x) (\(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@@ -453,9 +495,9 @@   inj1 :: Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)   inj2 :: Obj k x -> Obj k y -> k y (BinaryCoproduct k x y) -  (|||) :: (k x a) -> (k y a) -> (k (BinaryCoproduct k x y) a)+  (|||) :: k x a -> k y a -> k (BinaryCoproduct k x y) a -  (+++) :: (k a1 b1) -> (k a2 b2) -> (k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2))+  (+++) :: k a1 b1 -> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)   l +++ r = (inj1 (tgt l) (tgt r) . l) ||| (inj2 (tgt l) (tgt r) . r)  @@ -469,20 +511,20 @@   colimit = colimit'     where       colimit' :: forall f. Obj (Nat (i :++: j) k) f -> Cocone f (Colimit f)-      colimit' l@Nat{} = Nat (srcF l) (Const (x +++ y)) (\z -> unCom (h z))+      colimit' l@Nat{} = Nat (srcF l) (Const (x +++ y)) h         where           x = coconeVertex col1           y = coconeVertex col2           col1 = colimit (l `o` natId Inj1)           col2 = colimit (l `o` natId Inj2)-          h :: Obj (i :++: j) z -> Com f (ConstF f (ColimitFam (i :++: j) k f)) z-          h (I1 n) = Com (inj1 x y . col1 ! n)-          h (I2 n) = Com (inj2 x y . col2 ! n)+          h :: Obj (i :++: j) z -> Component f (ConstF f (ColimitFam (i :++: j) k f)) z+          h (I1 n) = inj1 x y . col1 ! n+          h (I2 n) = inj2 x y . col2 ! n    colimitFactorizer l@Nat{} c =-    colimitFactorizer (l `o` natId Inj1) (constPostcomp (tgtF c) Inj1 . (c `o` natId Inj1))+    colimitFactorizer (l `o` natId Inj1) (constPostcompOut (c `o` natId Inj1))     |||-    colimitFactorizer (l `o` natId Inj2) (constPostcomp (tgtF c) Inj2 . (c `o` natId Inj2))+    colimitFactorizer (l `o` natId Inj2) (constPostcompOut (c `o` natId Inj2))   -- | The coproduct of categories ':++:' is the binary coproduct in 'Cat'.@@ -549,7 +591,7 @@  -- | A specialisation of the colimit adjunction to coproducts. coprodAdj :: HasBinaryCoproducts k => Adjunction k (k :**: k) (CoproductFunctor k) (DiagProd k)-coprodAdj = mkAdjunction CoproductFunctor DiagProd (\(l :**: r) -> inj1 l r :**: inj2 l r) (\x -> x ||| x)+coprodAdj = mkAdjunctionUnits CoproductFunctor DiagProd (\(l :**: r) -> inj1 l r :**: inj2 l r) (\x -> x ||| x)  data p :+: q where   (:+:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryCoproducts k) => p -> q -> p :+: q@@ -636,3 +678,18 @@    colimit (Nat f _ _) = Nat f (Const (f % terminalObject)) (\z -> f % terminate z)   colimitFactorizer Nat{} n = n ! terminalObject+++data ForAll f = ForAll (forall a. Obj (->) a -> f :% a)+type instance LimitFam (->) (->) f = ForAll f++instance HasLimits (->) (->) where+  limit (Nat f _ _) = Nat (Const (\x -> x)) f (\a (ForAll g) -> g a)+  limitFactorizer Nat{} n = \z -> ForAll (\a -> (n ! a) z)++data Exists f = forall a. Exists (Obj (->) a) (f :% a)+type instance ColimitFam (->) (->) f = Exists f++instance HasColimits (->) (->) where+  colimit (Nat f _ _) = Nat f (Const (\x -> x)) Exists+  colimitFactorizer Nat{} n = \(Exists a fa) -> (n ! a) fa

@@ -22,7 +22,7 @@ import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation-import Data.Category.Adjunction (Adjunction(Adjunction))+import Data.Category.Adjunction import Data.Category.Limit import Data.Category.Product @@ -143,7 +143,10 @@ monadFunctor :: Monad f -> f monadFunctor (unit -> Nat _ f _) = f +idMonad :: Category k => Monad (Id k)+idMonad = MonoidObject (natId Id) (idPrecomp Id) + -- | A comonad is a comonoid in the category of endofunctors. type Comonad f = ComonoidObject (EndoFunctorCompose (Dom f)) f @@ -157,11 +160,30 @@   , comultiply = Nat f (f :.: f) dupl   } +idComonad :: Category k => Comonad (Id k)+idComonad = ComonoidObject (natId Id) (idPrecompInv Id) + -- | Every adjunction gives rise to an associated monad. adjunctionMonad :: Adjunction c d f g -> Monad (g :.: f)-adjunctionMonad (Adjunction f g un coun) = mkMonad (g :.: f) (un !) ((Wrap g f % coun) !)+adjunctionMonad adj@(Adjunction f g _ _) = +  let MonoidObject ret mult = adjunctionMonadT adj idMonad +  in mkMonad (g :.: f) (ret !) (mult !) +-- | Every adjunction gives rise to an associated monad transformer.+adjunctionMonadT :: (Dom m ~ c) => Adjunction c d f g -> Monad m -> Monad (g :.: m :.: f)+adjunctionMonadT adj@(Adjunction f g _ _) (MonoidObject ret@(Nat _ m _) mult) = mkMonad (g :.: m :.: f) +  ((Wrap g f % ret . idPrecompInv g `o` natId f . adjunctionUnit adj) !) +  ((Wrap g f % (mult . idPrecomp m `o` natId m . Wrap m m % adjunctionCounit adj)) !)+ -- | Every adjunction gives rise to an associated comonad. adjunctionComonad :: Adjunction c d f g -> Comonad (f :.: g)-adjunctionComonad (Adjunction f g un coun) = mkComonad (f :.: g) (coun !) ((Wrap f g % un) !)+adjunctionComonad adj@(Adjunction f g _ _) = +  let ComonoidObject extr dupl = adjunctionComonadT adj idComonad+  in mkComonad (f :.: g) (extr !) (dupl !)++-- | Every adjunction gives rise to an associated comonad transformer.+adjunctionComonadT :: (Dom w ~ d) => Adjunction c d f g -> Comonad w -> Comonad (f :.: w :.: g)+adjunctionComonadT adj@(Adjunction f g _ _) (ComonoidObject extr@(Nat w _ _) dupl) = mkComonad (f :.: w :.: g) +  ((adjunctionCounit adj . idPrecomp f `o` natId g . Wrap f g % extr) !)+  ((Wrap f g % (Wrap w w % adjunctionUnit adj . idPrecompInv w `o` natId w . dupl)) !)

@@ -10,7 +10,6 @@ ----------------------------------------------------------------------------- module Data.Category.NNO where -import Data.Category import Data.Category.Functor import Data.Category.Limit import Data.Category.Unit@@ -58,5 +57,5 @@   type Cod (PrimRec z s) = Cod z   type PrimRec z s :% I1 () = z :% ()   type PrimRec z s :% I2 n  = s :% PrimRec z s :% n-  PrimRec z s % Fix (I1 Unit) = z % Unit+  PrimRec z _ % Fix (I1 Unit) = z % Unit   PrimRec z s % Fix (I2 n) = s % PrimRec z s % n

@@ -13,7 +13,6 @@   -- * Natural transformations     (:~>)   , Component-  , Com(..)   , (!)   , o   , natId@@ -24,6 +23,7 @@   , Nat(..)   , Endo   , Presheaves+  , Profunctors    -- * Functor isomorphisms   , compAssoc@@ -32,10 +32,10 @@   , idPrecompInv   , idPostcomp   , idPostcompInv-  , constPrecomp-  , constPrecompInv-  , constPostcomp-  , constPostcompInv+  , constPrecompIn+  , constPrecompOut+  , constPostcompIn+  , constPostcompOut    -- * Related functors   , FunctorCompose(..)@@ -69,10 +69,6 @@ -- | A component for an object @z@ is an arrow from @F z@ to @G z@. type Component f g z = Cod f (f :% z) (g :% z) --- | A newtype wrapper for components,---   which can be useful for helper functions dealing with components.-newtype Com f g z = Com { unCom :: Component f g z }- -- | 'n ! a' returns the component for the object @a@ of a natural transformation @n@. --   This can be generalized to any arrow (instead of just identity arrows). (!) :: (Category c, Category d) => Nat c d f g -> c a b -> d (f :% a) (g :% b)@@ -126,21 +122,17 @@ idPostcompInv f = Nat f (Id :.: f) (f %)  -constPrecomp :: (Category c1, Functor f)-             => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (f :.: Const c1 (Dom f) x) (Const c1 (Cod f) (f :% x))-constPrecomp (Const x) f = let fx = f % x in Nat (f :.: Const x) (Const fx) (\_ -> fx)+constPrecompIn :: Nat j d (f :.: Const j c x) g -> Nat j d (Const j d (f :% x)) g+constPrecompIn (Nat (f :.: Const x) g n) = Nat (Const (f % x)) g n -constPrecompInv :: (Category c1, Functor f)-                => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (Const c1 (Cod f) (f :% x)) (f :.: Const c1 (Dom f) x)-constPrecompInv (Const x) f = let fx = f % x in Nat (Const fx) (f :.: Const x) (\_ -> fx)+constPrecompOut :: Nat j d f (g :.: Const j c x) -> Nat j d f (Const j d (g :% x))+constPrecompOut (Nat f (g :.: Const x) n) = Nat f (Const (g % x)) n -constPostcomp :: (Category c2, Functor f)-              => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Cod f) c2 x :.: f) (Const (Dom f) c2 x)-constPostcomp (Const x) f = Nat (Const x :.: f) (Const x) (\_ -> x)+constPostcompIn :: Nat j d (Const k d x :.: f) g -> Nat j d (Const j d x) g+constPostcompIn (Nat (Const x :.: _) g n) = Nat (Const x) g n -constPostcompInv :: (Category c2, Functor f)-                 => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Dom f) c2 x) (Const (Cod f) c2 x :.: f)-constPostcompInv (Const x) f = Nat (Const x) (Const x :.: f) (\_ -> x)+constPostcompOut :: Nat j d f (Const k d x :.: g) -> Nat j d f (Const j d x)+constPostcompOut (Nat f (Const x :.: _) n) = Nat f (Const x) n   data FunctorCompose (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) = FunctorCompose@@ -161,6 +153,8 @@  type Presheaves k = Nat (Op k) (->) +type Profunctors c d = Nat (Op d :**: c) (->)+ -- | @Precompose f e@ is the functor such that @Precompose f e :% g = g :.: f@, --   for functors @g@ that compose with @f@ and with codomain @e@. type Precompose f e = FunctorCompose (Dom f) (Cod f) e :.: Tuple2 (Nat (Cod f) e) (Nat (Dom f) (Cod f)) f@@ -171,7 +165,7 @@ --   for functors @g@ that compose with @f@ and with domain @c@. type Postcompose f c = FunctorCompose c (Dom f) (Cod f) :.: Tuple1 (Nat (Dom f) (Cod f)) (Nat c (Dom f)) f postcompose :: (Category e, Functor f) => f -> Postcompose f e-postcompose f = FunctorCompose :.: Tuple1 (natId f)+postcompose f = FunctorCompose :.: tuple1 (natId f)   data Wrap f h = Wrap f h@@ -200,4 +194,4 @@   type Dom (Tuple c1 c2) = c1   type Cod (Tuple c1 c2) = Nat c2 (c1 :**: c2)   type Tuple c1 c2 :% a = Tuple1 c1 c2 a-  Tuple % f = Nat (Tuple1 (src f)) (Tuple1 (tgt f)) (\z -> f :**: z)+  Tuple % f = Nat (tuple1 (src f)) (tuple1 (tgt f)) (\z -> f :**: z)

@@ -1,5 +1,5 @@ name:                data-category-version:             0.6.2+version:             0.7 synopsis:            Category theory  description:         Data-category is a collection of categories, and some categorical constructions on them.