Added a Category class with natural transformation Id -> Id.

Data/Category.hs

@@ -12,7 +12,8 @@
 module Data.Category (
 
   -- * Categories
-    CategoryO(..)
+    Category(..)
+  , CategoryO(..)
   , CategoryA(..)
   , Apply(..)
   , Obj, obj
@@ -48,10 +49,14 @@ module Data.Category (
 import Prelude hiding ((.), id, ($))
 
 
+class Category (~>) where
+  idNat :: Id (~>) :~> Id (~>)
+
 -- | An instance CategoryO (~>) a declares a as an object of the category (~>).
-class CategoryO (~>) a where
-  id  :: a ~> a
+class Category (~>) => CategoryO (~>) a where
   (!) :: Nat (~>) d f g -> Obj a -> Component f g a
+  id :: a ~> a
+  id = idNat ! (obj :: a)
 
 -- | An instance CategoryA (~>) a b c defines composition of the arrows a ~> b and b ~> c.
 class (CategoryO (~>) a, CategoryO (~>) b, CategoryO (~>) c) => CategoryA (~>) a b c where

Data/Category/Boolean.hs

@@ -35,11 +35,11 @@ data instance Boolean Fls Tru = FlsTru
 data instance Nat Boolean d f g = 
   BooleanNat (Component f g Fls) (Component f g Tru)
 
+instance Category Boolean where
+  idNat = BooleanNat IdFls IdTru
 instance CategoryO Boolean Fls where
-  id = IdFls
   BooleanNat f _ ! Fls = f
 instance CategoryO Boolean Tru where
-  id = IdTru
   BooleanNat _ t ! Tru = t
 
 instance CategoryA Boolean Fls Fls Fls where

Data/Category/Dialg.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, UndecidableInstances, RankNTypes #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Dialg
@@ -16,24 +16,32 @@ module Data.Category.Dialg where
 import Prelude hiding ((.), id)
 
 import Data.Category
+import Data.Category.Functor
 import Data.Category.Void
+import Data.Category.Pair
+import Data.Category.Product
+import Data.Category.Peano
 
 -- | Objects of Dialg(F,G) are (F,G)-dialgebras.
-newtype Dialgebra f g a = Dialgebra (Dom f (F f a) (F g a))
+newtype Dialgebra f g a = Dialgebra (Cod f (F f a) (F g a))
 
 -- | Arrows of Dialg(F,G) are (F,G)-homomorphisms.
 data family Dialg f g a b :: *
 data instance Dialg f g (Dialgebra f g a) (Dialgebra f g b) = DialgA (Dom f a b)
 
 newtype instance Nat (Dialg f g) d s t = 
-  DialgNat { unDialgNat :: forall a. Obj (Dialgebra f g a) -> Component s t (Dialgebra f g a) }
+  DialgNat { unDialgNat :: forall a. CategoryO (Dom f) a => Obj (Dialgebra f g a) -> Component s t (Dialgebra f g a) }
 
-instance (Dom f ~ (~>), Cod f ~ (~>), Dom g ~ (~>), Cod g ~ (~>), CategoryO (~>) a) 
+getCarrier :: Dialgebra f g a -> a
+getCarrier _ = obj :: a
+
+instance Category (Dom f) => Category (Dialg f g) where
+  idNat = DialgNat $ \dialg -> DialgA (idNat ! getCarrier dialg)
+instance (Dom f ~ c, Cod f ~ d, Dom g ~ c, Cod g ~ d, CategoryO c a) 
   => CategoryO (Dialg f g) (Dialgebra f g a) where
-  id = DialgA id
   (!) = unDialgNat
-instance (Dom f ~ (~>), Cod f ~ (~>), Dom g ~ (~>), Cod g ~ (~>), CategoryA (~>) a b c) 
-  => CategoryA (Dialg f g) (Dialgebra f g a) (Dialgebra f g b) (Dialgebra f g c) where
+instance (Dom f ~ c, Cod f ~ d, Dom g ~ c, Cod g ~ d, CategoryA c x y z) 
+  => CategoryA (Dialg f g) (Dialgebra f g x) (Dialgebra f g y) (Dialgebra f g z) where
   DialgA f . DialgA g = DialgA (f . g)
 
 type Alg f = Dialg f (Id (Dom f))

Data/Category/Hask.hs

@@ -19,23 +19,28 @@ import Data.Category
 import Data.Category.Functor
 import Data.Category.Void
 import Data.Category.Pair
+import Data.Category.Product
+import Data.Category.Peano
 import Data.Category.Dialg
 
 type Hask = (->)
 
-instance Apply (->) a b where
-  ($$) = ($)
-
+newtype instance Nat (->) d f g = 
+  HaskNat { unHaskNat :: forall a. Obj a -> Component f g a }
+
+instance Category (->) where
+  idNat = HaskNat $ const Prelude.id
+
 instance CategoryO (->) a where
   id = Prelude.id
   (!) = unHaskNat
 
 instance CategoryA (->) a b c where
   (.) = (Prelude..)
 
-newtype instance Nat (->) d f g = 
-  HaskNat { unHaskNat :: forall a. Obj a -> Component f g a }
-  
+instance Apply (->) a b where
+  ($$) = ($)
+
 -- | 'EndoHask' is a wrapper to turn instances of the 'Functor' class into categorical functors.
 data EndoHask (f :: * -> *) = EndoHask
 type instance Dom (EndoHask f) = (->)
@@ -84,7 +89,7 @@ instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA Pr
 
 -- | The product functor is right adjoint to the diagonal functor.
 prodInHaskAdj :: Adjunction (Diag Pair (->)) ProdInHask
-prodInHaskAdj = Adjunction { unit = HaskNat $ const (id &&& id), counit = FunctNat $ const (fst :***: snd) }
+prodInHaskAdj = Adjunction { unit = HaskNat $ const (id A.&&& id), counit = FunctNat $ const (fst :***: snd) }
 
 -- | The coproduct functor, Hask^2 -> Hask
 data CoprodInHask = CoprodInHask
@@ -96,7 +101,7 @@ instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA Co
 
 -- | The coproduct functor is left adjoint to the diagonal functor.
 coprodInHaskAdj :: Adjunction CoprodInHask (Diag Pair (->))
-coprodInHaskAdj = Adjunction { unit = FunctNat $ const (Left :***: Right), counit = HaskNat $ const (either id id) }
+coprodInHaskAdj = Adjunction { unit = FunctNat $ const (Left :***: Right), counit = HaskNat $ const (id A.||| id) }
 
 curryAdj :: Adjunction (EndoHask ((,) e)) (EndoHask ((->) e))
 curryAdj = Adjunction 

Data/Category/Kleisli.hs

@@ -27,11 +27,12 @@ class Pointed m => Monad m where
 
 data Kleisli ((~>) :: * -> * -> *) m a b = Kleisli (m -> a ~> F m b)
 
-newtype instance Nat (Kleisli (->) m) d f g = 
-  KleisliNat { unKleisliNat :: forall a. Obj a -> Component f g a }
+newtype instance Nat (Kleisli (~>) m) d f g = 
+  KleisliNat { unKleisliNat :: forall a. CategoryO (~>) a => Obj a -> Component f g a }
 
-instance (Monad m, Dom m ~ (->), Cod m ~ (->)) => CategoryO (Kleisli (->) m) o where
-  id = Kleisli $ \m -> point m ! (obj :: o)
+instance (Monad m, Dom m ~ (~>), Cod m ~ (~>)) => Category (Kleisli (~>) m) where
+  idNat = KleisliNat $ \o -> Kleisli $ \m -> point m ! o
+instance (Monad m, Dom m ~ (~>), Cod m ~ (~>), CategoryO (~>) o) => CategoryO (Kleisli (~>) m) o where
   (!) = unKleisliNat
 instance (Monad m, Dom m ~ (->), Cod m ~ (->), FunctorA m b (F m c)) => CategoryA (Kleisli (->) m) a b c where
   (Kleisli f) . (Kleisli g) = Kleisli $ \m -> join m ! (obj :: c) . (m % f m) . g m

Data/Category/Monoid.hs

@@ -24,8 +24,9 @@ newtype MonoidA m a b = MonoidA m
 newtype instance Nat (MonoidA m) d f g =
   MonoidNat (Component f g m)
 
+instance Monoid m => Category (MonoidA m) where
+  idNat = MonoidNat (MonoidA mempty)
 instance Monoid m => CategoryO (MonoidA m) m where
-  id = MonoidA mempty
   MonoidNat c ! _ = c  
 instance Monoid m => CategoryA (MonoidA m) m m m where
   MonoidA a . MonoidA b = MonoidA $ a `mappend` b

Data/Category/Omega.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Omega
@@ -27,19 +27,19 @@ data Z = Z deriving Show
 -- | The object S n represents the successor of n.
 newtype S n = S n deriving Show
 
-instance CategoryO Omega Z where
-  id = IdZ
-  OmegaNat z _ ! Z = z  
-instance (CategoryO Omega n) => CategoryO Omega (S n) where
-  id = StepS id
-  on@(OmegaNat _ s) ! (S n) = s n (on ! n)
-
 -- | The arrows of omega, there's an arrow from a to b iff a <= b.
 data family Omega a b :: *
 data instance Omega Z Z = IdZ
 newtype instance Omega Z (S n) = GTZ (Omega Z n)
 newtype instance Omega (S a) (S b) = StepS (Omega a b)
 
+instance Category Omega where
+  idNat = OmegaNat IdZ (const StepS)
+instance CategoryO Omega Z where
+  OmegaNat z _ ! Z = z  
+instance (CategoryO Omega n) => CategoryO Omega (S n) where
+  on@(OmegaNat _ s) ! (S n) = s n (on ! n)
+
 instance (CategoryO Omega n) => CategoryA Omega Z Z n where
   a . IdZ = a
 instance (CategoryA Omega Z n p) => CategoryA Omega Z (S n) (S p) where

Data/Category/Pair.hs

@@ -25,11 +25,11 @@ data Fst = Fst deriving Show
 -- | The other object of Pair
 data Snd = Snd deriving Show
 
+instance Category Pair where
+  idNat = IdFst :***: IdSnd
 instance CategoryO Pair Fst where
-  id = IdFst
   (f :***: _) ! Fst = f  
 instance CategoryO Pair Snd where
-  id = IdSnd
   (_ :***: s) ! Snd = s  
 
 -- | The arrows of Pair.
@@ -49,6 +49,8 @@ instance Apply Pair Snd Snd where
 
 
 data instance Nat Pair d f g = Component f g Fst :***: Component f g Snd
+instance Category (Nat Pair (~>)) where
+  idNat = undefined
 instance (Dom f ~ Pair, Cod f ~ (~>), CategoryO (~>) (F f Fst), CategoryO (~>) (F f Snd)) => CategoryO (Nat Pair (~>)) f where
   id = id :***: id
   FunctNat n ! f = n f
@@ -66,25 +68,64 @@ instance (CategoryO (~>) x) => FunctorA (PairF (~>) x y) Fst Fst where
 instance (CategoryO (~>) y) => FunctorA (PairF (~>) x y) Snd Snd where
   PairF % IdSnd = id
 
+
 -- | The product of 2 objects is the limit of the functor from Pair to (~>).
 class (CategoryO (~>) x, CategoryO (~>) y) => PairLimit (~>) x y where
+
   type Product x y :: *
   pairLimit :: Limit (PairF (~>) x y) (Product x y)
-  proj1 :: Product x y ~> x
-  proj2 :: Product x y ~> y
+
+  proj :: (Product x y ~> x, Product x y ~> y)
   (&&&) :: CategoryO (~>) a => (a ~> x) -> (a ~> y) -> (a ~> Product x y)
-  proj1 = p where TerminalUniversal (p :***: _) _ = pairLimit :: Limit (PairF (~>) x y) (Product x y)
-  proj2 = p where TerminalUniversal (_ :***: p) _ = pairLimit :: Limit (PairF (~>) x y) (Product x y)
+
+  pairLimit = TerminalUniversal (p1 :***: p2) undefined where
+    (p1, p2) = proj :: (Product x y ~> x, Product x y ~> y)
+  proj = (n ! Fst, n ! Snd) where 
+    TerminalUniversal n _ = pairLimit :: Limit (PairF (~>) x y) (Product x y)
   l &&& r = (n ! (obj :: a)) (l :***: r) where
     TerminalUniversal _ n = pairLimit :: Limit (PairF (~>) x y) (Product x y)
+
+
 -- | The coproduct of 2 objects is the colimit of the functor from Pair to (~>).
 class (CategoryO (~>) x, CategoryO (~>) y) => PairColimit (~>) x y where
+
   type Coproduct x y :: *
   pairColimit :: Colimit (PairF (~>) x y) (Coproduct x y)
-  inj1 :: x ~> Coproduct x y
-  inj2 :: y ~> Coproduct x y
+
+  inj :: (x ~> Coproduct x y, y ~> Coproduct x y)
   (|||) :: CategoryO (~>) a => (x ~> a) -> (y ~> a) -> (Coproduct x y ~> a)
-  inj1 = i where InitialUniversal (i :***: _) _ = pairColimit :: Colimit (PairF (~>) x y) (Coproduct x y)
-  inj2 = i where InitialUniversal (_ :***: i) _ = pairColimit :: Colimit (PairF (~>) x y) (Coproduct x y)
+
+  pairColimit = InitialUniversal (i1 :***: i2) undefined where
+    (i1, i2) = inj :: (x ~> Coproduct x y, y ~> Coproduct x y)
+  inj = (n ! Fst, n ! Snd) where 
+    InitialUniversal n _ = pairColimit :: Colimit (PairF (~>) x y) (Coproduct x y)
   l ||| r = (n ! (obj :: a)) (l :***: r) where
-    InitialUniversal _ n = pairColimit :: Colimit (PairF (~>) x y) (Coproduct x y)
+    InitialUniversal _ n = pairColimit :: Colimit (PairF (~>) x y) (Coproduct x y)
+
+
+-- t :: Nat Pair (~>) f g -> (Product x y ~> Product a b)
+-- t (f :***: g) = (f . proj1) &&& (g . proj2)
+
+-- | Functor product
+-- data Prod ((~>) :: * -> * -> *) = Prod
+-- type instance Dom (Prod (~>)) = Nat Pair (~>)
+-- type instance Cod (Prod (~>)) = (~>)
+-- type instance F (Prod (~>)) f = Product (F f Fst) (F f Snd)
+-- instance (Dom f ~ Pair, Cod f ~ (~>), Dom g ~ Pair, Cod g ~ (~>), F f Fst ~ fx, F f Snd ~ fy, F g Fst ~ gx, F g Snd ~ gy,
+--   CategoryO (~>) fx, CategoryO (~>) fy, CategoryO (~>) gx, CategoryO (~>) gy) 
+--   => FunctorA (Prod (~>)) f g where
+--   Prod % (f :***: g) = (f . proj1) &&& (g . proj2)
+
+-- data f :*: g = f :*: g
+-- type instance Dom (f :*: g) = Dom f -- ~ Dom g
+-- type instance Cod (f :*: g) = Cod f -- ~ Cod g
+-- type instance F (f :*: g) x = Product (F f x) (F g x)
+-- -- instance (FunctorA g a1 b1, FunctorA h a2 b2, a ~ Product a1 a2, b ~ Product b1 b2)
+-- --   => FunctorA (g :*: h) a b where
+-- --   _ % f = ((obj :: g) % f) &&& ((obj :: h) % f)
+-- 
+-- -- | Functor coproduct
+-- data f :+: g = f :+: g
+-- type instance Dom (f :+: g) = Dom f -- ~ Dom g
+-- type instance Cod (f :+: g) = Cod f -- ~ Cod g
+-- type instance F (f :+: g) x = Coproduct (F f x) (F g x)

Data/Category/Peano.hs

@@ -19,21 +19,23 @@ import Prelude hiding ((.), id)
 import Data.Category
 import Data.Category.Void
 
-data PeanoO (~>) x = PeanoO x (x ~> x)
+data PeanoO (~>) x = PeanoO (TerminalObject (~>) ~> x) (x ~> x)
 
 data family Peano ((~>) :: * -> * -> *) a b :: *
-newtype instance Peano (~>) (PeanoO (~>) a) (PeanoO (~>) b) = PeanoA (a ~> b)
+newtype instance Peano (~>) (PeanoO (~>) a) (PeanoO (~>) b) = PeanoA { unPeanoA :: a ~> b }
 
 newtype instance Nat (Peano (~>)) d f g =
-  PeanoNat { unPeanoNat :: forall x. PeanoO (~>) x -> Component f g (PeanoO (~>) x) }
+  PeanoNat { unPeanoNat :: forall x. CategoryO (~>) x => Obj (PeanoO (~>) x) -> Component f g (PeanoO (~>) x) }
 
+type family PeanoCarrier p :: *
+type instance PeanoCarrier (PeanoO (~>) x) = x
+
+getPeanoCarrier :: PeanoO (~>) x -> x
+getPeanoCarrier _ = obj :: x
+
+instance Category (~>) => Category (Peano (~>)) where
+  idNat = PeanoNat $ \x -> PeanoA (idNat ! getPeanoCarrier x)
 instance CategoryO (~>) x => CategoryO (Peano (~>)) (PeanoO (~>) x) where
-  id = PeanoA id
   (!) = unPeanoNat
 instance CategoryA (~>) a b c => CategoryA (Peano (~>)) (PeanoO (~>) a) (PeanoO (~>) b) (PeanoO (~>) c) where
-  (PeanoA f) . (PeanoA g) = PeanoA (f . g)
-
-instance VoidColimit (Peano (->)) where
-  type InitialObject (Peano (->)) = PeanoO (->) Integer
-  voidColimit = InitialUniversal VoidNat
-    (PeanoNat $ \(PeanoO z s) VoidNat -> PeanoA $ let { f 0 = z; f (n + 1) = s (f n) } in f)
+  (PeanoA f) . (PeanoA g) = PeanoA (f . g)

Data/Category/Unit.hs

@@ -25,8 +25,9 @@ data instance Unit UnitO UnitO = UnitId
 newtype instance Nat Unit d f g =
   UnitNat (Component f g UnitO)
 
+instance Category Unit where
+  idNat = UnitNat UnitId
 instance CategoryO Unit UnitO where
-  id = UnitId
   UnitNat c ! UnitO = c
 instance CategoryA Unit UnitO UnitO UnitO where
   UnitId . UnitId = UnitId

Data/Category/Void.hs

@@ -23,6 +23,10 @@ data Void a b
 
 data instance Nat Void d f g = 
   VoidNat
+
+instance Category Void where
+  idNat = VoidNat
+
 instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag Void (~>)) a b where
   Diag % _ = VoidNat