  As the prototypical category, $\mathbf{Set}$ has many properties which make
it special amongst categories. From the point of view of mathematical logic,
one such property is that $\mathbf{Set}$ has enough structure to "properly"
formalise logic. However, we could ask what it might mean to formalise logic in
another category $\mathbf{C}$. The notion of an (elementary) topos distills the
essential features of $\mathbf{Set}$ which allow us to do this. This expository
report defines topoi, and describes the development of first-order logic and
set theory within a topos.
