If you know Haskell, or are willing to learn, this is a brilliant explanation with code (you build a dependently typed language as you go). It ramps you up very fast yet each step is accessible. This alone really caused me to get bit by the dependent type bug.

https://augustss.blogspot.com/2007/10/simpler-easier-in-rece...

Here is the example code from this post

https://github.com/scott-fleischman/simpler-easier?files=1