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

Thierry Coquand

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.