On this page we look at proving things in different theories, such as,
- Set Theory
- Type Theory
- Homotopy Type Theory
- Category Theory
In many areas, such as set theory, we use a logic over the theory.
When proving things we usually use Intuitionistic logic (see page here). Although there is also a connection between set theory and boolean logic which can be seen nicely in Venn diagrams.
Logic and Type Theory
|'It is useful to distinguish between the internal type theory of a category and the internal logic which sits on top of that type theory. The type theory is about constructing objects, while the logic is about constructing subobjects.'||see ncatlab|
|In type theory, types can represent both the structure and the logic within type theory.|
Logic and Category Theory
See topos theory