The informal language of mathematics uses types and sets, but when mathematicians want to be rigorous about a concept, they tend to rely on the 100 year old tradition of reducing it to concepts in pure set theory. In these lectures, we will find the rigorous concepts in type theory. For pedagogical reasons, we will often mention the set theory version of a concept as well.
The idea of a type is built up inductively (as is the Zermelo hierarchical concept of set). We start with primitive types and type constructors.