Comment by leonidasrup

I would highly recommend "PROGRAM = PROOF" by Samuel Mimram.

It covers everything from pure lambda calculus through dependent type theory up to homotopy type theory. In comparison to the HoTT book, the book "PROGRAM = PROOF" is oriented less towards mathematicians more towards programmers. It contains also a short introduction to OCaml and Agda.

The book can downloaded from the authors web page:

https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching...

https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/publicat...