Indexed types and Curry-Howard for first-order quantifiers - a podcast by Aaron Stump

First-order quantifiers under CH are for types indexed by expressions from a different syntactic category than programs

Further episodes of Iowa Type Theory Commute

Further podcasts by Aaron Stump

Website of Aaron Stump