While this starts strong, a heads up: it peters out quick. There's only about an hour of material here, and the last of the three parts is unfinished, in the se

While this starts strong, a heads up: it peters out quick. There's only about an hour of material here, and the last of the three parts is unfinished, in the sense that there are gaps, not just an abrupt ending. After finishing this I jumped over to wadler/kokke's programming language theory in AGDA: https://wenkokke.github.io/sf/ https://wenkokke.github.io/sf/ Which is also unfinished, but generally more comprehensive and better motivated. It also stands a much greater probability of being continued.