On this page we look at proving things in different theories, such as,

- Set Theory
- Type Theory
- Topology
- 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