"A Boolean Model of Ultrafilters."

Thierry Coquand (1999)
a service of  Schloss Dagstuhl - Leibniz Center for Informatics