Foundations of Mathematics

There are several candidates for "foundations" for mathematics. A foundation for math is like a base layer to implement other mathematical ideas in. So for example, in set theory, we would model a function \(f:X \to Y\) as a kind of set \(\{ (x,y) \}\) where there are conditions like "if \((x,y_1)\) and \((x, y_2)\) are in the set, then \(y_1 = y_2\)", this is so we can write things like \(f(x)\) and have it be unambiguous.

If instead we used category theory as a foundation, then we would have to define a function in a way that made use of category theory's native abstractions.

Set Theory (ZFC)

Category Theory (ETCS) TODO

Homotopy Type Theory (HoTT) TODO