Abstract: We will discuss inductive types, which are defined using constructors. Examples include the unit type, sum types, and product types introduced last week. Then we will discuss proofs by induction in the context of inductive types. Lastly, we will discuss identity types, which will play the role of path spaces in the homotopical interpretation of type theory.