I was looking into this after listening to a little story at the beginning of an ICFP19 talk by Wouter Swierstra, telling about Edsger W. Dijkstra telling about Martin-Löf telling about his type theory.
> He (Martin-Löf) was a very sympathetic speaker and convinced at least me (Dijkstra) that something (possibly even of great conceptual elegance) was going on. He spoke with an endearing care.
Dijkstra's notes (EWD879) that are quoted there are also a marvel in themselves. Like everything he ever wrote pretty much.
Welcome to your niu world ! We are a cute and loving international community Ｏ(≧▽≦)Ｏ !