Plan du cours :
- traduction d’Aczel de la théorie des ensembles en théorie des types ;
- variation de Miquel pour les ensembles non nécessairement bien fondés ;
- application au problème de la force logique de certains systèmes de types et en particulier du système Lean (Mario Carneiro).