2 Setting up the environment

In this chapter, we construct the ambient environment inside which our model will reside. To do this, we will set up various pieces of abstract machinery that will help us later. Some mathematical background not already in mathlib will be included in chapter A.