packages feed

data-category (empty) → 0.0.1

raw patch · 12 files changed

+575/−0 lines, 12 filesdep +basesetup-changed

Dependencies added: base

Files

+ Data/Category.hs view
@@ -0,0 +1,71 @@+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes #-}+module Data.Category where++import Prelude hiding ((.), id, ($))++++class CategoryO (~>) a where+  id :: a ~> a+  +class (CategoryO (~>) a, CategoryO (~>) b, CategoryO (~>) c) => CategoryA (~>) a b c where+  (.) :: b ~> c -> a ~> b -> a ~> c++class (CategoryO (~>) a, CategoryO (~>) b) => Apply (~>) a b where+  -- Would have liked to use ($) here, but that causes GHC to crash.+  -- http://hackage.haskell.org/trac/ghc/ticket/3297+  ($$) :: a ~> b -> a -> b+  ++type family F ftag a :: *+type family Dom ftag :: * -> * -> *+type family Cod ftag :: * -> * -> *++class (CategoryO (Dom ftag) a, CategoryO (Dom ftag) b) +  => FunctorA ftag a b where+  (%) :: ftag -> Dom ftag a b -> Cod ftag (F ftag a) (F ftag b)++class (CategoryO (Dom ftag) a, CategoryO (Dom ftag) b) +  => ContraFunctorA ftag a b where+  (-%) :: ftag -> Dom ftag a b -> Cod ftag (F ftag b) (F ftag a)+++-- |The identity functor on (~>)+data Id ((~>) :: * -> * -> *) = Id+type instance F (Id (~>)) a = a+type instance Dom (Id (~>)) = (~>)+type instance Cod (Id (~>)) = (~>)+instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Id (~>)) a b where+  Id % f = f++-- |The composition of two functors.+data (g :.: h) = g :.: h+type instance F (g :.: h) a = F g (F h a)+type instance Dom (g :.: h) = Dom h+type instance Cod (g :.: h) = Cod g+instance (FunctorA g (F h a) (F h b), FunctorA h a b, Cod h ~ Dom g) => FunctorA (g :.: h) a b where+   (g :.: h) % f = g % (h % f)++-- |The constant functor.+data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x = Const+type instance F (Const c1 c2 x) a = x+type instance Dom (Const c1 c2 x) = c1+type instance Cod (Const c1 c2 x) = c2+instance (CategoryO c1 a, CategoryO c1 b, CategoryO c2 x) => FunctorA (Const c1 c2 x) a b where+  Const % f = id+  +-- |The covariant functor Hom(X,--)+data (x :*-: ((~>) :: * -> * -> *)) = HomX_+type instance F (x :*-: (~>)) a = x ~> a+type instance Dom (x :*-: (~>)) = (~>)+type instance Cod (x :*-: (~>)) = (->)+instance (CategoryO (~>) a, CategoryO (~>) b, CategoryA (~>) x a b) => FunctorA (x :*-: (~>)) a b where+  HomX_ % f = (f .)++-- |The contravariant functor Hom(--,X)+data (((~>) :: * -> * -> *) :-*: x) = Hom_X+type instance F ((~>) :-*: x) a = a ~> x+type instance Dom ((~>) :-*: x) = (~>)+type instance Cod ((~>) :-*: x) = (->)+instance (CategoryO (~>) a, CategoryO (~>) b, CategoryA (~>) a b x) => ContraFunctorA ((~>) :-*: x) a b where+  Hom_X -% f = (. f)
+ Data/Category/Boolean.hs view
@@ -0,0 +1,81 @@+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}+module Data.Category.Boolean where++import Prelude hiding ((.), id)++import Data.Category+import Data.Category.Functor+import Data.Category.Void+import Data.Category.Pair+++-- "2", Boolean Category+data family Boolean a b :: *++data Fls = Fls deriving Show+data Tru = Tru deriving Show++data instance Boolean Fls Fls = IdFls+data instance Boolean Tru Tru = IdTru+data instance Boolean Fls Tru = FlsTru++instance Apply Boolean Fls Fls where+  IdFls $$ Fls = Fls+instance Apply Boolean Fls Tru where+  FlsTru $$ Fls = Tru+instance Apply Boolean Tru Tru where+  IdTru $$ Tru = Tru+  +instance CategoryO Boolean Fls where+  id = IdFls+instance CategoryO Boolean Tru where+  id = IdTru++instance CategoryA Boolean Fls Fls Fls where+  IdFls . IdFls = IdFls+instance CategoryA Boolean Fls Fls Tru where+  FlsTru . IdFls = FlsTru  +instance CategoryA Boolean Fls Tru Tru where+  IdTru . FlsTru = FlsTru  +instance CategoryA Boolean Tru Tru Tru where+  IdTru . IdTru = IdTru+  ++  +data instance Funct Boolean d (FunctO Boolean d f) (FunctO Boolean d g) = +  BooleanNat { flsComp :: Component f g Fls, truComp :: Component f g Tru }+instance (CategoryO (Cod f) (F f Fls), CategoryO (Cod f) (F f Tru)) => CategoryO (Funct Boolean d) (FunctO Boolean d f) where+  id = BooleanNat id id++instance VoidColimit Boolean where+  type InitialObject Boolean = Fls+  voidColimit = InitialUniversal VoidNat (BooleanNat (\VoidNat -> IdFls) (\VoidNat -> FlsTru))+instance VoidLimit Boolean where+  type TerminalObject Boolean = Tru+  voidLimit = TerminalUniversal VoidNat (BooleanNat (\VoidNat -> FlsTru) (\VoidNat -> IdTru))++instance PairLimit Boolean Fls Fls where +  type Product Fls Fls = Fls+  pairLimit = TerminalUniversal (IdFls :***: IdFls) (BooleanNat fstComp sndComp)+instance PairLimit Boolean Fls Tru where +  type Product Fls Tru = Fls+  pairLimit = TerminalUniversal (IdFls :***: FlsTru) (BooleanNat fstComp fstComp)+instance PairLimit Boolean Tru Fls where +  type Product Tru Fls = Fls+  pairLimit = TerminalUniversal (FlsTru :***: IdFls) (BooleanNat sndComp sndComp)+instance PairLimit Boolean Tru Tru where +  type Product Tru Tru = Tru+  pairLimit = TerminalUniversal (IdTru :***: IdTru) (BooleanNat fstComp sndComp)++instance PairColimit Boolean Fls Fls where +  type Coproduct Fls Fls = Fls+  pairColimit = InitialUniversal (IdFls :***: IdFls) (BooleanNat fstComp sndComp)+instance PairColimit Boolean Fls Tru where +  type Coproduct Fls Tru = Tru+  pairColimit = InitialUniversal (FlsTru :***: IdTru) (BooleanNat sndComp sndComp)+instance PairColimit Boolean Tru Fls where +  type Coproduct Tru Fls = Tru+  pairColimit = InitialUniversal (IdTru :***: FlsTru) (BooleanNat fstComp fstComp)+instance PairColimit Boolean Tru Tru where +  type Coproduct Tru Tru = Tru+  pairColimit = InitialUniversal (IdTru :***: IdTru) (BooleanNat fstComp sndComp)
+ Data/Category/Functor.hs view
@@ -0,0 +1,50 @@+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs #-}+module Data.Category.Functor where+  +import Prelude hiding ((.), id)++import Data.Category+++-- |Functor category Funct(C, D), or D^C.+-- Arrows of Funct(C, D) are natural transformations.+-- Each category C needs its own data instance.+data family Funct (c :: * -> * -> *) (d :: * -> * -> *) (a :: *) (b :: *) :: *++-- |Objects of Funct(C, D) are functors from C to D.+data FunctO (c :: * -> * -> *) (d :: * -> * -> *) (f :: *) = (Dom f ~ c, Cod f ~ d) => FunctO f++-- |Arrows of the category Funct(Funct(C, D), E)+-- I.e. natural transformations between functors of type D^C -> E+data instance Funct (Funct c d) e (FunctO (Funct c d) e f) (FunctO (Funct c d) e g) =+  FunctNat (forall h. (Dom h ~ c, Cod h ~ d) => Component f g (FunctO c d h))+++type Component f g z = Cod f (F f z) (F g z)+type f :~> g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Funct c d (FunctO c d f) (FunctO c d g)+++-- | The diagonal functor from (index-) category J to (~>).+data Diag (j :: * -> * -> *) ((~>) :: * -> * -> *) = Diag+type instance Dom (Diag j (~>)) = (~>)+type instance Cod (Diag j (~>)) = Funct j (~>)+type instance F (Diag j (~>)) a = FunctO j (~>) (Const j (~>) a)+++type InitMorF x u = (x :*-: Cod u) :.: u+type TermMorF x u = (Cod u :-*: x) :.: u+data InitialUniversal  x u a = InitialUniversal  (F (InitMorF x u) a) (InitMorF x u :~> (a :*-: Dom u))+data TerminalUniversal x u a = TerminalUniversal (F (TermMorF x u) a) (TermMorF x u :~> (Dom u :-*: a))++-- |A cone from N to F is a natural transformation from the constant functor to N to F.+type Cone   f n = Const (Dom f) (Cod f) n :~> f+-- |A co-cone from F to N is a natural transformation from F to the constant functor to N.+type Cocone f n = f :~> Const (Dom f) (Cod f) n++type Limit   f l = TerminalUniversal (FunctO (Dom f) (Cod f) f) (Diag (Dom f) (Cod f)) l+type Colimit f l = InitialUniversal  (FunctO (Dom f) (Cod f) f) (Diag (Dom f) (Cod f)) l++data Adjunction f g = Adjunction +  { unit :: Id (Dom f) :~> (g :.: f)+  , counit :: (f :.: g) :~> Id (Dom g)+  }
+ Data/Category/Hask.hs view
@@ -0,0 +1,77 @@+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs, EmptyDataDecls #-}+module Data.Category.Hask where++import Prelude hiding ((.), id)+import qualified Prelude+import Control.Arrow ((&&&), (***), (+++))++import Data.Category+import Data.Category.Functor+import Data.Category.Void+import Data.Category.Pair++type Hask = (->)++instance Apply (->) a b where+  ($$) = ($)++instance CategoryO (->) a where+  id = Prelude.id+  +instance CategoryA (->) a b c where+  (.) = (Prelude..)++++newtype instance Funct (->) d (FunctO (->) d f) (FunctO (->) d g) = +  HaskNat { unHaskNat :: (forall a. CategoryO d (F f a) => Component f g a) }+instance (Dom f ~ (->), Cod f ~ d) => CategoryO (Funct (->) d) (FunctO (->) d f) where+  id = HaskNat id+instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag (->) (~>)) a b where+  Diag % f = HaskNat f+++data Zero+-- With thanks to Conor McBride+magic :: Zero -> a+magic x = x `seq` error "we never get this far"++instance VoidColimit (->) where+  type InitialObject (->) = Zero+  voidColimit = InitialUniversal VoidNat (HaskNat $ \VoidNat -> magic)+instance VoidLimit (->) where+  type TerminalObject (->) = ()+  voidLimit = TerminalUniversal VoidNat (HaskNat $ \VoidNat -> const ())++initObjInHask :: Limit (Id (->)) Zero+initObjInHask = TerminalUniversal (HaskNat $ magic) (HaskNat unHaskNat)+termObjInHask :: Colimit (Id (->)) ()+termObjInHask = InitialUniversal (HaskNat $ const ()) (HaskNat unHaskNat)++instance PairColimit (->) x y where+  type Coproduct x y = Either x y+  pairColimit = InitialUniversal (Left :***: Right) (HaskNat $ \(l :***: r) -> either l r)+instance PairLimit (->) x y where+  type Product x y = (x, y)+  pairLimit = TerminalUniversal (fst :***: snd) (HaskNat $ \(f :***: s) -> f &&& s)+++data ProdInHask = ProdInHask+type instance Dom ProdInHask = Funct Pair (->)+type instance Cod ProdInHask = (->)+type instance F ProdInHask (FunctO Pair (->) f) = (F f Fst, F f Snd)+instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA ProdInHask (FunctO Pair (->) f) (FunctO Pair (->) g) where+  ProdInHask % (f :***: g) = f *** g++prodInHaskAdj :: Adjunction (Diag Pair (->)) ProdInHask+prodInHaskAdj = Adjunction { unit = HaskNat $ id &&& id, counit = FunctNat $ fst :***: snd }++data SumInHask = SumInHask+type instance Dom SumInHask = Funct Pair (->)+type instance Cod SumInHask = (->)+type instance F SumInHask (FunctO Pair (->) f) = Either (F f Fst) (F f Snd)+instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA SumInHask (FunctO Pair (->) f) (FunctO Pair (->) g) where+  SumInHask % (f :***: g) = f +++ g++sumInHaskAdj :: Adjunction SumInHask (Diag Pair (->))+sumInHaskAdj = Adjunction { unit = FunctNat $ Left :***: Right, counit = HaskNat $ either id id }
+ Data/Category/Kleisli.hs view
@@ -0,0 +1,44 @@+{-# LANGUAGE TypeFamilies, TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}+module Data.Category.Kleisli where+  +import Prelude hiding ((.), id, Monad(..))++import Data.Category+import Data.Category.Functor+import Data.Category.Hask+import Unsafe.Coerce++class Pointed m where+  point :: m -> Id (Cod m) :~> m+  +class Pointed m => Monad m where+  join :: m -> (m :.: m) :~> m+  +data Kleisli ((~>) :: * -> * -> *) m a b = Kleisli (m -> a ~> F m b)++instance (Monad m, Dom m ~ (->), Cod m ~ (->)) => CategoryO (Kleisli (->) m) o where+  id = Kleisli $ \m -> unHaskNat (point m)+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 -> unsafeCoerce (unHaskNat (join m)) . (m % f m) . g m+newtype instance Funct (Kleisli (->) m) d (FunctO (Kleisli (->) m) d f) (FunctO (Kleisli (->) m) d g) = +  KleisliNat { unKleisliNat :: (forall a. CategoryO d (F f a) => Component f g a) }++data KleisliAdjF ((~>) :: * -> * -> *) m = KleisliAdjF m+type instance Dom (KleisliAdjF (~>) m) = (~>)+type instance Cod (KleisliAdjF (~>) m) = Kleisli (~>) m+type instance F (KleisliAdjF (~>) m) a = a+instance (Monad m, Dom m ~ (->), Cod m ~ (->)) => FunctorA (KleisliAdjF (->) m) a b where+  KleisliAdjF _ % f = Kleisli $ \m -> unHaskNat (point m) . f+  +data KleisliAdjG ((~>) :: * -> * -> *) m = KleisliAdjG m+type instance Dom (KleisliAdjG (~>) m) = Kleisli (~>) m+type instance Cod (KleisliAdjG (~>) m) = (~>)+type instance F (KleisliAdjG (~>) m) a = F m a+instance (Monad m, Dom m ~ (->), Cod m ~ (->), FunctorA m a (F m b)) => FunctorA (KleisliAdjG (->) m) a b where+  KleisliAdjG m % Kleisli f = unsafeCoerce (unHaskNat (join m)) . (m % f m)++instance (Pointed m, Dom m ~ (->), Cod m ~ (->)) => Pointed (KleisliAdjG (->) m :.: KleisliAdjF (->) m) where+  point (KleisliAdjG m :.: _) = HaskNat (unHaskNat (point m))+   +kleisliAdj :: (Monad m, Dom m ~ (->), Cod m ~ (->)) => m -> Adjunction (KleisliAdjF (->) m) (KleisliAdjG (->) m)+kleisliAdj m = Adjunction { unit = point (KleisliAdjG m :.: KleisliAdjF m), counit = KleisliNat (Kleisli $ \m -> undefined) }
+ Data/Category/Omega.hs view
@@ -0,0 +1,85 @@+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}+module Data.Category.Omega where++import Prelude hiding ((.), id)++import Data.Category+import Data.Category.Functor+import Data.Category.Void+import Data.Category.Pair+++-- Natural numbers, the omega Category 0 -> 1 -> 2 -> 3 ...+data family Omega a b :: * ++-- Objects+data Z = Z deriving Show+newtype S n = S { unS :: n } deriving Show++-- Arrows, there's an arrow from a to b when a is less than or equal to b+data instance Omega Z Z = IdZ+newtype instance Omega Z (S n) = GTZ { unGTZ :: Omega Z n }+newtype instance Omega (S a) (S b) = StepS { unStepS :: Omega a b }++instance Apply Omega Z Z where+  IdZ $$ Z = Z+instance Apply Omega Z n => Apply Omega Z (S n) where+  GTZ d $$ Z = S (d $$ Z)+instance Apply Omega a b => Apply Omega (S a) (S b) where+  StepS d $$ S a = S (d $$ a)++instance CategoryO Omega Z where+  id = IdZ+instance (CategoryO Omega n) => CategoryO Omega (S n) where+  id = StepS id++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+  (StepS a) . (GTZ n) = GTZ (a . n)+instance (CategoryA Omega n p q) => CategoryA Omega (S n) (S p) (S q) where+  (StepS a) . (StepS b) = StepS (a . b)+++data instance Funct Omega d (FunctO Omega d f) (FunctO Omega d g) = +  OmegaNat (Component f g Z) (forall n. CategoryO d (F f (S n)) => Component f g n -> Component f g (S n))+instance (Dom f ~ Omega, Cod f ~ d, CategoryO (Cod f) (F f Z)) => CategoryO (Funct Omega d) (FunctO Omega d f) where+  id = OmegaNat id (const id)++instance VoidColimit Omega where+  type InitialObject Omega = Z+  voidColimit = InitialUniversal VoidNat (OmegaNat (\VoidNat -> IdZ) (\cpt VoidNat -> GTZ (cpt VoidNat)))++-- The product in omega is the minimum.+instance PairLimit Omega Z Z where +  type Product Z Z = Z+  pairLimit = TerminalUniversal (IdZ :***: IdZ) (OmegaNat fstComp (\cpt -> sndComp))+instance (PairLimit Omega Z n, Product Z n ~ Z) => PairLimit Omega Z (S n) where +  type Product Z (S n) = Z+  pairLimit = TerminalUniversal (IdZ :***: GTZ p) (OmegaNat fstComp (\cpt -> fstComp)) where+    TerminalUniversal (_ :***: p) _ = pairLimit :: Limit (PairF Omega Z n) (Product Z n)+instance (PairLimit Omega n Z, Product n Z ~ Z) => PairLimit Omega (S n) Z where +  type Product (S n) Z = Z+  pairLimit = TerminalUniversal (GTZ p :***: IdZ) (OmegaNat sndComp (\cpt -> sndComp)) where+    TerminalUniversal (p :***: _) _ = pairLimit :: Limit (PairF Omega n Z) (Product n Z)+instance (PairLimit Omega a b) => PairLimit Omega (S a) (S b) where +  type Product (S a) (S b) = S (Product a b)+  pairLimit = TerminalUniversal (StepS p1 :***: StepS p2) undefined where+    TerminalUniversal (p1 :***: p2) _ = pairLimit :: Limit (PairF Omega a b) (Product a b)++-- The coproduct in omega is the maximum.+instance PairColimit Omega Z Z where +  type Coproduct Z Z = Z+  pairColimit = InitialUniversal (IdZ :***: IdZ) (OmegaNat fstComp (\cpt -> sndComp))+instance (PairColimit Omega Z n, Coproduct Z n ~ n) => PairColimit Omega Z (S n) where +  type Coproduct Z (S n) = S n+  pairColimit = InitialUniversal (GTZ p1 :***: StepS p2) (OmegaNat sndComp (\cpt -> sndComp)) where+    InitialUniversal (p1 :***: p2) _ = pairColimit :: Colimit (PairF Omega Z n) (Coproduct Z n)+instance (PairColimit Omega n Z, Coproduct n Z ~ n) => PairColimit Omega (S n) Z where +  type Coproduct (S n) Z = S n+  pairColimit = InitialUniversal (StepS p1 :***: GTZ p2) (OmegaNat fstComp (\cpt -> fstComp)) where+    InitialUniversal (p1 :***: p2) _ = pairColimit :: Colimit (PairF Omega n Z) (Coproduct n Z)+instance (PairColimit Omega a b) => PairColimit Omega (S a) (S b) where +  type Coproduct (S a) (S b) = S (Coproduct a b)+  pairColimit = InitialUniversal (StepS p1 :***: StepS p2) undefined where+    InitialUniversal (p1 :***: p2) _ = pairColimit :: Colimit (PairF Omega a b) (Coproduct a b)
+ Data/Category/Pair.hs view
@@ -0,0 +1,64 @@+{-# LANGUAGE TypeFamilies, TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}+module Data.Category.Pair where++import Prelude hiding ((.), id)++import Data.Category+import Data.Category.Functor++data family Pair a b :: *++data Fst = Fst deriving Show+data Snd = Snd deriving Show++data instance Pair Fst Fst = IdFst+data instance Pair Snd Snd = IdSnd++instance Apply Pair Fst Fst where+  IdFst $$ Fst = Fst+instance Apply Pair Snd Snd where+  IdSnd $$ Snd = Snd+  +instance CategoryO Pair Fst where+  id = IdFst+instance CategoryO Pair Snd where+  id = IdSnd++instance CategoryA Pair Fst Fst Fst where+  IdFst . IdFst = IdFst+instance CategoryA Pair Snd Snd Snd where+  IdSnd . IdSnd = IdSnd++data instance Funct Pair d (FunctO Pair d f) (FunctO Pair d g) = +  (:***:) { fstComp :: Component f g Fst, sndComp :: Component f g Snd }+instance (CategoryO (Cod f) (F f Fst), CategoryO (Cod f) (F f Snd)) => CategoryO (Funct Pair d) (FunctO Pair d f) where+  id = id :***: id+instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag Pair (~>)) a b where+  Diag % f = f :***: f+++data PairF ((~>) :: * -> * -> *) x y = PairF+type instance Dom (PairF (~>) x y) = Pair+type instance Cod (PairF (~>) x y) = (~>)+type instance F (PairF (~>) x y) Fst = x+type instance F (PairF (~>) x y) Snd = y+instance (CategoryO (~>) x) => FunctorA (PairF (~>) x y) Fst Fst where+  PairF % IdFst = id+instance (CategoryO (~>) y) => FunctorA (PairF (~>) x y) Snd Snd where+  PairF % IdSnd = id++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+  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)+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+  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)+
+ Data/Category/Unit.hs view
@@ -0,0 +1,17 @@+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}+module Data.Category.Unit where++import Data.Category++-- "1", Singleton category+data family Unit a b :: *++data instance Unit () () = UnitId++instance Apply Unit () () where+  UnitId $$ () = ()+  +instance CategoryO Unit () where+  id = UnitId+instance CategoryA Unit () () () where+  UnitId . UnitId = UnitId
+ Data/Category/Void.hs view
@@ -0,0 +1,26 @@+{-# LANGUAGE TypeFamilies, FlexibleInstances, MultiParamTypeClasses #-}+module Data.Category.Void where++import Data.Category+import Data.Category.Functor++-- Void, the empty category+data family Void a b :: *++data instance Funct Void d (FunctO Void d f) (FunctO Void d g) = +  VoidNat+instance CategoryO (Funct Void d) (FunctO Void d f) where+  id = VoidNat+instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag Void (~>)) a b where+  Diag % f = VoidNat++data VoidF ((~>) :: * -> * -> *) = VoidF+type instance Dom (VoidF (~>)) = Void+type instance Cod (VoidF (~>)) = (~>)++class VoidColimit (~>) where+  type InitialObject (~>) :: *+  voidColimit :: Colimit (VoidF (~>)) (InitialObject (~>))+class VoidLimit (~>) where+  type TerminalObject (~>) :: *+  voidLimit :: Limit (VoidF (~>)) (TerminalObject (~>))
+ LICENSE view
@@ -0,0 +1,31 @@+Copyright Sjoerd Visscher 2010++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Sjoerd Visscher nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.+
+ Setup.lhs view
@@ -0,0 +1,3 @@+#!/usr/bin/env runhaskell+> import Distribution.Simple+> main = defaultMain
+ data-category.cabal view
@@ -0,0 +1,26 @@+name:                data-category+version:             0.0.1+synopsis:            Restricted categories+description:         +  Data-category is a collection of categories, and some categorical constructions on them.+category:            Data+license:             BSD3+license-file:        LICENSE+author:              Sjoerd Visscher+maintainer:          sjoerd@w3future.com+build-type:          Simple+cabal-version:       >= 1.2++Library+  exposed-modules:     +    Data.Category,+    Data.Category.Functor,+    Data.Category.Void,+    Data.Category.Unit,+    Data.Category.Pair,+    Data.Category.Boolean,+    Data.Category.Omega,+    Data.Category.Hask,+    Data.Category.Kleisli+    +  build-depends:       base >= 3 && < 5