How to implement type theory in an hour
I was purging the disk on my laptop of large files and found a video lecture which I forgot to publish. Here it is with some delay. I lectured on how to implement type theory at the School and Workshop on Univalent Mathematics in December 2017, at the University of Birmingham (UK).
You may visit the GitHub repository spartan-type-theory. There used to be a video, but I lost it.