data-category 0.6.0 → 0.6.1

raw patch · 2 files changed

+115/−2 lines, 2 files

Files

• Data/Category/Cube.hs +112/−0
• data-category.cabal +3/−2

@@ -0,0 +1,112 @@+{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, TypeOperators, UndecidableInstances, NoImplicitPrelude #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Cube+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+--+-- The cube category.+-----------------------------------------------------------------------------+module Data.Category.Cube 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+++data Sign = M | P++data Cube :: * -> * -> * where+  Z :: Cube Z Z+  S :: Cube x y -> Cube (S x) (S y)+  Y :: Sign -> Cube x y -> Cube x (S y) -- face maps+  X :: Cube x y -> Cube (S x) y -- degeneracy map+++instance Category Cube where+  src Z = Z+  src (S c) = S (src c)+  src (Y _ c) = src c+  src (X c) = S (src c)++  tgt Z = Z+  tgt (S c) = S (tgt c)+  tgt (Y _ c) = S (tgt c)+  tgt (X c) = tgt c++  Z . c = c+  c . Z = c+  S c . S d = S (c . d)+  S c . Y s d = Y s (c . d)+  Y s c . d = Y s (c . d)+  X c . S d = X (c . d)+  X c . Y _ d = c . d+  c . X d = X (c . d)+++instance HasTerminalObject Cube where+  type TerminalObject Cube = Z++  terminalObject = Z++  terminate Z = Z+  terminate (S f) = X (terminate f)+++data Sign0 = SM | S0 | SP++data ACube :: * -> * where+  Nil :: ACube Z+  Cons :: Sign0 -> ACube n -> ACube (S n)++data Forget = Forget+-- | Turn @Cube x y@ arrows into @ACube x -> ACube y@ functions.+instance Functor Forget where+  type Dom Forget = Cube+  type Cod Forget = (->)+  type Forget :% n = ACube n+  Forget % Z     = \x -> x+  Forget % S f   = \(Cons s x) -> Cons s ((Forget % f) x)+  Forget % Y M f = \x -> Cons SM ((Forget % f) x)+  Forget % Y P f = \x -> Cons SP ((Forget % f) x)+  Forget % X f   = \(Cons _ x) -> (Forget % f) x+++data Add = Add+-- | Ordinal addition is a bifuntor, it concattenates the maps as it were.+instance Functor Add where+  type Dom Add = Cube :**: Cube+  type Cod Add = Cube+  type Add :% (Z  , n) = n+  type Add :% (S m, n) = S (Add :% (m, n))+  Add % (Z     :**: g) = g+  Add % (S f   :**: g) = S   (Add % (f :**: g))+  Add % (Y s f :**: g) = Y s (Add % (f :**: g))+  Add % (X f   :**: g) = X   (Add % (f :**: g))+++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 (S n) = S (rightUnitor Add n)+  rightUnitorInv Add    Z  = Z+  rightUnitorInv Add (S n) = S (rightUnitorInv Add n)+  associator     Add Z    Z  n = n+  associator     Add Z (S m) n = S (associator Add Z m n)+  associator     Add (S l) m n = S (associator Add l m n)+  associatorInv  Add Z    Z  n = n+  associatorInv  Add Z (S m) n = S (associatorInv Add Z m n)+  associatorInv  Add (S l) m n = S (associatorInv Add l m n)

@@ -1,5 +1,5 @@ name:                data-category-version:             0.6.0+version:             0.6.1 synopsis:            Category theory  description:         Data-category is a collection of categories, and some categorical constructions on them.@@ -48,8 +48,9 @@     Data.Category.Dialg,     Data.Category.NNO,     Data.Category.Simplex,+    Data.Category.Cube,     Data.Category.Comma-    +   default-language:    Haskell2010  source-repository head