Plan du cours :
- modalités exactes à gauche ;
- application pour construire des nouveaux modèles de la théorie des types ;
- non prouvabilité de la thèse de Church et du choix dénombrable ;
- structure de modèle de Quillen et modèle constructif de la notion de types d'homotopie.
