Abstract: After recalling the construction of identity types as inductive types, we will use the induction principle to prove basic facts about identity types. Throughout the talk, we will pursue the analogy between identity types and path spaces. We will illustrate how iterated identity types form a structure reminiscent of the low-dimensional data of an $\infty$-groupoid.