I believe Victor is justified in expecting QED to support
a number of different mathematical theories. Not only can
this accommodate different formalisation preferences, and
different mathematical preferences, it also provides modularity.
Two reality checks.
* A lot of algebra is *not* done within algebraic theories.
E.g., to cite Hall's `Theory of Groups' again; after
cursory inspection I conjecture there's no single page,
all of whose mathematics could be formalised in the
standard (first order) theory of groups. Hall's universe
of discourse is obviously set theory.
* The modularity benefit is obtained only when it is possible
to interpret one theory in another. Specifying such interpretations
needs a meta-theoretic vocabulary.
I sympathise with Victor's desire to just get on with mathematics,
and for that reason my own practice in contributing to QED would be to ignore
constructive object theories. However we do need to confront the issues
involved in getting to where we want to go. Formalisation of mathematics
is certainly a major issue; modularity, and preferences for different
formalisations and theories are others. Yes, we could all go off tomorrow
and use/build systems which have hardwired support for our own preferences.
This is the `Tower of Babel' approach, and is what we're trying to escape
from, rather than what we seek.
John Staples