Elementary Discrete Sets in Martin-Löf Type Theory
Mikael Fors · KTH Publication Database DiVA (KTH Royal Institute of Technology) · 2012
The concept of reducibility in the sense of computation is a central theme of computer science. Classic set theory, however, does not fully reflect this discrete notion. In Martin-Lof type theory, a set is viewed from a type-centric perspective; allowing more explicit structures to be considered. In this thesis we explore basic countable discrete sets from said type-centric perspective. While a keen focus on the notion of set is maintained, we also discuss the basic outline of the intuitionistic logic which the theory is based on.