This is a problem session talk I gave in HKU PL Gruop, the abstract of the talk is:
In this week, I will be discussing the basic idea of intrinsically typed systems and how they differ from the more commonly known extrinsic typed systems. I will also provide examples (Agda snippets) that demonstrate the potential of intrinsically typed systems in research by showcasing the integration of various language features.
Interested readers may want to skim over first three chapters (Lambda, Properties and Debruijn) of PLFA Part 2.