  To build a large library of mathematics, it seems more efficient to take
advantage of the inherent structure of mathematical theories. Various theory
presentation combinators have been proposed, and some have been implemented, in
both legacy and current systems. Surprisingly, the ``standard library'' of most
systems do not make pervasive use of these combinators.
  We present a set of combinators optimized for reuse, via the tiny theories
approach. Our combinators draw their power from the inherent structure already
present in the \emph{category of contexts} associated to a dependently typed
language. The current work builds on ideas originating in CLEAR and Specware
and their descendents (both direct and intellectual). Driven by some design
criteria for user-centric library design, our library-building experience via
the systematic use of combinators has fed back into the semantics of these
combinators, and later into an updated syntax for them.
