OpenMath Content Dictionary: meta_cats

Canonical URL:

http://www.openmath.org/cd/meta_cats.ocd

CD File:

meta_cats.ocd

CD as XML Encoded OpenMath:

meta_cats.omcd

Defines:

Category, domain, has, type

Date:

2002-06-17

Version:

0

Review Date:

2005-04-01

Status:

experimental

This CD holds symbols for making meta statements about categories

has

Description:

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.

Example:

field has group

Signatures:

sts

Category

Description:

This symbol is intended to denote the type of a category.

Example:

the type of field is Category

Signatures:

sts

domain

Description:

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).

Signatures:

sts

type

Description:

This symbol is unary and returns the type of its argument.

Signatures:

sts