meta_cats http://www.openmath.org/cd/meta_cats.ocd 2005-04-01 experimental 2002-06-17 0 0 This CD holds symbols for making meta statements about categories has This symbol represents the notion of category inclusion. It takes two arguments, which should both be categories. It implies that axioms of the second argument apply to the first, and that function signatures in the second category are also in the first. field has group Category This symbol is intended to denote the type of a category. the type of field is Category domain These objects have categories as there types and specific implementations of their functions. *** details to be worked out *** *** for now *** The first argument is a Category, the remaining arguments are the functions (e.g. lambda bindings or unapplied functions). type This symbol is unary and returns the type of its argument.