Proofs in Different Theories

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.

In type theory, types can represent both the structure and the logic within type theory.

EuclideanSpace

Equality of Types

In Set Theory
More on page here.

Two sets are equal if they contain the same elements (Principle of Extensionality).

If the set has structure then that would also have to be equal in some way.

In Category Theory
More on page here.

Often when comparing types we need some loser way of considering that two types are essentially the same.

Isomorphism is frequently the most appropriate type of equality. This is defined using a category theory way, that is, by external morphisms.

In Type Theory
More on page here.

In Homotopy Type Theory there is a different way to get isomorphism from equality. That is to allow types to be equal in many ways.

metadata block

see also:	Computation and Algebra
Correspondence about this page
Book Shop - Further reading. Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.
Commercial Software Shop Where I can, I have put links to Amazon for commercial software, not directly related to the software project, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.

This site may have errors. Don't use for critical systems.