 Before ending our tour of varieties of modern constructive mathematics, we visit a fourth variety, ML, based on Per Martin-Löf’s  intuitionistic type theory.  Martin-Löf published his Notes on Constructive Mathematics [1968], based on lectures he had given in Europe in 1966–68; so his involvement with constructivism in mathematics goes back at least to the period of Bishop’s writing of Foundations of Constructive Analysis. Martin-Löf’s book is in the spirit of RUSS, rather than BISH; indeed, its author did not have access to Bishop’s book until his own manuscript was finished. Martin-Löf later turned his attention to his theory of types as a foundation for Bishop-style constructive mathematics. 