The traditional view is that theorem provers, and automated reasoning tools in general, serve as back-ends to other user-facing tools. In this talk, I outline an alternative view where one interacts directly with a theorem prover by embedding the syntax and semantics of other formalisms/tools within this medium. Both views can happily coexist, but there are many advantages, and some disadvantages, to living entirely within a theorem proving universe. We speculate on what life might look like inside such a universe.