Abstract: We will discuss in more detail the rules that define types, along with examples. The focus will be on inductive types, which are characterized by their constructors. An important example of inductive types is given by identity types, which play the role of path spaces in the homotopical interpretation. We will discuss path induction and the higher groupoid structure obtained from iterated identity types.