product categories in scala

package scalaz

/**
 * Defines a category.
 *
 * <p>
 * All instances must satisfy 3 laws:
 * <ol>
 * <li><strong>left identity</strong><br/><code>∀ a. compose(id, a) == a</code></li>
 * <li><strong>right identity</strong><br/><code>∀ a. compose(a, id) == a</code></li>
 * <li><strong>associativity</strong><br/><code>∀ a b c. compose(a, compose(b, c)) == compose(compose(a, b), c)</code></li>
 * </ol>
 * </p>
 */

trait Hom { 
  type L
  type H>:L
  type C[_ >: L <: H, _ >: L <: H]
}

trait GeneralizedCategory { 
  type U <: Hom
  type =>:[A>:U#L<:U#H,B>:U#L<:U#H] = U#C[A,B]

  def id[A>:U#L<:U#H]: A =>: A
  def compose[A>:U#L<:U#H, B>:U#L<:U#H, C>:U#L<:U#H](
    f: B =>: C,
    g: A =>: B
  ): A =>: C
  def *[UY<:Hom](that : GeneralizedCategory {type U=UY}) = Category.ProductCategory[U,UY](this,that)
}

trait GeneralizedGroupoid extends GeneralizedCategory { 
  def invert[A>:U#L<:U#H,B>:U#L<:U#H](f : A =>: B): B =>: A
}

trait Category[~>:[_,_]] extends GeneralizedCategory { 
  trait U extends Hom { 
    type L = Nothing
    type H = Any
    type C[A,B] = ~>:[A,B] 
  }
}

trait Groupoid[~>:[_, _]] extends GeneralizedGroupoid with Category[~>:]

object Category {
  import Scalaz._
  import Leibniz._

  /* 
   * Product Categories
   */

  /** Index for a product category */
  sealed trait P[+IX,+IY] { type _1 = IX; type _2 = IY }

  case class ProductCategory[UX<:Hom,UY<:Hom](
    _1: GeneralizedCategory{type U = UX},
    _2: GeneralizedCategory{type U = UY} 
  ) extends GeneralizedCategory with Hom {
    type _1 = _1.type
    type _2 = _2.type
    type L = P[UX#L,UY#L]
    type H = P[UX#H,UY#H]
    case class C[A>:L<:H,B>:L<:H](
      _1: UX#C[A#_1,B#_1],
      _2: UY#C[A#_2,B#_2]
    ) extends P[UX#C[A#_1,B#_1], UY#C[A#_2,B#_2]]
    type U = ProductCategory[UX,UY]

    def id[A>:U#L<:U#H] = C(_1.id[A#_1],_2.id[A#_2])
    def compose [A>:U#L<:U#H, B>:U#L<:U#H, C>:U#L<:U#H](f: B =>: C, g: A =>: B) = 
      C(_1.compose(f._1,g._1), _2.compose(f._2,g._2))
  }
}