- Naïve Type Theory by Thorsten Altenkirch (University of Nottingham, UK) at FOMUS 2016
- Type Theory for absolute beginners by Hanneli Tavante at Devoxx 2016 in Belgium
- The Type Theory Podcast
- On types and testing by Peter Dybjer
- On Idris by Edwin Brady
- On Homotopy Type Theory by Dan Licata
- On Zombie programming language and Dependent Haskell by Stephanie Weirich
- On CTT and Nuprl by Bob Constable
- On Cedille, a proof assistant based on the Calculus of Dependent Lambda Eliminations by Aaron Stump

- Type Theory and its Meaning Explanations by Jon Sterling at LambdaConf 2015

- Computer Science ∩ Mathematics (Type Theory) by Thorsten Altenkirch (University of Nottingham, UK) on the Computerphile channel
- Homotopy Type Theory: Vladimir Voevodsky - Computerphile by Thorsten Altenkirch (University of Nottingham, UK) on the Computerphile channel
- A Functional Programmer's Guide to Homotopy Type Theory presented by Dan Licata at ICFP'2016
- A working (class) introduction to Homotopy Type Theory: The favourite type theory of the proletariat by Sophie Taylor
- Lambda Jam 2014 - Gershom Bazerman - Homotopy Type Theory: What's the Big Idea