data-category 0.0.1 → 0.0.2
raw patch · 3 files changed
+20/−4 lines, 3 files
Files
- Data/Category/Hask.hs +1/−3
- Data/Category/Omega.hs +16/−0
- data-category.cabal +3/−1
Data/Category/Hask.hs view
@@ -24,9 +24,7 @@ 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+ HaskNat { unHaskNat :: forall a. Component f g a } instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag (->) (~>)) a b where Diag % f = HaskNat f
Data/Category/Omega.hs view
@@ -46,6 +46,22 @@ 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) +data OmegaF ((~>) :: * -> * -> *) z f = OmegaF+type instance Dom (OmegaF (~>) z f) = Omega+type instance Cod (OmegaF (~>) z f) = (~>)+type instance F (OmegaF (~>) z f) Z = z+type instance F (OmegaF (~>) z f) (S n) = F f (F (OmegaF (~>) z f) n)+instance CategoryO (~>) z => FunctorA (OmegaF (~>) z f) Z Z where+ OmegaF % IdZ = id++class CategoryO (~>) z => OmegaLimit (~>) z f where+ type OmegaL (~>) z f :: *+ omegaLimit :: Limit (OmegaF (~>) z f) (OmegaL (~>) z f)+class CategoryO (~>) z => OmegaColimit (~>) z f where+ type OmegaC (~>) z f :: *+ omegaColimit :: Colimit (OmegaF (~>) z f) (OmegaC (~>) z f)+ + instance VoidColimit Omega where type InitialObject Omega = Z voidColimit = InitialUniversal VoidNat (OmegaNat (\VoidNat -> IdZ) (\cpt VoidNat -> GTZ (cpt VoidNat)))
data-category.cabal view
@@ -1,5 +1,5 @@ name: data-category-version: 0.0.1+version: 0.0.2 synopsis: Restricted categories description: Data-category is a collection of categories, and some categorical constructions on them.@@ -8,6 +8,8 @@ license-file: LICENSE author: Sjoerd Visscher maintainer: sjoerd@w3future.com+stability: experimental+homepage: http://github.com/sjoerdvisscher/data-category build-type: Simple cabal-version: >= 1.2