Люксембургский Сад зимой

 

Programming in Martin-Löf type theory

https://intuitionistic.files.wordpress.com/2010/07/nordstrom-et-al-programming.pdf



Seems like the book covers the issue of defining Set.