Foundation-agnostic mathematics

Some parts of these notes aim to be foundation-agnostic. This means we use language which may appropriately be interpreted in a variety of foundations of mathematics, such that the theorems given are true under each semantics.

It could be argued that the best way to be foundation-agnostic is to work in a type theory like MLTT, which generally admits semantics for each foundational system. We do not take this approach, for historical and pedagogical reasons.