Your Waifu (ZFC) is Shit-Tier: Elementary Motivation for Constructive Type Theory
In December of 2017, I gave a fairly hyperbolic talk to the CWRU math club in which I presented a basic introduction to constructive type theory, and why one may be motivated to prefer constructive type theory for foundations over ZFC. Despite (or maybe because of?) how ridiculously over-the-top I took things at certain points in the talk, it seemed to pique the interest of several members in constructive mathematics. Here are the slides to that talk, given on December 1st, 2017.