diff options
| author | dos-reis <gdr@axiomatics.org> | 2010-06-29 19:08:33 +0000 |
|---|---|---|
| committer | dos-reis <gdr@axiomatics.org> | 2010-06-29 19:08:33 +0000 |
| commit | 2394bfc186f7b57a7b8b737b4b17e1140d756416 (patch) | |
| tree | 7492c9de0429f3dfb0dd28bcaff91521f0be7d55 /src/algebra/catdef.spad.pamphlet | |
| parent | 77d293322d11ad09575a85f421796da7db471797 (diff) | |
| download | open-axiom-2394bfc186f7b57a7b8b737b4b17e1140d756416.tar.gz | |
* algebra/catdef.spad.pamphlet (OrderedType): New.
Diffstat (limited to 'src/algebra/catdef.spad.pamphlet')
| -rw-r--r-- | src/algebra/catdef.spad.pamphlet | 29 |
1 files changed, 26 insertions, 3 deletions
diff --git a/src/algebra/catdef.spad.pamphlet b/src/algebra/catdef.spad.pamphlet index 06723e56..76b0f796 100644 --- a/src/algebra/catdef.spad.pamphlet +++ b/src/algebra/catdef.spad.pamphlet @@ -245,9 +245,10 @@ BasicType(): Category == Type with ++ Category of types equipped with a total ordering. ++ Axioms: ++ forall(x,y) -++ x > y = y < x -++ x <= y = not(y > x) -++ x >= y = not(x < y) +++ x > y <=> y < x +++ x <= y <=> not(y > x) +++ x >= y <=> not(x < y) +++ x <= y and x >= y => x = y OrderedType(): Category == BasicType with < : (%,%) -> Boolean ++ \spad{x < y} holds if \spad{x} is less than \spad{y} in the @@ -282,6 +283,27 @@ OrderedType(): Category == BasicType with @ +\section{Ordered Structure} + +<<domain ORDSTRCT OrderedStructure>>= +++ Author: Gabriel Dos Reis +++ Date Created: June 28, 2010 +++ Date Last Modified: June 28, 2010 +++ See Also: OrderedType +++ Description: +++ This domain turns any total ordering \spad{f} on a type \spad{T} into +++ a model of the category \spadtype{OrderedType}. +)abbrev domain ORDSTRCT OrderedStructure +OrderedStructure(T: Type,f: (T,T) -> Boolean): Public == Private where + Public == Join(OrderedType,HomotopicTo T) + Private == T add + coerce(x: %): T == rep x + coerce(y: T): % == per y + x < y == f(rep x,rep y) + +@ + + \section{category BMODULE BiModule} @@ -2032,6 +2054,7 @@ VectorSpace(S:Field): Category == Module(S) with <<category BASTYPE BasicType>> <<category ORDTYPE OrderedType>> +<<domain ORDSTRCT OrderedStructure>> <<category SETCAT SetCategory>> <<category STEP StepThrough>> <<category SGROUP SemiGroup>> |