The main topic of this dissertation is Quine’s set theory with atoms (NFU), which can be regarded as a form of type theory. The dissertation is divided into two parts. In the first part, we rigorously formalize the syntax and develop the theory NFU. Then we develop the theory of cardinal numbers, using Kuratowski’s ordered pairs. The main contribution of this part is a proof of the cardinal squaring principle. Using it, we define type-level ordered pairs and present the alternative axiomatic extension of NFU. After that, we introduce the basic concepts of ordinal numbers in the alternative axiomatization and continue to develop the theory of cardinal numbers. The second part is the exposition of Boffa’s construction of a model for NFU, using the model of Zermelo–Fraenkel’s set theory. We show that Boffa’s construction yields a model for NFU and we then construct a model for NFU with the axiom of infinity and NFU with the axiom of choice. In the end, we show how to construct a model for NFU with both the axiom of infinity and choice and then consequently for the alternative axiomatization.