Type Theory and Agda

A ten-minute talk I gave at the conclusion of Johns Hopkins University’s Directed Reading Program 2021. No recording is available, but the slides can be found here.