Constructive Notions of Set. Part I. Sets in Martin-Löf Type Theory
Firenze University Press