The mystery of equality; the notion of type as a generalization of the notion of set

Lecture outline:

• how to represent the notion of equality in type theory;
• Voevodsky stratification of types;
• a uniform definition of the notion of equivalence;
• principle of univalence;
• application of mathematical structures to the notion of equality and comparison with set theory.