This chapter contains brief descriptions of some of the libraries which have been built with Nuprl. The accounts are intended to convey the flavor of various kinds of formalized mathematics. In much of the presentation which follows the theorems, definitions and proofs shown are not exactly in the form that would be displayed on the screen by Nuprl , although they come from actual Nuprl sessions (via the snapshot feature). The theorems (anything starting with `` >>'') will have some white space (i.e., carriage returns and blanks) added, while the DEF objects will have additional white space as well as escape characters and many of the parentheses omitted. (Usually the right--hand sides of definitions have seemingly redundant parentheses; these ensure correct parsing in any context.)