Outlines, plans, recordings, homeworks, and misc files related to some talks, seminars, and courses I did.
(in Russian) Jan Malakhovski. Introduction to Agda (Ян Малаховски. Введение в Agda) organized by (in Russian) The Journal of «The Practice of Functional Programming» (Журнал «Практика функционального программирования»)
The discussion after that talk spurned the publishing of my Brutal Introduction to Dependent Types in Agda.