data-category 0.4.1 → 0.5.0

raw patch · 26 files changed

+1005/−856 lines, 26 filesdep −basePVP ok

version bump matches the API change (PVP)

Dependencies removed: base

API changes (from Hackage documentation)

Files

• Data/Category.hs +16/−19
• Data/Category/Adjunction.hs +36/−15
• Data/Category/Boolean.hs +1/−27
• Data/Category/CartesianClosed.hs +30/−32
• Data/Category/Comma.hs +37/−7
• Data/Category/Coproduct.hs +46/−11
• Data/Category/Dialg.hs +10/−41
• Data/Category/Discrete.hs +0/−119
• Data/Category/Fix.hs +65/−0
• Data/Category/Functor.hs +32/−48
• Data/Category/Kleisli.hs +11/−13
• Data/Category/Limit.hs +305/−157
• Data/Category/Monoid.hs +0/−82
• Data/Category/Monoidal.hs +29/−41
• Data/Category/NNO.hs +62/−0
• Data/Category/NaturalTransformation.hs +17/−19
• Data/Category/Omega.hs +0/−119
• Data/Category/Peano.hs +0/−57
• Data/Category/Presheaf.hs +12/−14
• Data/Category/Product.hs +1/−3
• Data/Category/RepresentableFunctor.hs +8/−10
• Data/Category/Simplex.hs +200/−0
• Data/Category/Unit.hs +25/−0
• Data/Category/Void.hs +42/−0
• Data/Category/Yoneda.hs +12/−14
• data-category.cabal +8/−8

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, RankNTypes #-}+{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category@@ -19,39 +19,36 @@      ) where -import Prelude (($))-import qualified Prelude- infixr 8 .   -- | Whenever objects are required at value level, they are represented by their identity arrows.-type Obj (~>) a = a ~> a+type Obj k a = k a a --- | An instance of @Category (~>)@ declares the arrow @(~>)@ as a category.-class Category (~>) where+-- | An instance of @Category k@ declares the arrow @k@ as a category.+class Category k where   -  src :: a ~> b -> Obj (~>) a-  tgt :: a ~> b -> Obj (~>) b+  src :: k a b -> Obj k a+  tgt :: k a b -> Obj k b -  (.) :: b ~> c -> a ~> b -> a ~> c+  (.) :: k b c -> k a b -> k a c   -- | The category with Haskell types as objects and Haskell functions as arrows. instance Category (->) where   -  src _ = Prelude.id-  tgt _ = Prelude.id+  src _ = \x -> x+  tgt _ = \x -> x   -  (.)   = (Prelude..)    +  f . g = \x -> f (g x)  -data Op (~>) a b = Op { unOp :: b ~> a }+data Op k a b = Op { unOp :: k b a } --- | @Op (~>)@ is opposite category of the category @(~>)@.-instance Category (~>) => Category (Op (~>)) where+-- | @Op k@ is opposite category of the category @k@.+instance Category k => Category (Op k) where   -  src (Op a)      = Op $ tgt a-  tgt (Op a)      = Op $ src a+  src (Op a)      = Op (tgt a)+  tgt (Op a)      = Op (src a)   -  (Op a) . (Op b) = Op $ b . a+  (Op a) . (Op b) = Op (b . a)

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleContexts, ScopedTypeVariables, RankNTypes #-}+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleContexts, ScopedTypeVariables, RankNTypes, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Adjunction@@ -18,6 +18,8 @@   , rightAdjunct      -- * Adjunctions as a category+  , idAdj+  , composeAdj   , AdjArrow(..)      -- * Adjunctions from universal morphisms@@ -33,9 +35,6 @@    ) where   -import Prelude (($), id, flip)-import Control.Monad.Instances ()- import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation@@ -61,6 +60,8 @@ 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) ++ -- 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)@@ -80,29 +81,49 @@ terminalPropAdjunction :: forall f g c d. (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 terminalPropAdjunction f g univ = mkAdjunction f g -  (\a -> unOp $ represent (univ (f % a)) (Op a) (f % a)) +  (\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)++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')++ data AdjArrow c d where   AdjArrow :: (Category c, Category d) => Adjunction c d f g -> AdjArrow (CatW c) (CatW d)  -- | The category with categories as objects and adjunctions as arrows. instance Category AdjArrow where   -  src (AdjArrow (Adjunction _ _ _ _)) = AdjArrow $ mkAdjunction Id Id id id-  tgt (AdjArrow (Adjunction _ _ _ _)) = AdjArrow $ mkAdjunction Id Id id id+  src (AdjArrow (Adjunction _ _ _ _)) = AdjArrow idAdj+  tgt (AdjArrow (Adjunction _ _ _ _)) = AdjArrow idAdj   -  AdjArrow (Adjunction f g u c) . AdjArrow (Adjunction f' g' u' c') = AdjArrow $ -    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')+  AdjArrow x . AdjArrow y = AdjArrow (composeAdj x y)   +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 +  (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)++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 +  (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)+ contAdj :: Adjunction (Op (->)) (->) (Opposite ((->) :-*: r) :.: OpOpInv (->)) ((->) :-*: r) contAdj = mkAdjunction-  (Opposite (hom_X id) :.: OpOpInv)-  (hom_X id)-  (\_ -> flip ($))-  (\_ -> Op (flip ($)))+  (Opposite (hom_X (\x -> x)) :.: OpOpInv)+  (hom_X (\x -> x))+  (\_ x f -> f x)+  (\_ -> Op (\x f -> f x))

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, GADTs, TypeOperators, ScopedTypeVariables, UndecidableInstances #-}+{-# LANGUAGE TypeFamilies, GADTs, TypeOperators, ScopedTypeVariables, UndecidableInstances, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Boolean@@ -14,8 +14,6 @@ ----------------------------------------------------------------------------- module Data.Category.Boolean where -import Prelude hiding ((.), id, Functor)- import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation@@ -48,7 +46,6 @@   F2T . Fls = F2T   Tru . F2T = F2T   Tru . Tru = Tru-  _      . _      = error "Other combinations should not type check"   -- | False is the initial object in the Boolean category.@@ -57,7 +54,6 @@   initialObject = Fls   initialize Fls = Fls   initialize Tru = F2T-  initialize _   = error "Other values should not type check"    -- | True is the terminal object in the Boolean category. instance HasTerminalObject Boolean where@@ -65,7 +61,6 @@   terminalObject = Tru   terminate Fls = F2T   terminate Tru = Tru-  terminate _   = error "Other values should not type check"   type instance BinaryProduct Boolean Fls Fls = Fls@@ -80,19 +75,16 @@   proj1 Fls Tru = Fls   proj1 Tru Fls = F2T   proj1 Tru Tru = Tru-  proj1 _   _   = error "Other combinations should not type check"   proj2 Fls Fls = Fls   proj2 Fls Tru = F2T   proj2 Tru Fls = Fls   proj2 Tru Tru = Tru-  proj2 _   _   = error "Other combinations should not type check"        Fls &&& Fls = Fls   Fls &&& F2T = Fls   F2T &&& Fls = Fls   F2T &&& F2T = F2T   Tru &&& Tru = Tru-  _   &&& _   = error "Other combinations should not type check"   type instance BinaryCoproduct Boolean Fls Fls = Fls@@ -107,19 +99,16 @@   inj1 Fls Tru = F2T   inj1 Tru Fls = Tru   inj1 Tru Tru = Tru-  inj1 _   _   = error "Other combinations should not type check"   inj2 Fls Fls = Fls   inj2 Fls Tru = Tru   inj2 Tru Fls = F2T   inj2 Tru Tru = Tru-  inj2 _   _   = error "Other combinations should not type check"        Fls ||| Fls = Fls   F2T ||| F2T = F2T   F2T ||| Tru = Tru   Tru ||| F2T = Tru   Tru ||| Tru = Tru-  _   ||| _   = error "Other combinations should not type check"   type instance Exponential Boolean Fls Fls = Tru@@ -134,13 +123,11 @@   apply Fls Tru = F2T   apply Tru Fls = Fls   apply Tru Tru = Tru-  apply _   _   = error "Other combinations should not type check"      tuple Fls Fls = F2T   tuple Fls Tru = Tru   tuple Tru Fls = Fls   tuple Tru Tru = Tru-  tuple _   _   = error "Other combinations should not type check"      Fls ^^^ Fls = Tru   Fls ^^^ F2T = F2T@@ -171,16 +158,3 @@ falseProductComonoid :: ComonoidObject (ProductFunctor Boolean) Fls falseProductComonoid = ComonoidObject F2T Fls --data NatAsFunctor f g where-  NatAsFunctor :: (Functor f, Functor g, Category c, Category d, Dom f ~ c, Cod f ~ d, Dom g ~ c, Cod g ~ d)-               => Nat (Dom f) (Cod f) f g -> NatAsFunctor f g-type instance Dom (NatAsFunctor f g) = Dom f :**: Boolean-type instance Cod (NatAsFunctor f g) = Cod f-type instance NatAsFunctor f g :% (a, Fls) = f :% a-type instance NatAsFunctor f g :% (a, Tru) = g :% a--- | A natural transformation @Nat c d@ is isomorphic to a functor from @c :**: 2@ to @d@.-instance (Category (Dom f), Category (Cod f)) => Functor (NatAsFunctor f g) where-  NatAsFunctor (Nat f _ _) % (a :**: Fls) = f % a-  NatAsFunctor (Nat _ g _) % (a :**: Tru) = g % a-  NatAsFunctor n           % (a :**: F2T) = n ! a

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ScopedTypeVariables, UndecidableInstances, TypeSynonymInstances #-}+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ScopedTypeVariables, UndecidableInstances, TypeSynonymInstances, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.CartesianClosed@@ -10,8 +10,6 @@ ----------------------------------------------------------------------------- module Data.Category.CartesianClosed where   -import Prelude (($))- import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation@@ -21,22 +19,22 @@ import Data.Category.Monoidal as M  -type family Exponential (~>) y z :: *+type family Exponential (k :: * -> * -> *) y z :: *  -- | A category is cartesian closed if it has all products and exponentials for all objects.-class (HasTerminalObject (~>), HasBinaryProducts (~>)) => CartesianClosed (~>) where+class (HasTerminalObject k, HasBinaryProducts k) => CartesianClosed k where   -  apply :: Obj (~>) y -> Obj (~>) z -> BinaryProduct (~>) (Exponential (~>) y z) y ~> z-  tuple :: Obj (~>) y -> Obj (~>) z -> z ~> Exponential (~>) y (BinaryProduct (~>) z y)-  (^^^) :: (z1 ~> z2) -> (y2 ~> y1) -> (Exponential (~>) y1 z1 ~> Exponential (~>) y2 z2)+  apply :: Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) z+  tuple :: Obj k y -> Obj k z -> k z (Exponential k y (BinaryProduct k z y))+  (^^^) :: k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)  -data ExpFunctor ((~>) :: * -> * -> *) = ExpFunctor-type instance Dom (ExpFunctor (~>)) = Op (~>) :**: (~>)-type instance Cod (ExpFunctor (~>)) = (~>)-type instance (ExpFunctor (~>)) :% (y, z) = Exponential (~>) y z+data ExpFunctor (k :: * -> * -> *) = ExpFunctor+type instance Dom (ExpFunctor k) = Op k :**: k+type instance Cod (ExpFunctor k) = k+type instance (ExpFunctor k) :% (y, z) = Exponential k y z -- | The exponential as a bifunctor.-instance CartesianClosed (~>) => Functor (ExpFunctor (~>)) where+instance CartesianClosed k => Functor (ExpFunctor k) where   ExpFunctor % (Op y :**: z) = z ^^^ y  @@ -66,7 +64,7 @@ type instance ToTuple1 y z :% a = Tuple1 z y a -- | 'ToTuple1' converts an object @a@ to the functor 'Tuple1' @a@. instance (Category y, Category z) => Functor (ToTuple1 y z) where-  ToTuple1 % f = Nat (Tuple1 (src f)) (Tuple1 (tgt f)) $ \z -> f :**: z+  ToTuple1 % f = Nat (Tuple1 (src f)) (Tuple1 (tgt f)) (\z -> f :**: z)  data ToTuple2 (y :: * -> * -> *) (z :: * -> * -> *) = ToTuple2 type instance Dom (ToTuple2 y z) = y@@ -74,7 +72,7 @@ type instance ToTuple2 y z :% a = Tuple2 z y a -- | 'ToTuple2' converts an object @a@ to the functor 'Tuple2' @a@. instance (Category y, Category z) => Functor (ToTuple2 y z) where-  ToTuple2 % f = Nat (Tuple2 (src f)) (Tuple2 (tgt f)) $ \y -> y :**: f+  ToTuple2 % f = Nat (Tuple2 (src f)) (Tuple2 (tgt f)) (\y -> y :**: f)   type instance Exponential Cat (CatW c) (CatW d) = CatW (Nat c d)@@ -88,36 +86,36 @@   -- | The product functor is left adjoint the the exponential functor.-curryAdj :: CartesianClosed (~>) -         => Obj (~>) y -         -> Adjunction (~>) (~>) -              (ProductFunctor (~>) :.: Tuple2 (~>) (~>) y) -              (ExpFunctor (~>) :.: Tuple1 (Op (~>)) (~>) y)+curryAdj :: CartesianClosed k +         => Obj k y +         -> 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)  -- | From the adjunction between the product functor and the exponential functor we get the curry and uncurry functions, --   generalized to any cartesian closed category.-curry :: CartesianClosed (~>) => Obj (~>) x -> Obj (~>) y -> Obj (~>) z -> BinaryProduct (~>) x y ~> z -> x ~> Exponential (~>) y z+curry :: CartesianClosed k => Obj k x -> Obj k y -> Obj k z -> k (BinaryProduct k x y) z -> k x (Exponential k y z) curry x y _ = leftAdjunct (curryAdj y) x -uncurry :: CartesianClosed (~>) => Obj (~>) x -> Obj (~>) y -> Obj (~>) z -> x ~> Exponential (~>) y z -> BinaryProduct (~>) x y ~> z+uncurry :: CartesianClosed k => Obj k x -> Obj k y -> Obj k z -> k x (Exponential k y z) -> k (BinaryProduct k x y) z uncurry _ y z = rightAdjunct (curryAdj y) z  -- | From every adjunction we get a monad, in this case the State monad.-type State (~>) s a = Exponential (~>) s (BinaryProduct (~>) a s)+type State k s a = Exponential k s (BinaryProduct k a s) -stateMonadReturn :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> a ~> State (~>) s a-stateMonadReturn s a = M.unit (adjunctionMonad $ curryAdj s) ! a+stateMonadReturn :: CartesianClosed k => Obj k s -> Obj k a -> k a (State k s a)+stateMonadReturn s a = M.unit (adjunctionMonad (curryAdj s)) ! a -stateMonadJoin :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> State (~>) s (State (~>) s a) ~> State (~>) s a-stateMonadJoin s a = M.multiply (adjunctionMonad $ curryAdj s) ! a+stateMonadJoin :: CartesianClosed k => Obj k s -> Obj k a -> k (State k s (State k s a)) (State k s a)+stateMonadJoin s a = M.multiply (adjunctionMonad (curryAdj s)) ! a  -- ! From every adjunction we also get a comonad, the Context comonad in this case.-type Context (~>) s a = BinaryProduct (~>) (Exponential (~>) s a) s+type Context k s a = BinaryProduct k (Exponential k s a) s -contextComonadExtract :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> Context (~>) s a ~> a-contextComonadExtract s a = M.counit (adjunctionComonad $ curryAdj s) ! a+contextComonadExtract :: CartesianClosed k => Obj k s -> Obj k a -> k (Context k s a) a+contextComonadExtract s a = M.counit (adjunctionComonad (curryAdj s)) ! a -contextComonadDuplicate :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> Context (~>) s a ~> Context (~>) s (Context (~>) s a)-contextComonadDuplicate s a = M.comultiply (adjunctionComonad $ curryAdj s) ! a+contextComonadDuplicate :: CartesianClosed k => Obj k s -> Obj k a -> k (Context k s a) (Context k s (Context k s a))+contextComonadDuplicate s a = M.comultiply (adjunctionComonad (curryAdj s)) ! a 

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances #-}+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, ScopedTypeVariables, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Comma@@ -12,15 +12,15 @@ ----------------------------------------------------------------------------- module Data.Category.Comma where -import Prelude()- import Data.Category import Data.Category.Functor+import Data.Category.Limit+import Data.Category.RepresentableFunctor   data CommaO :: * -> * -> * -> * where-  CommaO :: (Cod t ~ (~>), Cod s ~ (~>))-    => Obj (Dom t) a -> ((t :% a) ~> (s :% b)) -> Obj (Dom s) b -> CommaO t s (a, b)+  CommaO :: (Cod t ~ k, Cod s ~ k)+    => Obj (Dom t) a -> k (t :% a) (s :% b) -> Obj (Dom s) b -> CommaO t s (a, b)      data (:/\:) :: * -> * -> * -> * -> * where    CommaA :: @@ -30,11 +30,14 @@     CommaO t s (a', b') ->     (t :/\: s) (a, b) (a', b') +commaId :: CommaO t s (a, b) -> Obj (t :/\: s) (a, b)+commaId o@(CommaO a _ b) = CommaA o a b o+ -- | The comma category T \\downarrow S instance (Category (Dom t), Category (Dom s)) => Category (t :/\: s) where     -  src (CommaA so@(CommaO a _ b) _ _ _)    = CommaA so a        b        so-  tgt (CommaA _ _ _ to@(CommaO a _ b))    = CommaA to a        b        to+  src (CommaA so _ _ _) = commaId so+  tgt (CommaA _ _ _ to) = commaId to      (CommaA _ g h to) . (CommaA so g' h' _) = CommaA so (g . g') (h . h') to @@ -44,3 +47,30 @@  type (c `ObjectsUnder` a) = Id c `ObjectsFUnder` a type (c `ObjectsOver`  a) = Id c `ObjectsFOver`  a+++initialUniversalComma :: forall u x c a a_+                       . (Functor u, c ~ (u `ObjectsFUnder` x), HasInitialObject c, (a_, a) ~ InitialObject c)+                      => u -> InitialUniversal x u a+initialUniversalComma u = case initialObject :: Obj c (a_, a) of+  CommaA (CommaO _ mor a) _ _ _ -> +    initialUniversal u a mor factorizer+      where+        factorizer :: forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y+        factorizer y arr = case (init (commaId (CommaO y arr y))) of CommaA _ _ f _ -> f+          where+            init :: Obj c (y, y) -> c (a_, a) (y, y)+            init = initialize++terminalUniversalComma :: forall u x c a a_+                        . (Functor u, c ~ (u `ObjectsFOver` x), HasTerminalObject c, (a, a_) ~ TerminalObject c)+                       => u -> TerminalUniversal x u a+terminalUniversalComma u = case terminalObject :: Obj c (a, a_) of+  CommaA (CommaO a mor _) _ _ _ ->+    terminalUniversal u a mor factorizer+      where+        factorizer :: forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a+        factorizer y arr = case (term (commaId (CommaO y arr y))) of CommaA _ f _ _ -> f+          where+            term :: Obj c (y, y) -> c (y, y) (a, a_)+            term = terminate

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleContexts #-}+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleContexts, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Coproduct@@ -10,12 +10,14 @@ ----------------------------------------------------------------------------- module Data.Category.Coproduct where -import Prelude (error)- import Data.Category import Data.Category.Functor +import Data.Category.NaturalTransformation+import Data.Category.Product+import Data.Category.Unit + data I1 a data I2 a @@ -23,7 +25,7 @@   I1 :: c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)   I2 :: c2 a2 b2 -> (:++:) c1 c2 (I2 a2) (I2 b2) --- | The coproduct category of category @c1@ and @c2@.+-- | The coproduct category of categories @c1@ and @c2@. instance (Category c1, Category c2) => Category (c1 :++: c2) where      src (I1 a)      = I1 (src a)@@ -33,7 +35,6 @@    (I1 a) . (I1 b) = I1 (a . b)   (I2 a) . (I2 b) = I2 (a . b)-  _      . _      = error "Other combinations should not type check"       @@ -64,13 +65,13 @@   (g :+++: _) % I1 f = I1 (g % f)   (_ :+++: g) % I2 f = I2 (g % f)   -data CodiagCoprod ((~>) :: * -> * -> *) = CodiagCoprod-type instance Dom (CodiagCoprod (~>)) = (~>) :++: (~>)-type instance Cod (CodiagCoprod (~>)) = (~>)-type instance CodiagCoprod (~>) :% I1 a = a-type instance CodiagCoprod (~>) :% I2 a = a+data CodiagCoprod (k :: * -> * -> *) = CodiagCoprod+type instance Dom (CodiagCoprod k) = k :++: k+type instance Cod (CodiagCoprod k) = k+type instance CodiagCoprod k :% I1 a = a+type instance CodiagCoprod k :% I2 a = a -- | 'CodiagCoprod' is the codiagonal functor for coproducts.-instance Category (~>) => Functor (CodiagCoprod (~>)) where +instance Category k => Functor (CodiagCoprod k) where    CodiagCoprod % I1 f = f   CodiagCoprod % I2 f = f @@ -94,3 +95,37 @@   Cotuple2 a % I1 _ = a   Cotuple2 _ % I2 f = f ++data (:>>:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where+  I1A :: c1 a1 b1 -> (:>>:) c1 c2 (I1 a1) (I1 b1)+  I12 :: Obj c1 a -> Obj c2 b -> (:>>:) c1 c2 (I1 a) (I2 b)+  I2A :: c2 a2 b2 -> (:>>:) c1 c2 (I2 a2) (I2 b2)++-- | The directed coproduct category of categories @c1@ and @c2@.+instance (Category c1, Category c2) => Category (c1 :>>: c2) where++  src (I1A a)   = I1A (src a)+  src (I12 a _) = I1A a+  src (I2A a)   = I2A (src a)+  tgt (I1A a)   = I1A (tgt a)+  tgt (I12 _ b) = I2A b+  tgt (I2A a)   = I2A (tgt a)++  (I1A a) . (I1A b) = I1A (a . b)+  (I12 _ a) . (I1A b) = I12 (src b) a+  (I2A a) . (I12 b _) = I12 b (tgt a)+  (I2A a) . (I2A b) = I2A (a . b)+++++data NatAsFunctor f g = NatAsFunctor (Nat (Dom f) (Cod f) f g)+type instance Dom (NatAsFunctor f g) = Dom f :**: (Unit :>>: Unit)+type instance Cod (NatAsFunctor f g) = Cod f+type instance NatAsFunctor f g :% (a, I1 ()) = f :% a+type instance NatAsFunctor f g :% (a, I2 ()) = g :% a+-- | A natural transformation @Nat c d@ is isomorphic to a functor from @c :**: 2@ to @d@.+instance (Functor f, Functor g, Dom f ~ Dom g, Cod f ~ Cod g) => Functor (NatAsFunctor f g) where+  NatAsFunctor (Nat f _ _) % (a :**: I1A Unit) = f % a+  NatAsFunctor (Nat _ g _) % (a :**: I2A Unit) = g % a+  NatAsFunctor n           % (a :**: I12 Unit Unit) = n ! a

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances, FlexibleContexts, ViewPatterns, ScopedTypeVariables, UndecidableInstances #-}+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances, FlexibleContexts, ViewPatterns, ScopedTypeVariables, UndecidableInstances, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Dialg@@ -12,9 +12,6 @@ ----------------------------------------------------------------------------- module Data.Category.Dialg where -import Prelude (($), id)-import qualified Prelude- import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation@@ -46,7 +43,7 @@   src (DialgA s _ _) = dialgId s   tgt (DialgA _ t _) = dialgId t   -  DialgA _ t f . DialgA s _ g = DialgA s t $ f . g+  DialgA _ t f . DialgA s _ g = DialgA s t (f . g)   @@ -70,35 +67,7 @@   -newtype FixF f = InF { outF :: f :% FixF f } --- | Catamorphisms for endofunctors in Hask.-cataHask :: Prelude.Functor f => Cata (EndoHask f) a-cataHask a@(Dialgebra _ f) = DialgA (dialgebra initialObject) a $ cata_f where cata_f = f . (EndoHask % cata_f) . outF ---- | Anamorphisms for endofunctors in Hask.-anaHask :: Prelude.Functor f => Ana (EndoHask f) a-anaHask a@(Dialgebra _ f) = DialgA a (dialgebra terminalObject) $ ana_f where ana_f = InF . (EndoHask % ana_f) . f ----- | 'FixF' provides the initial F-algebra for endofunctors in Hask.-instance Prelude.Functor f => HasInitialObject (Dialg (EndoHask f) (Id (->))) where-  -  type InitialObject (Dialg (EndoHask f) (Id (->))) = FixF (EndoHask f)-  -  initialObject = dialgId $ Dialgebra id InF-  initialize a = cataHask (dialgebra a)-  --- | 'FixF' also provides the terminal F-coalgebra for endofunctors in Hask.-instance Prelude.Functor f => HasTerminalObject (Dialg (Id (->)) (EndoHask f)) where--  type TerminalObject (Dialg (Id (->)) (EndoHask f)) = FixF (EndoHask f)-  -  terminalObject = dialgId $ Dialgebra id outF-  terminate a = anaHask (dialgebra a)-  -- data NatNum = Z () | S NatNum primRec :: (() -> t) -> (t -> t) -> NatNum -> t primRec z _ (Z ()) = z ()@@ -110,9 +79,9 @@      type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) = NatNum     -  initialObject = dialgId $ Dialgebra id (Z :**: S)+  initialObject = dialgId (Dialgebra (\x -> x) (Z :**: S))   -  initialize (dialgebra -> d@(Dialgebra _ (z :**: s))) = DialgA (dialgebra initialObject) d $ primRec z s+  initialize (dialgebra -> d@(Dialgebra _ (z :**: s))) = DialgA (dialgebra initialObject) d (primRec z s)   @@ -121,10 +90,10 @@ type instance Cod (FreeAlg m) = Alg m type instance FreeAlg m :% a = m :% a -- | @FreeAlg@ M takes @x@ to the free algebra @(M x, mu_x)@ of the monad @M@.-instance (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (FreeAlg m) where-  FreeAlg m % f = DialgA (alg (src f)) (alg (tgt f)) $ monadFunctor m % f+instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (FreeAlg m) where+  FreeAlg m % f = DialgA (alg (src f)) (alg (tgt f)) (monadFunctor m % f)     where-      alg :: Obj (~>) x -> Algebra m (m :% x)+      alg :: Obj k x -> Algebra m (m :% x)       alg x = Dialgebra (monadFunctor m % x) (multiply m ! x)  data ForgetAlg m = ForgetAlg@@ -132,11 +101,11 @@ type instance Cod (ForgetAlg m) = Dom m type instance ForgetAlg m :% a = a -- | @ForgetAlg m@ is the forgetful functor for @Alg m@.-instance (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (ForgetAlg m) where+instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (ForgetAlg m) where   ForgetAlg % DialgA _ _ f = f -eilenbergMooreAdj :: (Functor m, Dom m ~ (~>), Cod m ~ (~>)) -  => Monad m -> A.Adjunction (Alg m) (~>) (FreeAlg m) (ForgetAlg m)+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   (\x -> unit m ! x)   (\(DialgA (Dialgebra _ h) _ _) -> DialgA (Dialgebra (src h) (monadFunctor m % h)) (Dialgebra (tgt h) h) h)

