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.