Modalities and models of type theory

Lecture outline:

• exact modalities left;
• application to the construction of new type-theoretic models;
• unprovability of Church's thesis and countable choice;
• Quillen model structure and constructive model of the notion of homotopy types.