- 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
- Improving techniques, methods and tools of automatic verification, interview with Herman Geuvers
- Propositions as Types by Thorsten Altenkirch (University of Nottingham, UK) on the Computerphile channel
- Why Type Theory matters by Thorsten Altenkirch (University of Nottingham, UK) at Lambda Days 2019 in Krakow
- Lectures on the Curry-Howard correspondence by Xavier Leroy and others.
- Programming with Monadic CSP Style Processes in Dependent Type Theory talk by Anton Setzer (Swansea University) at TyDe2016
- An Agda formalization of the transitive closure of block matrices talk by Adam Sandberg Eriksson (Chalmers University) at TyDe2016
- Separation Logic and Concurrency lectures by Aleksandar Nanevski at Lecture notes for Oregon Programming Languages Summer School (OPLSS) (June 2016).

- 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
- HoTT-2019, course by Andrej Bauer and Jaka Smrekar