Introduction to Type Theory

The essence of the type theory approach to mathematical logic is that the semenatic rules only allow you to construct true statements from other true statements.

Heirachy of Types

It is up to you how you define your hierachy of types. Generally it is good to have a Prop type that is the type of propositions. The type hierachy A:B:C can be read as "The C of A is B".

Logic