[cinnamonheart]

>Also, more tangential, but this comment section might attract people who know the answer: any good resources for getting started on type systems more generally?

I like Philip Wadler's Programming Language Foundations in Agda: https://plfa.github.io/

>The original goal was to simply adapt Software Foundations, maintaining the same text but transposing the code from Coq to Agda. But it quickly became clear to me that after five years in the classroom I had my own ideas about how to present the material. They say you should never write a book unless you cannot not write the book, and I soon found that this was a book I could not not write.

I found Agda + PLFA was more approachable for me than Coq + Software Foundations.

(Edit: clarifying that I'm responding to the tangent.)