@@ -1,119 +0,0 @@-{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, RankNTypes, ScopedTypeVariables, FlexibleContexts, FlexibleInstances, UndecidableInstances #-}--------------------------------------------------------------------------------- |--- Module      :  Data.Category.Discrete--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  sjoerd@w3future.com--- Stability   :  experimental--- Portability :  non-portable------ Discrete n, the category with n objects, and as the only arrows their identities.-------------------------------------------------------------------------------module Data.Category.Discrete (--  -- * Discrete Categories-    Discrete(..)-  , Z, S-  , Void-  , Unit-  , Pair-  , magicZ-  -  -- * Functors-  , Succ(..)-  , DiscreteDiagram(..)-    -  -- * Natural Transformations-  , voidNat-    -) where--import Prelude hiding ((.), id, Functor, product)--import Data.Category-import Data.Category.Functor-import Data.Category.NaturalTransformation---data Z-data S n---- | The arrows in Discrete n, a finite set of identity arrows.-data Discrete :: * -> * -> * -> * where-  Z :: Discrete (S n) Z Z-  S :: Discrete n a a -> Discrete (S n) (S a) (S a)---magicZ :: Discrete Z a b -> x-magicZ x = x `seq` error "we never get this far"----- | @Discrete Z@ is the discrete category with no objects.-instance Category (Discrete Z) where-  -  src   = magicZ-  tgt   = magicZ-  -  a . b = magicZ (a `seq` b)----- | @Discrete (S n)@ is the discrete category with one object more than @Discrete n@.-instance Category (Discrete n) => Category (Discrete (S n)) where-  -  src Z     = Z-  src (S a) = S $ src a-  -  tgt Z     = Z-  tgt (S a) = S $ tgt a-  -  Z   . Z   = Z-  S a . S b = S (a . b)-  _   . _   = error "Other combinations should not type-check."----- | 'Void' is the empty category.-type Void = Discrete Z--- | 'Unit' is the discrete category with one object.-type Unit = Discrete (S Z)--- | 'Pair' is the discrete category with two objects.-type Pair = Discrete (S (S Z))---data Succ n = Succ-type instance Dom (Succ n) = Discrete n-type instance Cod (Succ n) = Discrete (S n)-type instance Succ n :% a = S a--- | 'Succ' maps each object in @Discrete n@ to its successor in @Discrete (S n)@.-instance (Category (Discrete n)) => Functor (Succ n) where-  Succ % Z     = S Z-  Succ % (S a) = S (S a)---infixr 7 :::---- | The functor from @Discrete n@ to @(~>)@, a diagram of @n@ objects in @(~>)@. -data DiscreteDiagram :: (* -> * -> *) -> * -> * -> * where-  Nil   :: DiscreteDiagram (~>) Z ()-  (:::) :: (Category (~>), Category (Discrete n)) -        => Obj (~>) x -> DiscreteDiagram (~>) n xs -> DiscreteDiagram (~>) (S n) (x, xs)-  -type instance Dom (DiscreteDiagram (~>) n xs) = Discrete n-type instance Cod (DiscreteDiagram (~>) n xs) = (~>)-type instance DiscreteDiagram (~>) (S n) (x, xs) :% Z = x-type instance DiscreteDiagram (~>) (S n) (x, xs) :% (S a) = DiscreteDiagram (~>) n xs :% a---- | The empty diagram.-instance Category (~>) => Functor (DiscreteDiagram (~>) Z ()) where-  Nil        % f = magicZ f---- | A diagram with one more object.-instance Functor (DiscreteDiagram (~>) n xs) => Functor (DiscreteDiagram (~>) (S n) (x, xs)) where-  (x ::: _)  % Z   = x-  (_ ::: xs) % S n = xs % n----- | Natural transformations in 'Void' are trivial.-voidNat :: (Functor f, Functor g, Category d, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d)-  => f -> g -> Nat Void d f g-voidNat f g = Nat f g magicZ

@@ -0,0 +1,65 @@+{-# LANGUAGE TypeOperators, TypeFamilies, UndecidableInstances, NoImplicitPrelude #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.AddObject+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category.Fix where+  +import Data.Category+import Data.Category.Functor+import Data.Category.Limit++import Data.Category.Unit+import Data.Category.Coproduct+++newtype Fix f a b = Fix (f (Fix f) a b)++-- | @`Fix` f@ is the fixed point category for a category combinator `f`.+instance Category (f (Fix f)) => Category (Fix f) where+  src (Fix a) = Fix (src a)+  tgt (Fix a) = Fix (tgt a)+  Fix a . Fix b = Fix (a . b)++-- | @Fix f@ inherits its (co)limits from @f (Fix f)@.+instance HasInitialObject (f (Fix f)) => HasInitialObject (Fix f) where+  type InitialObject (Fix f) = InitialObject (f (Fix f))+  initialObject = Fix initialObject+  initialize (Fix o) = Fix (initialize o)++-- | @Fix f@ inherits its (co)limits from @f (Fix f)@.+instance HasTerminalObject (f (Fix f)) => HasTerminalObject (Fix f) where+  type TerminalObject (Fix f) = TerminalObject (f (Fix f))+  terminalObject = Fix terminalObject+  terminate (Fix o) = Fix (terminate o)++type instance BinaryProduct (Fix f) a b = BinaryProduct (f (Fix f)) a b+-- | @Fix f@ inherits its (co)limits from @f (Fix f)@.+instance HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f) where+  proj1 (Fix a) (Fix b) = Fix (proj1 a b)+  proj2 (Fix a) (Fix b) = Fix (proj2 a b)+  Fix a &&& Fix b = Fix (a &&& b)+  +type instance BinaryCoproduct (Fix f) a b = BinaryCoproduct (f (Fix f)) a b+-- | @Fix f@ inherits its (co)limits from @f (Fix f)@.+instance HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f) where+  inj1 (Fix a) (Fix b) = Fix (inj1 a b)+  inj2 (Fix a) (Fix b) = Fix (inj2 a b)+  Fix a ||| Fix b = Fix (a ||| b)++data Wrap (f :: (* -> * -> *) -> * -> * -> *) = Wrap+type instance Dom (Wrap f) = f (Fix f)+type instance Cod (Wrap f) = Fix f+type instance Wrap f :% a = a+-- | The `Wrap` functor wraps `Fix` around @f (Fix f)@.+instance Category (f (Fix f)) => Functor (Wrap f) where+  Wrap % f = Fix f++-- | Take the `Omega` category, add a new disctinct object, and an arrow from that object to every object in `Omega`,+--   and you get `Omega` again.+type Omega = Fix ((:>>:) Unit)

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleContexts, FlexibleInstances, UndecidableInstances, GADTs, RankNTypes #-}+{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleContexts, FlexibleInstances, UndecidableInstances, GADTs, RankNTypes, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Functor@@ -27,7 +27,6 @@   , Opposite(..)   , OpOp(..)   , OpOpInv(..)-  , EndoHask(..)      -- *** Related to the product category   , Proj1(..)@@ -46,9 +45,6 @@    ) where   -import Prelude hiding ((.), Functor)-import qualified Prelude-   import Data.Category import Data.Category.Product @@ -87,14 +83,14 @@   -data Id ((~>) :: * -> * -> *) = Id+data Id (k :: * -> * -> *) = Id -type instance Dom (Id (~>)) = (~>)-type instance Cod (Id (~>)) = (~>)-type instance Id (~>) :% a = a+type instance Dom (Id k) = k+type instance Cod (Id k) = k+type instance Id k :% a = a --- | The identity functor on (~>)-instance Category (~>) => Functor (Id (~>)) where +-- | The identity functor on k+instance Category k => Functor (Id k) where    _ % f = f  @@ -134,43 +130,31 @@  -- | The dual of a functor instance (Category (Dom f), Category (Cod f)) => Functor (Opposite f) where-  Opposite f % Op a = Op $ f % a+  Opposite f % Op a = Op (f % a)  -data OpOp ((~>) :: * -> * -> *) = OpOp+data OpOp (k :: * -> * -> *) = OpOp -type instance Dom (OpOp (~>)) = Op (Op (~>))-type instance Cod (OpOp (~>)) = (~>)-type instance OpOp (~>) :% a = a+type instance Dom (OpOp k) = Op (Op k)+type instance Cod (OpOp k) = k+type instance OpOp k :% a = a  -- | The @Op (Op x) = x@ functor.-instance Category (~>) => Functor (OpOp (~>)) where+instance Category k => Functor (OpOp k) where   OpOp % Op (Op f) = f  -data OpOpInv ((~>) :: * -> * -> *) = OpOpInv+data OpOpInv (k :: * -> * -> *) = OpOpInv -type instance Dom (OpOpInv (~>)) = (~>)-type instance Cod (OpOpInv (~>)) = Op (Op (~>))-type instance OpOpInv (~>) :% a = a+type instance Dom (OpOpInv k) = k+type instance Cod (OpOpInv k) = Op (Op k)+type instance OpOpInv k :% a = a  -- | The @x = Op (Op x)@ functor.-instance Category (~>) => Functor (OpOpInv (~>)) where+instance Category k => Functor (OpOpInv k) where   OpOpInv % f = Op (Op f)  -data EndoHask :: (* -> *) -> * where-  EndoHask :: Prelude.Functor f => EndoHask f-  -type instance Dom (EndoHask f) = (->)-type instance Cod (EndoHask f) = (->)-type instance EndoHask f :% r = f r---- | 'EndoHask' is a wrapper to turn instances of the 'Functor' class into categorical functors.-instance Functor (EndoHask f) where-  EndoHask % f = fmap f-- data Proj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj1  type instance Dom (Proj1 c1 c2) = c1 :**: c2@@ -204,14 +188,14 @@   (g1 :***: g2) % (f1 :**: f2) = (g1 % f1) :**: (g2 % f2)      -data DiagProd ((~>) :: * -> * -> *) = DiagProd+data DiagProd (k :: * -> * -> *) = DiagProd -type instance Dom (DiagProd (~>)) = (~>)-type instance Cod (DiagProd (~>)) = (~>) :**: (~>)-type instance DiagProd (~>) :% a = (a, a)+type instance Dom (DiagProd k) = k+type instance Cod (DiagProd k) = k :**: k+type instance DiagProd k :% a = (a, a)  -- | 'DiagProd' is the diagonal functor for products.-instance Category (~>) => Functor (DiagProd (~>)) where +instance Category k => Functor (DiagProd k) where    DiagProd % f = f :**: f  @@ -237,23 +221,23 @@   Tuple2 a % f = f :**: a  -data Hom ((~>) :: * -> * -> *) = Hom  +data Hom (k :: * -> * -> *) = Hom   -type instance Dom (Hom (~>)) = Op (~>) :**: (~>)-type instance Cod (Hom (~>)) = (->)-type instance (Hom (~>)) :% (a1, a2) = a1 ~> a2+type instance Dom (Hom k) = Op k :**: k+type instance Cod (Hom k) = (->)+type instance (Hom k) :% (a1, a2) = k a1 a2  -- | The Hom functor, Hom(--,--), a bifunctor contravariant in its first argument and covariant in its second argument.-instance Category (~>) => Functor (Hom (~>)) where +instance Category k => Functor (Hom k) where    Hom % (Op f1 :**: f2) = \g -> f2 . g . f1  -type x :*-: (~>) = Hom (~>) :.: Tuple1 (Op (~>)) (~>) x+type x :*-: k = Hom k :.: Tuple1 (Op k) k x -- | The covariant functor Hom(X,--)-homX_ :: Category (~>) => Obj (~>) x -> x :*-: (~>)+homX_ :: Category k => Obj k x -> x :*-: k homX_ x = Hom :.: Tuple1 (Op x) -type (~>) :-*: x = Hom (~>) :.: Tuple2 (Op (~>)) (~>) x+type k :-*: x = Hom k :.: Tuple2 (Op k) k x -- | The contravariant functor Hom(--,X)-hom_X :: Category (~>) => Obj (~>) x -> (~>) :-*: x+hom_X :: Category k => Obj k x -> k :-*: x hom_X x = Hom :.: Tuple2 x

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleInstances, FlexibleContexts, RankNTypes, ScopedTypeVariables, UndecidableInstances  #-}+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleInstances, FlexibleContexts, RankNTypes, ScopedTypeVariables, UndecidableInstances, NoImplicitPrelude  #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Kleisli@@ -13,8 +13,6 @@ ----------------------------------------------------------------------------- module Data.Category.Kleisli where   -import Prelude hiding ((.), id, Functor(..), Monad(..))- import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation@@ -23,10 +21,10 @@   data Kleisli m a b where-  Kleisli :: (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Monad m -> Obj (~>) b -> a ~> (m :% b) -> Kleisli m a b+  Kleisli :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Obj k b -> k a (m :% b) -> Kleisli m a b -kleisliId :: (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Monad m -> Obj (~>) a -> Kleisli m a a-kleisliId m a = Kleisli m a $ unit m ! a+kleisliId :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Obj k a -> Kleisli m a a+kleisliId m a = Kleisli m a (unit m ! a)  -- | The category of Kleisli arrows. instance Category (Kleisli m) where@@ -34,7 +32,7 @@   src (Kleisli m _ f) = kleisliId m (src f)   tgt (Kleisli m b _) = kleisliId m b   -  (Kleisli m c f) . (Kleisli _ _ g) = Kleisli m c $ (multiply m ! c) . (monadFunctor m % f) . g+  (Kleisli m c f) . (Kleisli _ _ g) = Kleisli m c ((multiply m ! c) . (monadFunctor m % f) . g)   @@ -42,18 +40,18 @@ type instance Dom (KleisliAdjF m) = Dom m type instance Cod (KleisliAdjF m) = Kleisli m type instance KleisliAdjF m :% a = a-instance (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (KleisliAdjF m) where-  KleisliAdjF m % f = Kleisli m (tgt f) $ (unit m ! tgt f) . f+instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliAdjF m) where+  KleisliAdjF m % f = Kleisli m (tgt f) ((unit m ! tgt f) . f)     data KleisliAdjG m = KleisliAdjG (Monad m) type instance Dom (KleisliAdjG m) = Kleisli m type instance Cod (KleisliAdjG m) = Dom m type instance KleisliAdjG m :% a = m :% a-instance (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (KleisliAdjG m) where+instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliAdjG m) where   KleisliAdjG m % Kleisli _ b f = (multiply m ! b) . (monadFunctor m % f) -kleisliAdj :: (Functor m, Dom m ~ (~>), Cod m ~ (~>)) -  => Monad m -> A.Adjunction (Kleisli m) (~>) (KleisliAdjF m) (KleisliAdjG m)+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)   (\x -> unit m ! x)-  (\(Kleisli _ x _) -> Kleisli m x $ monadFunctor m % x)+  (\(Kleisli _ x _) -> Kleisli m x (monadFunctor m % x))

@@ -8,7 +8,9 @@   TypeOperators,    TypeFamilies,   TypeSynonymInstances,-  UndecidableInstances  #-}+  UndecidableInstances, +  LambdaCase,+  NoImplicitPrelude  #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Limit@@ -67,9 +69,6 @@    ) where -import Prelude hiding ((.), Functor, product)-import qualified Control.Arrow as A ((&&&), (***), (|||), (+++))- import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation@@ -77,7 +76,8 @@  import Data.Category.Product import Data.Category.Coproduct-import Data.Category.Discrete+import Data.Category.Unit+import Data.Category.Void  infixl 3 *** infixl 3 &&&@@ -86,15 +86,15 @@   data Diag :: (* -> * -> *) -> (* -> * -> *) -> * where-  Diag :: Diag j (~>)+  Diag :: Diag j k   -type instance Dom (Diag j (~>)) = (~>)-type instance Cod (Diag j (~>)) = Nat j (~>)-type instance Diag j (~>) :% a = Const j (~>) a+type instance Dom (Diag j k) = k+type instance Cod (Diag j k) = Nat j k+type instance Diag j k :% a = Const j k a --- | The diagonal functor from (index-) category J to (~>).-instance (Category j, Category (~>)) => Functor (Diag j (~>)) where -  Diag % f = Nat (Const $ src f) (Const $ tgt f) $ const f+-- | The diagonal functor from (index-) category J to k.+instance (Category j, Category k) => Functor (Diag j k) where +  Diag % f = Nat (Const (src f)) (Const (tgt f)) (\_ -> f)  -- | The diagonal functor with the same domain and codomain as @f@. type DiagF f = Diag (Dom f) (Cod f)@@ -118,77 +118,77 @@   --- | Limits in a category @(~>)@ by means of a diagram of type @j@, which is a functor from @j@ to @(~>)@.-type family LimitFam j (~>) f :: *+-- | Limits in a category @k@ by means of a diagram of type @j@, which is a functor from @j@ to @k@.+type family LimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *  type Limit f = LimitFam (Dom f) (Cod f) f --- | An instance of @HasLimits j (~>)@ says that @(~>)@ has all limits of type @j@.-class (Category j, Category (~>)) => HasLimits j (~>) where+-- | An instance of @HasLimits j k@ says that @k@ has all limits of type @j@.+class (Category j, Category k) => HasLimits j k where   -- | 'limit' returns the limiting cone for a functor @f@.-  limit           :: Obj (Nat j (~>)) f -> Cone f (Limit f)+  limit           :: Obj (Nat j k) f -> Cone f (Limit f)   -- | 'limitFactorizer' shows that the limiting cone is universal – i.e. any other cone of @f@ factors through it –   --   by returning the morphism between the vertices of the cones.-  limitFactorizer :: Obj (Nat j (~>)) f -> (forall n. Cone f n -> n ~> Limit f)+  limitFactorizer :: Obj (Nat j k) f -> (forall n. Cone f n -> k n (Limit f)) -data LimitFunctor (j :: * -> * -> *) ((~>)  :: * -> * -> *) = LimitFunctor-type instance Dom (LimitFunctor j (~>)) = Nat j (~>)-type instance Cod (LimitFunctor j (~>)) = (~>)-type instance LimitFunctor j (~>) :% f = LimitFam j (~>) f--- | If every diagram of type @j@ has a limit in @(~>)@ there exists a limit functor.+data LimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = LimitFunctor+type instance Dom (LimitFunctor j k) = Nat j k+type instance Cod (LimitFunctor j k) = k+type instance LimitFunctor j k :% f = LimitFam j k f+-- | 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 (~>) => Functor (LimitFunctor j (~>)) where+instance HasLimits j k => Functor (LimitFunctor j k) where   LimitFunctor % n @ Nat{}  = limitFactorizer (tgt n) (n . limit (src n))  -- | The limit functor is right adjoint to the diagonal functor.-limitAdj :: HasLimits j (~>) => Adjunction (Nat j (~>)) (~>) (Diag j (~>)) (LimitFunctor j (~>))+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)-  where diag = Diag -- Forces the type of all Diags to be the same.+  where diag = Diag :: Diag j k -- Forces the type of all Diags to be the same.   --- | Colimits in a category @(~>)@ by means of a diagram of type @j@, which is a functor from @j@ to @(~>)@.-type family ColimitFam j (~>) f :: *+-- | 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 :: *) :: *  type Colimit f = ColimitFam (Dom f) (Cod f) f --- | An instance of @HasColimits j (~>)@ says that @(~>)@ has all colimits of type @j@.-class (Category j, Category (~>)) => HasColimits j (~>) where+-- | An instance of @HasColimits j k@ says that @k@ has all colimits of type @j@.+class (Category j, Category k) => HasColimits j k where   -- | 'colimit' returns the limiting co-cone for a functor @f@.-  colimit           :: Obj (Nat j (~>)) f -> Cocone f (Colimit f)+  colimit           :: Obj (Nat j k) f -> Cocone f (Colimit f)   -- | 'colimitFactorizer' shows that the limiting co-cone is universal – i.e. any other co-cone of @f@ factors through it –   --   by returning the morphism between the vertices of the cones.-  colimitFactorizer :: Obj (Nat j (~>)) f -> (forall n. Cocone f n -> Colimit f ~> n)+  colimitFactorizer :: Obj (Nat j k) f -> (forall n. Cocone f n -> k (Colimit f) n) -data ColimitFunctor (j :: * -> * -> *) ((~>)  :: * -> * -> *) = ColimitFunctor-type instance Dom (ColimitFunctor j (~>)) = Nat j (~>)-type instance Cod (ColimitFunctor j (~>)) = (~>)-type instance ColimitFunctor j (~>) :% f = ColimitFam j (~>) f--- | If every diagram of type @j@ has a colimit in @(~>)@ there exists a colimit functor.+data ColimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = ColimitFunctor+type instance Dom (ColimitFunctor j k) = Nat j k+type instance Cod (ColimitFunctor j k) = k+type instance ColimitFunctor j k :% f = ColimitFam j k f+-- | 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 (~>) => Functor (ColimitFunctor j (~>)) where+instance HasColimits j k => Functor (ColimitFunctor j k) where   ColimitFunctor % n @ Nat{}  = colimitFactorizer (src n) (colimit (tgt n) . n)  -- | The colimit functor is left adjoint to the diagonal functor.-colimitAdj :: HasColimits j (~>) => Adjunction (~>) (Nat j (~>)) (ColimitFunctor j (~>)) (Diag j (~>))+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)) -  where diag = Diag -- Forces the type of all Diags to be the same.+  where diag = Diag :: Diag j k -- Forces the type of all Diags to be the same.     -class Category (~>) => HasTerminalObject (~>) where+class Category k => HasTerminalObject k where   -  type TerminalObject (~>) :: *+  type TerminalObject k :: *   -  terminalObject :: Obj (~>) (TerminalObject (~>))+  terminalObject :: Obj k (TerminalObject k)   -  terminate :: Obj (~>) a -> a ~> TerminalObject (~>)+  terminate :: Obj k a -> k a (TerminalObject k)  -type instance LimitFam Void (~>) f = TerminalObject (~>)+type instance LimitFam Void k f = TerminalObject k --- | A terminal object is the limit of the functor from /0/ to (~>).-instance (HasTerminalObject (~>)) => HasLimits Void (~>) where+-- | A terminal object is the limit of the functor from /0/ to k.+instance (HasTerminalObject k) => HasLimits Void k where      limit (Nat f _ _) = voidNat (Const terminalObject) f   limitFactorizer Nat{} = terminate . coneVertex@@ -199,7 +199,7 @@      type TerminalObject (->) = ()   -  terminalObject = id+  terminalObject = \x -> x      terminate _ _ = () @@ -210,17 +210,26 @@      terminalObject = CatA Id   -  terminate (CatA _) = CatA $ Const Z+  terminate (CatA _) = CatA (Const Unit)  -- | The constant functor to the terminal object is itself the terminal object in its functor category. instance (Category c, HasTerminalObject d) => HasTerminalObject (Nat c d) where      type TerminalObject (Nat c d) = Const c d (TerminalObject d)   -  terminalObject = natId $ Const terminalObject+  terminalObject = natId (Const terminalObject)   -  terminate (Nat f _ _) = Nat f (Const terminalObject) $ terminate . (f %)+  terminate (Nat f _ _) = Nat f (Const terminalObject) (terminate . (f %)) +-- | The category of one object has that object as terminal object.+instance HasTerminalObject Unit where+  +  type TerminalObject Unit = ()+  +  terminalObject = Unit+  +  terminate Unit = Unit+   -- | The terminal object of the product of 2 categories is the product of their terminal objects. instance (HasTerminalObject c1, HasTerminalObject c2) => HasTerminalObject (c1 :**: c2) where   @@ -230,21 +239,31 @@      terminate (a1 :**: a2) = terminate a1 :**: terminate a2   +-- | The terminal object of the direct coproduct of categories is the terminal object of the terminal category.+instance (Category c1, HasTerminalObject c2) => HasTerminalObject (c1 :>>: c2) where   +  type TerminalObject (c1 :>>: c2) = I2 (TerminalObject c2)+  +  terminalObject = I2A terminalObject+  +  terminate (I1A a) = I12 a terminalObject+  terminate (I2A a) = I2A (terminate a) -class Category (~>) => HasInitialObject (~>) where+++class Category k => HasInitialObject k where   -  type InitialObject (~>) :: *+  type InitialObject k :: *   -  initialObject :: Obj (~>) (InitialObject (~>))+  initialObject :: Obj k (InitialObject k) -  initialize :: Obj (~>) a -> InitialObject (~>) ~> a+  initialize :: Obj k a -> k (InitialObject k) a  -type instance ColimitFam Void (~>) f = InitialObject (~>)+type instance ColimitFam Void k f = InitialObject k --- | An initial object is the colimit of the functor from /0/ to (~>).-instance HasInitialObject (~>) => HasColimits Void (~>) where+-- | An initial object is the colimit of the functor from /0/ to k.+instance HasInitialObject k => HasColimits Void k where      colimit (Nat f _ _) = voidNat f (Const initialObject)   colimitFactorizer Nat{} = initialize . coconeVertex@@ -257,10 +276,9 @@      type InitialObject (->) = Zero   -  initialObject = id+  initialObject = \x -> x   -  -- With thanks to Conor McBride-  initialize _ x = x `seq` error "we never get this far"+  initialize = initialize  -- | The empty category is the initial object in @Cat@. instance HasInitialObject Cat where@@ -269,16 +287,16 @@      initialObject = CatA Id   -  initialize (CatA _) = CatA Nil+  initialize (CatA _) = CatA Magic  -- | The constant functor to the initial object is itself the initial object in its functor category. instance (Category c, HasInitialObject d) => HasInitialObject (Nat c d) where      type InitialObject (Nat c d) = Const c d (InitialObject d)   -  initialObject = natId $ Const initialObject+  initialObject = natId (Const initialObject)   -  initialize (Nat f _ _) = Nat (Const initialObject) f $ initialize . (f %)+  initialize (Nat f _ _) = Nat (Const initialObject) f (initialize . (f %))  -- | The initial object of the product of 2 categories is the product of their initial objects. instance (HasInitialObject c1, HasInitialObject c2) => HasInitialObject (c1 :**: c2) where@@ -289,38 +307,63 @@      initialize (a1 :**: a2) = initialize a1 :**: initialize a2 +-- | The category of one object has that object as initial object. +instance HasInitialObject Unit where+  +  type InitialObject Unit = ()+  +  initialObject = Unit+  +  initialize Unit = Unit +-- | The initial object of the direct coproduct of categories is the initial object of the initial category.+instance (HasInitialObject c1, Category c2) => HasInitialObject (c1 :>>: c2) where+  +  type InitialObject (c1 :>>: c2) = I1 (InitialObject c1)+  +  initialObject = I1A initialObject+  +  initialize (I1A a) = I1A (initialize a)+  initialize (I2A a) = I12 initialObject a -type family BinaryProduct ((~>) :: * -> * -> *) x y :: * -class Category (~>) => HasBinaryProducts (~>) where+type family BinaryProduct (k :: * -> * -> *) x y :: *++class Category k => HasBinaryProducts k where   -  proj1 :: Obj (~>) x -> Obj (~>) y -> BinaryProduct (~>) x y ~> x-  proj2 :: Obj (~>) x -> Obj (~>) y -> BinaryProduct (~>) x y ~> y+  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 -  (&&&) :: (a ~> x) -> (a ~> y) -> (a ~> BinaryProduct (~>) x y)+  (&&&) :: (k a x) -> (k a y) -> (k a (BinaryProduct k x y)) -  (***) :: (a1 ~> b1) -> (a2 ~> b2) -> (BinaryProduct (~>) a1 a2 ~> BinaryProduct (~>) 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)) -type instance LimitFam (Discrete (S n)) (~>) f = BinaryProduct (~>) (f :% Z) (LimitFam (Discrete n) (~>) (f :.: Succ n)) --- | The product of @n@ objects is the limit of the functor from @Discrete n@ to @(~>)@.-instance (HasLimits (Discrete n) (~>), HasBinaryProducts (~>)) => HasLimits (Discrete (S n)) (~>) where+type instance LimitFam (i :++: j) k f = BinaryProduct k +  (LimitFam i k (f :.: Inj1 i j))+  (LimitFam j k (f :.: Inj2 i j))++-- | If `k` has binary products, we can take the limit of 2 joined diagrams.+instance (HasLimits i k, HasLimits j k, HasBinaryProducts k) => HasLimits (i :++: j) k where      limit = limit'     where-      limit' :: forall f. Obj (Nat (Discrete (S n)) (~>)) f -> Cone f (Limit f)-      limit' l@Nat{} = Nat (Const $ x *** y) (srcF l) (\z -> unCom $ h z)+      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))         where-          x = l ! Z-          y = coneVertex limNext-          limNext = limit (l `o` natId Succ)-          h :: Obj (Discrete (S n)) z -> Com (ConstF f (LimitFam (Discrete (S n)) (~>) f)) f z-          h Z     = Com $               proj1 x y-          h (S n) = Com $ limNext ! n . proj2 x y+          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) -  limitFactorizer l@Nat{} c = c ! Z &&& limitFactorizer (l `o` natId Succ) ((c `o` natId Succ) . constPostcompInv (srcF c) Succ)+  limitFactorizer l@Nat{} c = +    limitFactorizer (l `o` natId Inj1) ((c `o` natId Inj1) . constPostcompInv (srcF c) Inj1)+    &&& +    limitFactorizer (l `o` natId Inj2) ((c `o` natId Inj2) . constPostcompInv (srcF c) Inj2)   type instance BinaryProduct (->) x y = (x, y)@@ -328,15 +371,15 @@ -- | The tuple is the binary product in @Hask@. instance HasBinaryProducts (->) where   -  proj1 _ _ = fst-  proj2 _ _ = snd+  proj1 _ _ = \(x, _) -> x+  proj2 _ _ = \(_, y) -> y   -  (&&&) = (A.&&&)-  (***) = (A.***)+  f &&& g = \x -> (f x, g x)+  f *** g = \(x, y) -> (f x, g y)  type instance BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :**: c2) --- | The product of categories '(:**:)' is the binary product in 'Cat'.+-- | The product of categories ':**:' is the binary product in 'Cat'. instance HasBinaryProducts Cat where      proj1 (CatA _) (CatA _) = CatA Proj1@@ -345,6 +388,17 @@   CatA f1 &&& CatA f2 = CatA ((f1 :***: f2) :.: DiagProd)   CatA f1 *** CatA f2 = CatA (f1 :***: f2) +type instance BinaryProduct Unit () () = ()++-- | In the category of one object that object is its own product.+instance HasBinaryProducts Unit where++  proj1 Unit Unit = Unit+  proj2 Unit Unit = Unit+  +  Unit &&& Unit = Unit+  Unit *** Unit = Unit+ type instance BinaryProduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryProduct c1 x1 y1, BinaryProduct c2 x2 y2)  -- | The binary product of the product of 2 categories is the product of their binary products.@@ -356,17 +410,39 @@   (f1 :**: f2) &&& (g1 :**: g2) = (f1 &&& g1) :**: (f2 &&& g2)   (f1 :**: f2) *** (g1 :**: g2) = (f1 *** g1) :**: (f2 *** g2) +type instance BinaryProduct (c1 :>>: c2) (I1 a) (I1 b) = I1 (BinaryProduct c1 a b)+type instance BinaryProduct (c1 :>>: c2) (I1 a) (I2 b) = I1 a+type instance BinaryProduct (c1 :>>: c2) (I2 a) (I1 b) = I1 b+type instance BinaryProduct (c1 :>>: c2) (I2 a) (I2 b) = I2 (BinaryProduct c2 a b) -data ProductFunctor ((~>) :: * -> * -> *) = ProductFunctor-type instance Dom (ProductFunctor (~>)) = (~>) :**: (~>)-type instance Cod (ProductFunctor (~>)) = (~>)-type instance ProductFunctor (~>) :% (a, b) = BinaryProduct (~>) a b+instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :>>: c2) where++  proj1 (I1A a) (I1A b) = I1A (proj1 a b)+  proj1 (I1A a) (I2A _) = I1A a+  proj1 (I2A a) (I1A b) = I12 b a+  proj1 (I2A a) (I2A b) = I2A (proj1 a b)+  +  proj2 (I1A a) (I1A b) = I1A (proj2 a b)+  proj2 (I1A a) (I2A b) = I12 a b+  proj2 (I2A _) (I1A b) = I1A b+  proj2 (I2A a) (I2A b) = I2A (proj2 a b)++  I1A a &&& I1A b = I1A (a &&& b)+  I1A a &&& I12 _ _ = I1A a+  I12 _ _ &&& I1A b = I1A b+  I2A a &&& I2A b = I2A (a &&& b)+++data ProductFunctor (k :: * -> * -> *) = ProductFunctor+type instance Dom (ProductFunctor k) = k :**: k+type instance Cod (ProductFunctor k) = k+type instance ProductFunctor k :% (a, b) = BinaryProduct k a b -- | Binary product as a bifunctor.-instance HasBinaryProducts (~>) => Functor (ProductFunctor (~>)) where+instance HasBinaryProducts k => Functor (ProductFunctor k) where   ProductFunctor % (a1 :**: a2) = a1 *** a2  data p :*: q where -  (:*:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ (~>), Cod q ~ (~>), HasBinaryProducts (~>)) => p -> q -> p :*: q+  (:*:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryProducts k) => p -> q -> p :*: q type instance Dom (p :*: q) = Dom p type instance Cod (p :*: q) = Cod p type instance (p :*: q) :% a = BinaryProduct (Cod p) (p :% a) (q :% a)@@ -376,64 +452,59 @@  type instance BinaryProduct (Nat c d) x y = x :*: y --- | The functor product '(:*:)' is the binary product in functor categories.+-- | The functor product ':*:' is the binary product in functor categories. instance (Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d) where   -  proj1 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) f $ \z -> proj1 (f % z) (g % z)-  proj2 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) g $ \z -> proj2 (f % z) (g % z)+  proj1 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) f (\z -> proj1 (f % z) (g % z))+  proj2 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) g (\z -> proj2 (f % z) (g % z))   -  Nat a f af &&& Nat _ g ag = Nat a (f :*: g) $ \z -> af z &&& ag z-  Nat f1 f2 f *** Nat g1 g2 g = Nat (f1 :*: g1) (f2 :*: g2) $ \z -> f z *** g z+  Nat a f af &&& Nat _ g ag = Nat a (f :*: g) (\z -> af z &&& ag z)+  Nat f1 f2 f *** Nat g1 g2 g = Nat (f1 :*: g1) (f2 :*: g2) (\z -> f z *** g z)       -type family BinaryCoproduct ((~>) :: * -> * -> *) x y :: *+type family BinaryCoproduct (k :: * -> * -> *) x y :: * -class Category (~>) => HasBinaryCoproducts (~>) where+class Category k => HasBinaryCoproducts k where -  inj1 :: Obj (~>) x -> Obj (~>) y -> x ~> BinaryCoproduct (~>) x y-  inj2 :: Obj (~>) x -> Obj (~>) y -> y ~> BinaryCoproduct (~>) x y+  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) -  (|||) :: (x ~> a) -> (y ~> a) -> (BinaryCoproduct (~>) x y ~> a)+  (|||) :: (k x a) -> (k y a) -> (k (BinaryCoproduct k x y) a)     -  (+++) :: (a1 ~> b1) -> (a2 ~> b2) -> (BinaryCoproduct (~>) a1 a2 ~> BinaryCoproduct (~>) 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)      -type instance ColimitFam (Discrete (S n)) (~>) f = BinaryCoproduct (~>) (f :% Z) (ColimitFam (Discrete n) (~>) (f :.: Succ n))+type instance ColimitFam (i :++: j) k f = BinaryCoproduct k +  (ColimitFam i k (f :.: Inj1 i j))+  (ColimitFam j k (f :.: Inj2 i j)) --- | The coproduct of @n@ objects is the colimit of the functor from @Discrete n@ to @(~>)@.-instance (HasColimits (Discrete n) (~>), HasBinaryCoproducts (~>)) => HasColimits (Discrete (S n)) (~>) where+-- | If `k` has binary coproducts, we can take the colimit of 2 joined diagrams.+instance (HasColimits i k, HasColimits j k, HasBinaryCoproducts k) => HasColimits (i :++: j) k where      colimit = colimit'     where-      colimit' :: forall f. Obj (Nat (Discrete (S n)) (~>)) f -> Cocone f (Colimit f)-      colimit' l@Nat{} = Nat (srcF l) (Const $ x +++ y) (\z -> unCom $ h z)+      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))         where-          x = l ! Z-          y = coconeVertex colNext-          colNext = colimit (l `o` natId Succ)-          h :: Obj (Discrete (S n)) z -> Com f (ConstF f (ColimitFam (Discrete (S n)) (~>) f)) z-          h Z     = Com $ inj1 x y-          h (S n) = Com $ inj2 x y . colNext ! n+          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)   -  colimitFactorizer l@Nat{} c = c ! Z ||| colimitFactorizer (l `o` natId Succ) (constPostcomp (tgtF c) Succ . (c `o` natId Succ))+  colimitFactorizer l@Nat{} c = +    colimitFactorizer (l `o` natId Inj1) (constPostcomp (tgtF c) Inj1 . (c `o` natId Inj1))+    ||| +    colimitFactorizer (l `o` natId Inj2) (constPostcomp (tgtF c) Inj2 . (c `o` natId Inj2))  -type instance BinaryCoproduct (->) x y = Either x y---- | 'Either' is the coproduct in @Hask@.-instance HasBinaryCoproducts (->) where-  -  inj1 _ _ = Left-  inj2 _ _ = Right-  -  (|||) = (A.|||)-  (+++) = (A.+++)- type instance BinaryCoproduct Cat (CatW c1) (CatW c2) = CatW (c1 :++: c2) --- | The coproduct of categories '(:++:)' is the binary coproduct in 'Cat'.+-- | The coproduct of categories ':++:' is the binary coproduct in 'Cat'. instance HasBinaryCoproducts Cat where      inj1 (CatA _) (CatA _) = CatA Inj1@@ -442,6 +513,17 @@   CatA f1 ||| CatA f2 = CatA (CodiagCoprod :.: (f1 :+++: f2))   CatA f1 +++ CatA f2 = CatA (f1 :+++: f2) +type instance BinaryCoproduct Unit () () = ()++-- | In the category of one object that object is its own coproduct.+instance HasBinaryCoproducts Unit where+  +  inj1 Unit Unit = Unit+  inj2 Unit Unit = Unit+  +  Unit ||| Unit = Unit+  Unit +++ Unit = Unit+   type instance BinaryCoproduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryCoproduct c1 x1 y1, BinaryCoproduct c2 x2 y2)  -- | The binary coproduct of the product of 2 categories is the product of their binary coproducts.@@ -453,17 +535,39 @@   (f1 :**: f2) ||| (g1 :**: g2) = (f1 ||| g1) :**: (f2 ||| g2)   (f1 :**: f2) +++ (g1 :**: g2) = (f1 +++ g1) :**: (f2 +++ g2) +type instance BinaryCoproduct (c1 :>>: c2) (I1 a) (I1 b) = I1 (BinaryCoproduct c1 a b)+type instance BinaryCoproduct (c1 :>>: c2) (I1 a) (I2 b) = I2 b+type instance BinaryCoproduct (c1 :>>: c2) (I2 a) (I1 b) = I2 a+type instance BinaryCoproduct (c1 :>>: c2) (I2 a) (I2 b) = I2 (BinaryCoproduct c2 a b) -data CoproductFunctor ((~>) :: * -> * -> *) = CoproductFunctor-type instance Dom (CoproductFunctor (~>)) = (~>) :**: (~>)-type instance Cod (CoproductFunctor (~>)) = (~>)-type instance CoproductFunctor (~>) :% (a, b) = BinaryCoproduct (~>) a b+instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :>>: c2) where++  inj1 (I1A a) (I1A b) = I1A (inj1 a b)+  inj1 (I1A a) (I2A b) = I12 a b+  inj1 (I2A a) (I1A _) = I2A a+  inj1 (I2A a) (I2A b) = I2A (inj1 a b)++  inj2 (I1A a) (I1A b) = I1A (inj2 a b)+  inj2 (I1A _) (I2A b) = I2A b+  inj2 (I2A a) (I1A b) = I12 b a+  inj2 (I2A a) (I2A b) = I2A (inj2 a b)++  I1A a ||| I1A b = I1A (a ||| b)+  I2A a ||| I12 _ _ = I2A a+  I12 _ _ ||| I2A b = I2A b+  I2A a ||| I2A b = I2A (a ||| b)+++data CoproductFunctor (k :: * -> * -> *) = CoproductFunctor+type instance Dom (CoproductFunctor k) = k :**: k+type instance Cod (CoproductFunctor k) = k+type instance CoproductFunctor k :% (a, b) = BinaryCoproduct k a b -- | Binary coproduct as a bifunctor.-instance HasBinaryCoproducts (~>) => Functor (CoproductFunctor (~>)) where+instance HasBinaryCoproducts k => Functor (CoproductFunctor k) where   CoproductFunctor % (a1 :**: a2) = a1 +++ a2  data p :+: q where -  (:+:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ (~>), Cod q ~ (~>), HasBinaryCoproducts (~>)) => p -> q -> p :+: q+  (:+:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryCoproducts k) => p -> q -> p :+: q type instance Dom (p :+: q) = Dom p type instance Cod (p :+: q) = Cod p type instance (p :+: q) :% a = BinaryCoproduct (Cod p) (p :% a) (q :% a)@@ -473,31 +577,75 @@  type instance BinaryCoproduct (Nat c d) x y = x :+: y --- | The functor coproduct '(:+:)' is the binary coproduct in functor categories.+-- | The functor coproduct ':+:' is the binary coproduct in functor categories. instance (Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d) where   -  inj1 (Nat f _ _) (Nat g _ _) = Nat f (f :+: g) $ \z -> inj1 (f % z) (g % z)-  inj2 (Nat f _ _) (Nat g _ _) = Nat g (f :+: g) $ \z -> inj2 (f % z) (g % z)+  inj1 (Nat f _ _) (Nat g _ _) = Nat f (f :+: g) (\z -> inj1 (f % z) (g % z))+  inj2 (Nat f _ _) (Nat g _ _) = Nat g (f :+: g) (\z -> inj2 (f % z) (g % z))   -  Nat f a fa ||| Nat g _ ga = Nat (f :+: g) a $ \z -> fa z ||| ga z-  Nat f1 f2 f +++ Nat g1 g2 g = Nat (f1 :+: g1) (f2 :+: g2) $ \z -> f z +++ g z+  Nat f a fa ||| Nat g _ ga = Nat (f :+: g) a (\z -> fa z ||| ga z)+  Nat f1 f2 f +++ Nat g1 g2 g = Nat (f1 :+: g1) (f2 :+: g2) (\z -> f z +++ g z) +-- | Terminal objects are the dual of initial objects.+instance HasInitialObject k => HasTerminalObject (Op k) where+  type TerminalObject (Op k) = InitialObject k+  terminalObject = Op initialObject+  terminate (Op f) = Op (initialize f) --- newtype ForAll f = ForAll { unForAll :: forall a. f :% a }--- --- type instance LimitFam (->) (->) f = ForAll f--- --- instance HasLimits (->) (->) where---   ---   limit (Nat f _ _) = Nat (Const id) f $ \_ -> unForAll---   limitFactorizer Nat{} c n = ForAll $ (c ! id) n -- ForAll . (c ! id)--- --- --- data Exists f = forall a. Exists (f :% a)--- --- type instance ColimitFam (->) (->) f = Exists f--- --- instance HasColimits (->) (->) where---   ---   colimit (Nat f _ _) = Nat f (Const id) $ \_ -> Exists---   colimitFactorizer Nat{} c (Exists fa) = (c ! id) fa -- (c ! id) . unExists+-- | Terminal objects are the dual of initial objects.+instance HasTerminalObject k => HasInitialObject (Op k) where+  type InitialObject (Op k) = TerminalObject k+  initialObject = Op terminalObject+  initialize (Op f) = Op (terminate f)++type instance BinaryProduct (Op k) x y = BinaryCoproduct k x y+-- | Binary products are the dual of binary coproducts.+instance HasBinaryCoproducts k => HasBinaryProducts (Op k) where+  proj1 (Op x) (Op y) = Op (inj1 x y)+  proj2 (Op x) (Op y) = Op (inj2 x y)+  Op f &&& Op g = Op (f ||| g)+  Op f *** Op g = Op (f +++ g)++type instance BinaryCoproduct (Op k) x y = BinaryProduct k x y+-- | Binary products are the dual of binary coproducts.+instance HasBinaryProducts k => HasBinaryCoproducts (Op k) where+  inj1 (Op x) (Op y) = Op (proj1 x y)+  inj2 (Op x) (Op y) = Op (proj2 x y)+  Op f ||| Op g = Op (f &&& g)+  Op f +++ Op g = Op (f *** g)+++++type instance LimitFam Unit k f = f :% ()++-- | The limit of a single object is that object.+instance Category k => HasLimits Unit k where+  +  limit (Nat f _ _) = Nat (Const (f % Unit)) f (\Unit -> f % Unit)+  limitFactorizer Nat{} n = n ! Unit++type instance LimitFam (i :>>: j) k f = f :% InitialObject (i :>>: j)++-- | The limit of any diagram with an initial object, has the limit at the initial object.+instance (HasInitialObject (i :>>: j), Category k) => HasLimits (i :>>: j) k where+  +  limit (Nat f _ _) = Nat (Const (f % initialObject)) f (\z -> f % initialize z)+  limitFactorizer Nat{} n = n ! initialObject+++type instance ColimitFam Unit k f = f :% ()++-- | The colimit of a single object is that object.+instance Category k => HasColimits Unit k where+  +  colimit (Nat f _ _) = Nat f (Const (f % Unit)) (\Unit -> f % Unit)+  colimitFactorizer Nat{} n = n ! Unit+  +type instance ColimitFam (i :>>: j) k f = f :% TerminalObject (i :>>: j)++-- | The colimit of any diagram with a terminal object, has the limit at the terminal object.+instance (HasTerminalObject (i :>>: j), Category k) => HasColimits (i :>>: j) k where++  colimit (Nat f _ _) = Nat f (Const (f % terminalObject)) (\z -> f % terminate z)+  colimitFactorizer Nat{} n = n ! terminalObject

@@ -1,82 +0,0 @@-{-# LANGUAGE TypeFamilies, GADTs, FlexibleInstances #-}--------------------------------------------------------------------------------- |--- Module      :  Data.Category.Monoid--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  sjoerd@w3future.com--- Stability   :  experimental--- Portability :  non-portable------ A monoid as a category with one object.-------------------------------------------------------------------------------module Data.Category.Monoid where--import Prelude hiding ((.), Functor)-import Data.Monoid--import Data.Category-import Data.Category.Functor-import Data.Category.NaturalTransformation-import Data.Category.Adjunction-import Data.Category.Monoidal as M---- | The arrows are the values of the monoid.-data MonoidA m a b where-  MonoidA :: Monoid m => m -> MonoidA m m m---- | A (prelude) monoid as a category with one object.-instance Monoid m => Category (MonoidA m) where-  -  src (MonoidA _) = MonoidA mempty-  tgt (MonoidA _) = MonoidA mempty-  -  MonoidA a . MonoidA b = MonoidA $ a `mappend` b---data Mon :: * -> * -> * where-  MonoidMorphism :: (Monoid m1, Monoid m2) => (m1 -> m2) -> Mon m1 m2---- | The category of all monoids, with monoid morphisms as arrows.-instance Category Mon where-  -  src (MonoidMorphism _) = MonoidMorphism id-  tgt (MonoidMorphism _) = MonoidMorphism id-  -  MonoidMorphism f . MonoidMorphism g = MonoidMorphism $ f . g---data ForgetMonoid = ForgetMonoid-type instance Dom ForgetMonoid = Mon-type instance Cod ForgetMonoid = (->)-type instance ForgetMonoid :% a = a--- | The 'ForgetMonoid' functor forgets the monoid structure.-instance Functor ForgetMonoid where-  ForgetMonoid % MonoidMorphism f = f-  -data FreeMonoid = FreeMonoid-type instance Dom FreeMonoid = (->)-type instance Cod FreeMonoid = Mon-type instance FreeMonoid :% a = [a]--- | The 'FreeMonoid' functor is the list functor.-instance Functor FreeMonoid where-  FreeMonoid % f = MonoidMorphism $ map f---- | The free monoid functor is left adjoint to the forgetful functor.-freeMonoidAdj :: Adjunction Mon (->) FreeMonoid ForgetMonoid-freeMonoidAdj = mkAdjunction FreeMonoid ForgetMonoid (\_ -> (:[])) (\(MonoidMorphism _) -> MonoidMorphism mconcat)--foldMap :: Monoid m => (a -> m) -> [a] -> m-foldMap = (ForgetMonoid %) . rightAdjunct freeMonoidAdj (MonoidMorphism id)--listMonadReturn :: a -> [a]-listMonadReturn = M.unit (adjunctionMonad freeMonoidAdj) ! id--listMonadJoin :: [[a]] -> [a]-listMonadJoin = M.multiply (adjunctionMonad freeMonoidAdj) ! id--listComonadExtract :: Monoid m => [m] -> m-listComonadExtract = ForgetMonoid % (M.counit (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id)--listComonadDuplicate :: Monoid m => [m] -> [[m]]-listComonadDuplicate = ForgetMonoid % (M.comultiply (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id)

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ViewPatterns #-}+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ViewPatterns, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Monoidal@@ -10,10 +10,6 @@ ----------------------------------------------------------------------------- module Data.Category.Monoidal where -import Prelude (($), uncurry)-import qualified Control.Monad as M-import qualified Data.Monoid as M- import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation@@ -24,25 +20,25 @@  -- | A monoidal category is a category with some kind of tensor product. --   A tensor product is a bifunctor, with a unit object.-class Functor f => TensorProduct f where+class (Functor f, Dom f ~ (Cod f :**: Cod f)) => TensorProduct f where      type Unit f :: *   unitObject :: f -> Obj (Cod f) (Unit f) -  leftUnitor     :: Cod f ~ (~>) => f -> Obj (~>) a -> (f :% (Unit f, a)) ~> a-  leftUnitorInv  :: Cod f ~ (~>) => f -> Obj (~>) a -> a ~> (f :% (Unit f, a))-  rightUnitor    :: Cod f ~ (~>) => f -> Obj (~>) a -> (f :% (a, Unit f)) ~> a-  rightUnitorInv :: Cod f ~ (~>) => f -> Obj (~>) a -> a ~> (f :% (a, Unit f))+  leftUnitor     :: Cod f ~ k => f -> Obj k a -> k (f :% (Unit f, a)) a+  leftUnitorInv  :: Cod f ~ k => f -> Obj k a -> k a (f :% (Unit f, a))+  rightUnitor    :: Cod f ~ k => f -> Obj k a -> k (f :% (a, Unit f)) a+  rightUnitorInv :: Cod f ~ k => f -> Obj k a -> k a (f :% (a, Unit f))   -  associator     :: Cod f ~ (~>) => f -> Obj (~>) a -> Obj (~>) b -> Obj (~>) c -> (f :% (f :% (a, b), c)) ~> (f :% (a, f :% (b, c)))-  associatorInv  :: Cod f ~ (~>) => f -> Obj (~>) a -> Obj (~>) b -> Obj (~>) c -> (f :% (a, f :% (b, c))) ~> (f :% (f :% (a, b), c))+  associator     :: Cod f ~ k => f -> Obj k a -> Obj k b -> Obj k c -> k (f :% (f :% (a, b), c)) (f :% (a, f :% (b, c)))+  associatorInv  :: Cod f ~ k => f -> Obj k a -> Obj k b -> Obj k c -> k (f :% (a, f :% (b, c))) (f :% (f :% (a, b), c))   -- | If a category has all products, then the product functor makes it a monoidal category, --   with the terminal object as unit.-instance (HasTerminalObject (~>), HasBinaryProducts (~>)) => TensorProduct (ProductFunctor (~>)) where+instance (HasTerminalObject k, HasBinaryProducts k) => TensorProduct (ProductFunctor k) where   -  type Unit (ProductFunctor (~>)) = TerminalObject (~>)+  type Unit (ProductFunctor k) = TerminalObject k   unitObject _ = terminalObject    leftUnitor     _ a = proj2 terminalObject a@@ -55,9 +51,9 @@  -- | If a category has all coproducts, then the coproduct functor makes it a monoidal category, --   with the initial object as unit.-instance (HasInitialObject (~>), HasBinaryCoproducts (~>)) => TensorProduct (CoproductFunctor (~>)) where+instance (HasInitialObject k, HasBinaryCoproducts k) => TensorProduct (CoproductFunctor k) where   -  type Unit (CoproductFunctor (~>)) = InitialObject (~>)+  type Unit (CoproductFunctor k) = InitialObject k   unitObject _ = initialObject    leftUnitor     _ a = initialize a ||| a@@ -69,9 +65,9 @@   associatorInv _ a b c = (inj1 (a +++ b) c . inj1 a b) ||| (inj2 a b +++ c)    -- | Functor composition makes the category of endofunctors monoidal, with the identity functor as unit.-instance Category (~>) => TensorProduct (FunctorCompose (~>)) where+instance Category k => TensorProduct (FunctorCompose k) where   -  type Unit (FunctorCompose (~>)) = Id (~>)+  type Unit (FunctorCompose k) = Id k   unitObject _ = natId Id      leftUnitor     _ (Nat g _ _) = idPostcomp g@@ -85,50 +81,42 @@  -- | @MonoidObject f a@ defines a monoid @a@ in a monoidal category with tensor product @f@. data MonoidObject f a = MonoidObject-  { unit     :: (Cod f ~ (~>)) => Unit f        ~> a-  , multiply :: (Cod f ~ (~>)) => (f :% (a, a)) ~> a+  { unit     :: (Cod f ~ k) => k (Unit f)        a+  , multiply :: (Cod f ~ k) => k ((f :% (a, a))) a   }    -- | @ComonoidObject f a@ defines a comonoid @a@ in a comonoidal category with tensor product @f@. data ComonoidObject f a = ComonoidObject-  { counit     :: (Cod f ~ (~>)) => a ~> Unit f-  , comultiply :: (Cod f ~ (~>)) => a ~> (f :% (a, a))+  { counit     :: (Cod f ~ k) => k a (Unit f)+  , comultiply :: (Cod f ~ k) => k a (f :% (a, a))   } --- | Monoids as defined in the prelude are monoids in @Hask@ with the product functor as tensor product.-preludeMonoid :: M.Monoid m => MonoidObject (ProductFunctor (->)) m-preludeMonoid = MonoidObject M.mempty (uncurry M.mappend)-- data MonoidAsCategory f m a b where-  MonoidValue :: (TensorProduct f, Dom f ~ ((~>) :**: (~>)), Cod f ~ (~>))-              => f -> MonoidObject f m -> Unit f ~> m -> MonoidAsCategory f m m m+  MonoidValue :: (TensorProduct f, Dom f ~ (k :**: k), Cod f ~ k)+              => f -> MonoidObject f m -> k (Unit f) m -> MonoidAsCategory f m m m  -- | A monoid as a category with one object. instance Category (MonoidAsCategory f m) where   -  src (MonoidValue f m _) = MonoidValue f m $ unit m-  tgt (MonoidValue f m _) = MonoidValue f m $ unit m+  src (MonoidValue f m _) = MonoidValue f m (unit m)+  tgt (MonoidValue f m _) = MonoidValue f m (unit m)   -  MonoidValue f m a . MonoidValue _ _ b = MonoidValue f m $ multiply m . f % (a :**: b) . leftUnitorInv f (unitObject f)+  MonoidValue f m a . MonoidValue _ _ b = MonoidValue f m (multiply m . f % (a :**: b) . leftUnitorInv f (unitObject f))   -- | A monad is a monoid in the category of endofunctors. type Monad f = MonoidObject (FunctorCompose (Dom f)) f -mkMonad :: (Functor f, Dom f ~ (~>), Cod f ~ (~>), Category (~>)) +mkMonad :: (Functor f, Dom f ~ k, Cod f ~ k, Category k)    => f -  -> (forall a. Obj (~>) a -> Component (Id (~>)) f a) -  -> (forall a. Obj (~>) a -> Component (f :.: f) f a)+  -> (forall a. Obj k a -> Component (Id k) f a) +  -> (forall a. Obj k a -> Component (f :.: f) f a)   -> Monad f mkMonad f ret join = MonoidObject   { unit     = Nat Id        f ret   , multiply = Nat (f :.: f) f join   } -preludeMonad :: (M.Functor f, M.Monad f) => Monad (EndoHask f)-preludeMonad = mkMonad EndoHask (\_ -> M.return) (\_ -> M.join)- monadFunctor :: Monad f -> f monadFunctor (unit -> Nat _ f _) = f @@ -136,10 +124,10 @@ -- | A comonad is a comonoid in the category of endofunctors. type Comonad f = ComonoidObject (FunctorCompose (Dom f)) f -mkComonad :: (Functor f, Dom f ~ (~>), Cod f ~ (~>), Category (~>)) +mkComonad :: (Functor f, Dom f ~ k, Cod f ~ k, Category k)    => f -  -> (forall a. Obj (~>) a -> Component f (Id (~>)) a) -  -> (forall a. Obj (~>) a -> Component f (f :.: f) a)+  -> (forall a. Obj k a -> Component f (Id k) a) +  -> (forall a. Obj k a -> Component f (f :.: f) a)   -> Comonad f mkComonad f extr dupl = ComonoidObject   { counit     = Nat f Id        extr

@@ -0,0 +1,62 @@+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, UndecidableInstances, NoImplicitPrelude #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Peano+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category.NNO where++import Data.Category+import Data.Category.Functor+import Data.Category.Limit+import Data.Category.Unit+import Data.Category.Coproduct+import Data.Category.Fix+++class HasTerminalObject k => HasNaturalNumberObject k where+  +  type NaturalNumberObject k :: *+  +  zero :: k (TerminalObject k) (NaturalNumberObject k)+  succ :: k (NaturalNumberObject k) (NaturalNumberObject k)+  +  primRec :: k (TerminalObject k) a -> k a a -> k (NaturalNumberObject k) a+  +  +data NatNum = Z | S NatNum++instance HasNaturalNumberObject (->) where+  +  type NaturalNumberObject (->) = NatNum+  +  zero = \() -> Z+  succ = S+  +  primRec z _  Z    = z ()+  primRec z s (S n) = s (primRec z s n)+++type Nat = Fix ((:++:) Unit)++instance HasNaturalNumberObject Cat where+  +  type NaturalNumberObject Cat = CatW Nat+  +  zero = CatA (Const (Fix (I1 Unit)))+  succ = CatA (Wrap :.: Inj2)+  +  primRec (CatA z) (CatA s) = CatA (PrimRec z s)+  +data PrimRec z s = PrimRec z s+type instance Dom (PrimRec z s) = Nat+type instance Cod (PrimRec z s) = Cod z+type instance PrimRec z s :% I1 () = z :% ()+type instance PrimRec z s :% I2 n  = s :% PrimRec z s :% n+instance (Functor z, Functor s, Dom z ~ Unit, Cod z ~ Dom s, Dom s ~ Cod s) => Functor (PrimRec z s) where+  PrimRec z s % Fix (I1 Unit) = z % Unit+  PrimRec z s % Fix (I2 n) = s % PrimRec z s % n

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs #-}+{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.NaturalTransformation@@ -44,8 +44,6 @@    ) where   -import Prelude hiding ((.), Functor)- import Data.Category import Data.Category.Functor import Data.Category.Product@@ -77,12 +75,12 @@  -- | Horizontal composition of natural transformations. o :: (Category c, Category d, Category e) => Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)-njk@(Nat j k _) `o` nfg@(Nat f g _) = Nat (j :.: f) (k :.: g) $ (njk !) . (nfg !)--- Nat j k njk `o` Nat f g nfg = Nat (j :.: f) (k :.: g) $ \x -> njk (g % x) . j % nfg x -- or k % nfg x . njk (f % x)+njk@(Nat j k _) `o` nfg@(Nat f g _) = Nat (j :.: f) (k :.: g) ((njk !) . (nfg !))+-- Nat j k njk `o` Nat f g nfg = Nat (j :.: f) (k :.: g) (\x -> njk (g % x) . j % nfg x) -- or k % nfg x . njk (f % x)  -- | The identity natural transformation of a functor. natId :: Functor f => f -> Nat (Dom f) (Cod f) f f-natId f = Nat f f $ \i -> f % i+natId f = Nat f f (\i -> f % i)  srcF :: Nat c d f g -> f srcF (Nat f _ _) = f@@ -98,16 +96,16 @@   src (Nat f _ _)           = natId f   tgt (Nat _ g _)           = natId g   -  Nat _ h ngh . Nat f _ nfg = Nat f h $ \i -> ngh i . nfg i+  Nat _ h ngh . Nat f _ nfg = Nat f h (\i -> ngh i . nfg i)   compAssoc :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h)            => f -> g -> h -> Nat (Dom h) (Cod f) ((f :.: g) :.: h) (f :.: (g :.: h))-compAssoc f g h = Nat ((f :.: g) :.: h) (f :.: (g :.: h)) $ \i -> f % g % h % i+compAssoc f g h = Nat ((f :.: g) :.: h) (f :.: (g :.: h)) (\i -> f % g % h % i)  compAssocInv :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h)               => f -> g -> h -> Nat (Dom h) (Cod f) (f :.: (g :.: h)) ((f :.: g) :.: h)-compAssocInv f g h = Nat (f :.: (g :.: h)) ((f :.: g) :.: h) $ \i -> f % g % h % i+compAssocInv f g h = Nat (f :.: (g :.: h)) ((f :.: g) :.: h) (\i -> f % g % h % i)  idPrecomp :: Functor f => f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f idPrecomp f = Nat (f :.: Id) f (f %)@@ -123,31 +121,31 @@   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) $ const fx+constPrecomp (Const x) f = let fx = f % x in Nat (f :.: Const x) (Const fx) (\_ -> fx)  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) $ const fx+constPrecompInv (Const x) f = let fx = f % x in Nat (Const fx) (f :.: Const x) (\_ -> fx)  constPostcomp :: 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) $ const x+constPostcomp (Const x) f = Nat (Const x :.: f) (Const x) (\_ -> x)  constPostcompInv :: 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) $ const x+constPostcompInv (Const x) f = Nat (Const x) (Const x :.: f) (\_ -> x)    -- | The category of endofunctors.-type Endo (~>) = Nat (~>) (~>)+type Endo k = Nat k k  -data FunctorCompose ((~>) :: * -> * -> *) = FunctorCompose+data FunctorCompose (k :: * -> * -> *) = FunctorCompose -type instance Dom (FunctorCompose (~>)) = Endo (~>) :**: Endo (~>)-type instance Cod (FunctorCompose (~>)) = Endo (~>)-type instance FunctorCompose (~>) :% (f, g) = f :.: g+type instance Dom (FunctorCompose k) = Endo k :**: Endo k+type instance Cod (FunctorCompose k) = Endo k+type instance FunctorCompose k :% (f, g) = f :.: g  -- | Composition of endofunctors is a functor.-instance Category (~>) => Functor (FunctorCompose (~>)) where+instance Category k => Functor (FunctorCompose k) where   FunctorCompose % (n1 :**: n2) = n1 `o` n2  

@@ -1,119 +0,0 @@-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances #-}--------------------------------------------------------------------------------- |--- Module      :  Data.Category.Omega--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  sjoerd@w3future.com--- Stability   :  experimental--- Portability :  non-portable------ Omega, the category 0 -> 1 -> 2 -> 3 -> ... --- The objects are the natural numbers, and there's an arrow from a to b iff a <= b.-------------------------------------------------------------------------------module Data.Category.Omega where--import Prelude hiding ((.), id, Functor, product)--import Data.Category-import Data.Category.Limit-import Data.Category.Monoidal---data Z-data S n---- | The arrows of omega, there's an arrow from a to b iff a <= b.-data Omega :: * -> * -> * where-  Z   :: Omega Z Z-  Z2S :: Omega Z n -> Omega Z (S n)-  S   :: Omega a b -> Omega (S a) (S b)-  --- | The objects of omega are the natural numbers, and there's an arrow from a to b iff a <= b.-instance Category Omega where-  -  src Z       = Z-  src (Z2S _) = Z-  src (S   a) = S (src a)-  -  tgt Z       = Z-  tgt (Z2S a) = S (tgt a)-  tgt (S   a) = S (tgt a)-  -  a     . Z       = a-  (S a) . (Z2S n) = Z2S (a . n)-  (S a) . (S   b) = S   (a . b)-  _       . _     = error "Other combinations should not type check"----- | 'Z' (zero) is the initial object of omega.-instance HasInitialObject Omega where-  -  type InitialObject Omega = Z-  -  initialObject    = Z-  -  initialize Z     = Z-  initialize (S n) = Z2S $ initialize n-  initialize _     = error "Other combinations should not type check"----type instance BinaryProduct Omega Z     n = Z-type instance BinaryProduct Omega n     Z = Z-type instance BinaryProduct Omega (S a) (S b) = S (BinaryProduct Omega a b)---- | The product in omega is the minimum.-instance HasBinaryProducts Omega where --  proj1 Z     Z     = Z-  proj1 Z     (S _) = Z-  proj1 (S n) Z     = Z2S $ proj1 n Z-  proj1 (S a) (S b) = S $ proj1 a b-  proj1 _     _     = error "Other combinations should not type check"--  proj2 Z     Z     = Z-  proj2 Z     (S n) = Z2S $ proj2 Z n-  proj2 (S _) Z     = Z-  proj2 (S a) (S b) = S $ proj2 a b-  proj2 _     _     = error "Other combinations should not type check"-  -  Z     &&& _     = Z-  _     &&& Z     = Z-  Z2S a &&& Z2S b = Z2S (a &&& b)-  S a   &&& S b   = S (a &&& b)-  _     &&& _     = error "Other combinations should not type check"---type instance BinaryCoproduct Omega Z     n     = n-type instance BinaryCoproduct Omega n     Z     = n-type instance BinaryCoproduct Omega (S a) (S b) = S (BinaryCoproduct Omega a b)---- | The coproduct in omega is the maximum.-instance HasBinaryCoproducts Omega where -  -  inj1 Z     Z     = Z-  inj1 Z     (S n) = Z2S $ inj1 Z n-  inj1 (S n) Z     = S $ inj1 n Z-  inj1 (S a) (S b) = S $ inj1 a b-  inj1 _     _     = error "Other combinations should not type check"-  inj2 Z     Z     = Z-  inj2 Z     (S n) = S $ inj2 Z n-  inj2 (S n) Z     = Z2S $ inj2 n Z-  inj2 (S a) (S b) = S $ inj2 a b-  inj2 _     _     = error "Other combinations should not type check"-  -  Z     ||| Z     = Z-  Z2S _ ||| a     = a-  a     ||| Z2S _ = a-  S a   ||| S b   = S (a ||| b)-  _     ||| _     = error "Other combinations should not type check"----- | Zero is a monoid object wrt the maximum.-zeroMonoid :: MonoidObject (CoproductFunctor Omega) Z-zeroMonoid = MonoidObject Z Z---- | Zero is also a comonoid object wrt the maximum.-zeroComonoid :: ComonoidObject (CoproductFunctor Omega) Z-zeroComonoid = ComonoidObject Z Z

@@ -1,57 +0,0 @@-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances, ViewPatterns #-}--------------------------------------------------------------------------------- |--- Module      :  Data.Category.Peano--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  sjoerd@w3future.com--- Stability   :  experimental--- Portability :  non-portable--- --- A Peano category as in @When is one thing equal to some other thing?@--- Barry Mazur, 2007-------------------------------------------------------------------------------module Data.Category.Peano where--import Prelude(($))--import Data.Category-import Data.Category.Limit---data PeanoO (~>) a where-  PeanoO :: (TerminalObject (~>) ~> x) -> (x ~> x) -> PeanoO (~>) x-    -data Peano :: (* -> * -> *) -> * -> * -> * where-  PeanoA :: PeanoO (~>) a -> PeanoO (~>) b -> (a ~> b) -> Peano (~>) a b--peanoId :: Category (~>) => PeanoO (~>) a -> Obj (Peano (~>)) a-peanoId o@(PeanoO z _) = PeanoA o o $ tgt z--peanoO :: Category (~>) => Obj (Peano (~>)) a -> PeanoO (~>) a-peanoO (PeanoA o _ _) = o---- | The 'Peano' category.-instance HasTerminalObject (~>) => Category (Peano (~>)) where-  -  src (PeanoA s _ _) = peanoId s-  tgt (PeanoA _ t _) = peanoId t-  -  (PeanoA _ t f) . (PeanoA s _ g) = PeanoA s t $ f . g-  -  -data NatNum = Z () | S NatNum---- | Primitive recursion is the factorizer from the natural numbers.-primRec :: (() -> t) -> (t -> t) -> NatNum -> t-primRec z _ (Z ()) = z ()-primRec z s (S  n) = s (primRec z s n)-  --- | The natural numbers are the initial object for the 'Peano' category.-instance HasInitialObject (Peano (->)) where-  -  type InitialObject (Peano (->)) = NatNum-  -  initialObject = peanoId $ PeanoO Z S-  -  initialize (peanoO -> o@(PeanoO z s)) = PeanoA (peanoO initialObject) o $ primRec z s

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, TypeSynonymInstances, GADTs #-}+{-# LANGUAGE TypeOperators, TypeFamilies, TypeSynonymInstances, GADTs, FlexibleInstances, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Presheaf@@ -10,8 +10,6 @@ ----------------------------------------------------------------------------- module Data.Category.Presheaf where -import Prelude (($))- import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation@@ -20,23 +18,23 @@ import Data.Category.Yoneda  -type Presheaves (~>) = Nat (Op (~>)) (->)+type Presheaves k = Nat (Op k) (->) -type PShExponential (~>) y z = (Presheaves (~>) :-*: z) :.: Opposite -  (   ProductFunctor (Presheaves (~>))-  :.: Tuple2 (Presheaves (~>)) (Presheaves (~>)) y-  :.: YonedaEmbedding (~>)+type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite +  (   ProductFunctor (Presheaves k)+  :.: Tuple2 (Presheaves k) (Presheaves k) y+  :.: YonedaEmbedding k   )-pshExponential :: Category (~>) => Obj (Presheaves (~>)) y -> Obj (Presheaves (~>)) z -> PShExponential (~>) y z+pshExponential :: Category k => Obj (Presheaves k) y -> Obj (Presheaves k) z -> PShExponential k y z pshExponential y z = hom_X z :.: Opposite (ProductFunctor :.: Tuple2 y :.: yonedaEmbedding) -type instance Exponential (Presheaves (~>)) y z = PShExponential (~>) y z+type instance Exponential (Presheaves k) y z = PShExponential k y z  -- | The category of presheaves on a category @C@ is cartesian closed for any @C@.-instance Category (~>) => CartesianClosed (Presheaves (~>)) where+instance Category k => CartesianClosed (Presheaves k) where   -  apply yn@(Nat y _ _) zn@(Nat z _ _) = Nat (pshExponential yn zn :*: y) z $ \(Op i) (n, yi) -> (n ! Op i) (i, yi)-  tuple yn zn@(Nat z _ _) = Nat z (pshExponential yn (zn *** yn)) $ \(Op i) zi -> (Nat (hom_X i) z $ \_ j2i -> (z % Op j2i) zi) *** yn-  zn ^^^ yn = Nat (pshExponential (tgt yn) (src zn)) (pshExponential (src yn) (tgt zn)) $ \(Op i) n -> zn . n . (natId (hom_X i) *** yn)+  apply yn@(Nat y _ _) zn@(Nat z _ _) = Nat (pshExponential yn zn :*: y) z (\(Op i) (n, yi) -> (n ! Op i) (i, yi))+  tuple yn zn@(Nat z _ _) = Nat z (pshExponential yn (zn *** yn)) (\(Op i) zi -> (Nat (hom_X i) z (\_ j2i -> (z % Op j2i) zi) *** yn))+  zn ^^^ yn = Nat (pshExponential (tgt yn) (src zn)) (pshExponential (src yn) (tgt zn)) (\(Op i) n -> zn . n . (natId (hom_X i) *** yn))      

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleContexts #-}+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleContexts, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Product@@ -9,8 +9,6 @@ -- Portability :  non-portable ----------------------------------------------------------------------------- module Data.Category.Product where--import Prelude ()  import Data.Category 

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, RankNTypes #-}+{-# LANGUAGE TypeOperators, TypeFamilies, RankNTypes, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.RepresentableFunctor@@ -10,8 +10,6 @@ ----------------------------------------------------------------------------- module Data.Category.RepresentableFunctor where -import Prelude (($), id)- import Data.Category import Data.Category.Functor @@ -19,22 +17,22 @@ data Representable f repObj = Representable   { representedFunctor :: f   , representingObject :: Obj (Dom f) repObj-  , represent          :: (Dom f ~ (~>), Cod f ~ (->)) => Obj (~>) z -> f :% z -> repObj ~> z-  , universalElement   :: (Dom f ~ (~>), Cod f ~ (->)) => f :% repObj+  , represent          :: (Dom f ~ k, Cod f ~ (->)) => Obj k z -> f :% z -> k repObj z+  , universalElement   :: (Dom f ~ k, Cod f ~ (->)) => f :% repObj   } -unrepresent :: (Functor f, Dom f ~ (~>), Cod f ~ (->)) => Representable f repObj -> repObj ~> z -> f :% z-unrepresent rep h = representedFunctor rep % h $ universalElement rep+unrepresent :: (Functor f, Dom f ~ k, Cod f ~ (->)) => Representable f repObj -> k repObj z -> f :% z+unrepresent rep h = (representedFunctor rep % h) (universalElement rep) -covariantHomRepr :: Category (~>) => Obj (~>) x -> Representable (x :*-: (~>)) x+covariantHomRepr :: Category k => Obj k x -> Representable (x :*-: k) x covariantHomRepr x = Representable   { representedFunctor = homX_ x   , representingObject = x-  , represent          = \_ -> id+  , represent          = \_ h -> h   , universalElement   = x   } -contravariantHomRepr :: Category (~>) => Obj (~>) x -> Representable ((~>) :-*: x) x+contravariantHomRepr :: Category k => Obj k x -> Representable (k :-*: x) x contravariantHomRepr x = Representable   { representedFunctor = hom_X x   , representingObject = Op x

@@ -0,0 +1,200 @@+{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, TypeOperators, UndecidableInstances, NoImplicitPrelude #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Simplex+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+--+-- The (augmented) simplex category.+-----------------------------------------------------------------------------+module Data.Category.Simplex (+  +  -- * Simplex Category+    Simplex(..)+  , Z, S+  , suc+  +  -- * Functor+  , Forget(..)+  , Fin(..)+  , Add(..)+  +  -- * The universal monoid+  , universalMonoid+  , Replicate(..)+        +) where+  +import Data.Category+import Data.Category.Product+import Data.Category.Functor+import Data.Category.Monoidal+import Data.Category.Limit+++data Z+data S n+++-- A Simplex x y structure plots a non-decreasing line, ending with Z+--+--   ^  +-----Z+--   |  |   XXY+--   y  |   Y |+--      |XXXY |+--      XY----++--         x ->++data Simplex :: * -> * -> * where+  Z ::                    Simplex    Z     Z+  Y :: Simplex x    y  -> Simplex    x  (S y)+  X :: Simplex x (S y) -> Simplex (S x) (S y)++suc :: Obj Simplex n -> Obj Simplex (S n)+suc = X . Y+-- Note: Objects are represented by their identity arrows, +-- which are in the shape of the elements of `iterate suc Z`.++-- | The (augmented) simplex category is the category of finite ordinals and order preserving maps.+instance Category Simplex where+  src Z = Z+  src (Y f) = src f+  src (X f) = suc (src f)+  +  tgt Z = Z+  tgt (Y f) = suc (tgt f)+  tgt (X f) = tgt f+  +  Z     .    f  = f+  f     .    Z  = f+  (Y f) .    g  = Y (f . g)+  (X f) . (Y g) = f . g+  (X f) . (X g) = X ((X f) . g)+++-- | The ordinal @0@ is the initial object of the simplex category.+instance HasInitialObject Simplex where+  type InitialObject Simplex = Z+  +  initialObject = Z+  +  initialize Z = Z+  initialize (X (Y f)) = Y (initialize f)++-- | The ordinal @1@ is the terminal object of the simplex category.+instance HasTerminalObject Simplex where+  type TerminalObject Simplex = S Z++  terminalObject = suc Z++  terminate Z = Y Z+  terminate (X (Y f)) = X (terminate f)++++type Merge m n = BinaryCoproduct Simplex m n+type instance BinaryCoproduct Simplex  Z       Z  = Z+type instance BinaryCoproduct Simplex  Z    (S n) = S (Merge Z n)+type instance BinaryCoproduct Simplex (S m)    Z  = S (Merge m Z)+type instance BinaryCoproduct Simplex (S m) (S n) = S (S (Merge m n))++mergeLS :: Obj Simplex m -> Obj Simplex n -> Simplex (Merge (S m) n) (S (Merge m n))+mergeLS Z Z = X (Y Z)+mergeLS Z (X (Y n)) = X (Y (X (Y (Z +++ n))))+mergeLS (X (Y m)) Z = X (Y (X (Y (m +++ Z))))+mergeLS (X (Y m)) (X (Y n)) = X (Y (X (Y (mergeLS m n))))++mergeRS :: Obj Simplex m -> Obj Simplex n -> Simplex (Merge m (S n)) (S (Merge m n))+mergeRS Z Z = X (Y Z)+mergeRS Z (X (Y n)) = X (Y (X (Y (Z +++ n))))+mergeRS (X (Y m)) Z = X (Y (X (Y (m +++ Z))))+mergeRS (X (Y m)) (X (Y n)) = X (Y (X (Y (mergeRS m n))))++-- | The coproduct in the simplex category is a merge operation.+instance HasBinaryCoproducts Simplex where+  inj1       Z         Z   = Z+  inj1       Z   (X (Y n)) = Y (inj1 Z n)+  inj1 (X (Y m))       Z   = X (Y (inj1 m Z))+  inj1 (X (Y m)) (X (Y n)) = X (Y (Y (inj1 m n)))++  inj2       Z         Z   = Z+  inj2       Z   (X (Y n)) = X (Y (inj2 Z n))+  inj2 (X (Y m))       Z   = Y (inj2 m Z)+  inj2 (X (Y m)) (X (Y n)) = Y (X (Y (inj2 m n)))++  Z   ||| Z   = Z+  X f ||| X g = X (X (f ||| g))+  X f ||| Y g = X (f ||| Y g) . mergeLS (src f) (src g)+  Y f ||| X g = X (Y f ||| g) . mergeRS (src f) (src g)+  Y f ||| Y g = Y (f ||| g)+++data Fin :: * -> * where+  Fz ::          Fin (S n)+  Fs :: Fin n -> Fin (S n)++data Forget = Forget+type instance Dom Forget = Simplex+type instance Cod Forget = (->)+type instance Forget :% n = Fin n+-- | Turn @Simplex x y@ arrows into @Fin x -> Fin y@ functions.+instance Functor Forget where +  Forget %  Z    = \x -> x+  Forget % (Y f) = \x -> Fs ((Forget % f) x)+  Forget % (X f) = \x -> case x of+    Fz -> Fz+    Fs n -> (Forget % f) n+++data Add = Add+type instance Dom Add = Simplex :**: Simplex+type instance Cod Add = Simplex+type instance Add :% (Z  , n) = n+type instance Add :% (S m, n) = S (Add :% (m, n))+-- | Ordinal addition is a bifuntor, it concattenates the maps as it were.+instance Functor Add where+  Add % (Z   :**: g) = g+  Add % (Y f :**: g) = Y (Add % (f :**: g))+  Add % (X f :**: g) = X (Add % (f :**: g))++-- | Ordinal addition makes the simplex category a monoidal category, with @0@ as unit.+instance TensorProduct Add where+  type Unit Add = Z+  unitObject Add = Z+  +  leftUnitor     Add       a   = a+  leftUnitorInv  Add       a   = a+  rightUnitor    Add       Z   = Z+  rightUnitor    Add (X (Y n)) = X (Y (rightUnitor Add n))+  rightUnitorInv Add       Z   = Z+  rightUnitorInv Add (X (Y n)) = X (Y (rightUnitorInv Add n))+  associator     Add Z       Z   n = n+  associator     Add Z (X (Y m)) n = X (Y (associator Add Z m n))+  associator     Add (X (Y l)) m n = X (Y (associator Add l m n))+  associatorInv  Add Z       Z   n = n+  associatorInv  Add Z (X (Y m)) n = X (Y (associatorInv Add Z m n))+  associatorInv  Add (X (Y l)) m n = X (Y (associatorInv Add l m n))+++-- | The maps @0 -> 1@ and @2 -> 1@ form a monoid, which is universal, c.f. `Replicate`.+universalMonoid :: MonoidObject (CoproductFunctor Simplex) (S Z)+universalMonoid = MonoidObject { unit = Y Z, multiply = X (X (Y Z)) }++data Replicate f a = Replicate f (MonoidObject f a)+type instance Dom (Replicate f a) = Simplex+type instance Cod (Replicate f a) = Cod f+type instance Replicate f a :% Z = Unit f+type instance Replicate f a :% S n = f :% (a, Replicate f a :% n)+-- | Replicate a monoid a number of times.+instance TensorProduct f => Functor (Replicate f a) where+  Replicate f _ % Z = unitObject f+  Replicate f m % Y n = f % (unit m :**: tgt n') . leftUnitorInv f (tgt n') . n' where n' = Replicate f m % n+  Replicate f m % X (Y n) = f % (tgt (unit m) :**: (Replicate f m % n))+  Replicate f m % X (X n) = n' . (f % (multiply m :**: b)) . associatorInv f a a b +    where+      n' = Replicate f m % X n+      a = tgt (unit m)+      b = src (Replicate f m % n)

@@ -0,0 +1,25 @@+{-# LANGUAGE GADTs, NoImplicitPrelude #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Unit+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category.Unit where++import Data.Category+++data Unit a b where+  Unit :: Unit () ()++-- | `Unit` is the category with one object.+instance Category Unit where++  src Unit = Unit+  tgt Unit = Unit++  Unit . Unit = Unit

@@ -0,0 +1,42 @@+{-# LANGUAGE GADTs, TypeFamilies, NoImplicitPrelude #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Void+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category.Void where++import Data.Category+import Data.Category.Functor+import Data.Category.NaturalTransformation+++data Void a b++magic :: Void a b -> x+magic x = magic x++-- | `Void` is the category with no objects.+instance Category Void where++  src = magic+  tgt = magic++  (.) = magic+++voidNat :: (Functor f, Functor g, Category d, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d)+  => f -> g -> Nat Void d f g+voidNat f g = Nat f g magic+++data Magic (k :: * -> * -> *) = Magic+type instance Dom (Magic k) = Void+type instance Cod (Magic k) = k+-- | Since there is nothing to map in `Void`, there's a functor from it to any other category.+instance Category k => Functor (Magic k) where+  Magic % f = magic f

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies #-}+{-# LANGUAGE TypeOperators, RankNTypes, TypeFamilies, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Yoneda@@ -10,32 +10,30 @@ ----------------------------------------------------------------------------- module Data.Category.Yoneda where -import Prelude (($))- import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation import Data.Category.CartesianClosed -type YonedaEmbedding (~>) = Postcompose (Hom (~>)) (Op (~>)) :.: ToTuple2 (~>) (Op (~>)) +type YonedaEmbedding k = Postcompose (Hom k) (Op k) :.: ToTuple2 k (Op k)   -- | The Yoneda embedding functor, @C -> Set^(C^op)@.-yonedaEmbedding :: Category (~>) => YonedaEmbedding (~>)+yonedaEmbedding :: Category k => YonedaEmbedding k yonedaEmbedding = Postcompose Hom :.: ToTuple2  -data Yoneda ((~>) :: * -> * -> *) f = Yoneda-type instance Dom (Yoneda (~>) f) = Op (~>)-type instance Cod (Yoneda (~>) f) = (->)-type instance Yoneda (~>) f :% a = Nat (Op (~>)) (->) ((~>) :-*: a) f+data Yoneda (k :: * -> * -> *) f = Yoneda+type instance Dom (Yoneda k f) = Op k+type instance Cod (Yoneda k f) = (->)+type instance Yoneda k f :% a = Nat (Op k) (->) (k :-*: a) f -- | 'Yoneda' converts a functor @f@ into a natural transformation from the hom functor to f.-instance (Category (~>), Functor f, Dom f ~ Op (~>), Cod f ~ (->)) => Functor (Yoneda (~>) f) where+instance (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => Functor (Yoneda k f) where   Yoneda % Op ab = \n -> n . yonedaEmbedding % ab           -- | 'fromYoneda' and 'toYoneda' are together the isomophism from the Yoneda lemma.-fromYoneda :: (Category (~>), Functor f, Dom f ~ Op (~>), Cod f ~ (->)) => f -> Yoneda (~>) f :~> f-fromYoneda f = Nat Yoneda f $ \(Op a) n -> (n ! Op a) a+fromYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Yoneda k f :~> f+fromYoneda f = Nat Yoneda f (\(Op a) n -> (n ! Op a) a) -toYoneda   :: (Category (~>), Functor f, Dom f ~ Op (~>), Cod f ~ (->)) => f -> f :~> Yoneda (~>) f-toYoneda   f = Nat f Yoneda $ \(Op a) fa -> Nat (hom_X a) f $ \_ h -> (f % Op h) fa+toYoneda   :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> f :~> Yoneda k f+toYoneda   f = Nat f Yoneda (\(Op a) fa -> Nat (hom_X a) f (\_ h -> (f % Op h) fa))

@@ -1,5 +1,5 @@ name:                data-category-version:             0.4.1+version:             0.5.0 synopsis:            Category theory  description:         Data-category is a collection of categories, and some categorical constructions on them.@@ -31,25 +31,25 @@     Data.Category,     Data.Category.Functor,     Data.Category.NaturalTransformation,+    Data.Category.Unit,+    Data.Category.Void,+    Data.Category.Product,+    Data.Category.Coproduct,     Data.Category.RepresentableFunctor,     Data.Category.Adjunction,     Data.Category.Limit,     Data.Category.Monoidal,     Data.Category.CartesianClosed,-    Data.Category.Product,-    Data.Category.Coproduct,-    Data.Category.Discrete,     Data.Category.Yoneda,     Data.Category.Presheaf,-    Data.Category.Monoid,     Data.Category.Boolean,-    Data.Category.Omega,+    Data.Category.Fix,     Data.Category.Kleisli,     Data.Category.Dialg,-    Data.Category.Peano,+    Data.Category.NNO,+    Data.Category.Simplex,     Data.Category.Comma     -  build-depends:       base >= 3 && < 5   default-language:    Haskell2010  source-repository head