MonCat.hs

module Categories where

-- | Definition of a category enriched over the language. The sets of objects
-- are represented by constraints.
class Category ob_c hom_c where
  unit :: (ob_c x) => hom_c x x                        
  comp :: (ob_c x) => hom_c y z -> hom_c x y -> hom_c x z


-- | Bifunctors.
class (
  Category ob_c hom_c,
  Category ob_d hom_d,
  Category ob_e hom_e,
  forall x y. 
    (ob_c x , ob_d y)
    => ob_e (f x y)
)
=> Bifunctor ob_c hom_c
             ob_d hom_d
             ob_e hom_e f 
where

  bimap :: (
    ob_c x1,
    ob_c x2,
    ob_d y1,
    ob_d y2
  )
  => hom_c x1 x2 
     -> hom_d y1 y2
     -> hom_e (f x1 y1) (f x2 y2)

-- | Monoidal categories.
-- The definition follows that of a enriched monoidal category, taking Hask as the base of enrichment.
class (
  Category ob_a hom_a,
  Bifunctor
    ob_a hom_a
    ob_a hom_a 
    ob_a hom_a m,
  ob_a i
)
=> MonoidalCategory ob_a hom_a m i 
where
  
  alpha:: (
    ob_a x,
    ob_a y,
    ob_a z
  ) 
  => hom_a 
       (m x (m y z))
       (m (m x y) z)
  
  alphainv:: (
    ob_a x,
    ob_a y,
    ob_a z
  )
  => hom_a (m x (m y z))
           (m (m x y) z)
  
  lambda    :: (ob_a x) => hom_a (m x i) x
  lambdainv :: (ob_a x) => hom_a x (m x i)
  rho       :: (ob_a x) => hom_a (m i x) x
  rhoinv    :: (ob_a x) => hom_a x (m i x)