  It is commonly believed that algebraic notions of type theory support only
universes \`a la Tarski, and that universes \`a la Russell must be removed by
elaboration. We clarify the state of affairs, recalling the details of
Cartmell's discipline of _generalized algebraic theory_, showing how to
formulate an algebraic version of Coquand's cumulative cwfs with universes \`a
la Russell. To demonstrate the power of algebraic techniques, we sketch a
purely algebraic proof of canonicity for Martin-L\"of Type Theory with
universes, dependent function types, and a base type with two constants.
