Lecture outline :
- aczel's translation of set theory into type theory ;
- miquel's variation for not necessarily well-founded sets ;
- application to the problem of the logical strength of certain type systems, in particular the Lean system (Mario Carneiro).
