I would highly recommend "PROGRAM = PROOF" by Samuel Mimram. It covers everything from pure lambda calculus through dependent type theory up to homotopy type t

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/pp/course.pdf https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching... https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/publications/ https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/publicat...