This thesis consists of four papers on type theory and a formalisation of certain results from the two first papers in the Agda language. We cover topics such as models of multisets and sets in Homotopy Type Theory, and explore ideas of using type theory as a language for databases and different ways of expressing dependencies between terms. The two first papers build on work by Aczel 1978. We establish that the underlying type of Aczel’s model of set theory in type theory can be seen as a type of multisets from the perspective of Homotopy Type Theory, and we identify a suitable subtype which becomes a model of set theory in which equality of sets is the identity type. The third paper is joint work with Henrik Forssell and David I .Spivak and explores a certain model of type theory, consisting of simplicial complexes, from the perspective of database theory. In the fourth and final paper, we consider two approaches to unraveling the dependency structures between terms in dependent type theory, and formulate a few conjectures about how these two approaches relate.

No description available.

In this paper we show how to give an intrinsic definition of a constructible circle on the sphere. The classical definition of constructible circle in the plane, using straight edge and compass is there by translated in ters of so called Lenart tools. The process by which we achieve our goal involves concepts from the algebra of Hermitian matrices, complex variables, and Sterographic projection. However, the discussion is entirely elementary throughout and hopefully can serve as a guide for teachers in advanced geometry.

In this paper we will study the 1p spaces. We will begin with definitions and different examples of 1p spaces. In particular, we will prove Holder's and Minkowski's inequalities for 1p sequence.

We present a novel theorem of Borel Combinatorics that sheds light on the types of continuous functions that can be defined on the Cantor space. We specifically consider the part X=F(2ᴳ) from the Cantor space, where the group G is the additive group of integer pairs ℤ². That is, X is the set of aperiodic {0,1} labelings of the two-dimensional infinite lattice graph. We give X the Bernoulli shift action, and this action induces a graph on X in which each connected component is again a two-dimensional lattice graph. It is folklore that no continuous (indeed, Borel) function provides a two-coloring of the graph on X, despite the fact that any finite subgraph of X is bipartite. Our main result offers a much more complete analysis of continuous functions on this space. We construct a countable collection of finite graphs, each consisting of twelve "tiles", such that for any property P (such as "two-coloring") that is locally recognizable in the proper sense, a continuous function with property P exists on X if and only if a function with a corresponding property P' exists on one of the graphs in the collection. We present the theorem, and give several applications.

Spreading models have become fundamental to the study of asymptotic geometry in Banach spaces. The existence of spreading models in every Banach space, and the so-called good sequences which generate them, was one of the first applications of Ramsey theory in Banach space theory. We use Ramsey theory and other techniques from infinitary combinatorics to examine some old and new questions concerning spreading models and good sequences. First, we consider the lp spreading model problem which asks whether a Banach space contains lp provided that every spreading model of a normalized block basic sequence of the basis is isometrically equivalent to lp. Next, using the Hindman-Milliken-Taylor theorem, we prove a new stabilization theorem for spreading models which produces a basic sequence all of whose normalized constant coefficient block basic sequences are good. When the resulting basic sequence is semi-normalized, all the spreading models generated by the above good sequences must be uniformly equivalent to lp or c0. Finally, we investigate the assumption that every normalized block tree on a Banach space has a good branch. This turns out to be a very strong assumption and is equivalent to the space being 1-asymptotic lp. We also show that the stronger assumption that every block basic sequence is good is equivalent to the space being stabilized 1-asymptotic lp.

Diese Arbeit beschäftigt sich mit der Speziestheorie aus Mochizukis Beweis(versuch) der abc-Vermutung. Es wird ein Standpunkt eingeführt, der Parallelen zwischen der Kategorientheorie und der Speziestheorie aufzeigt und es werden so die Besonderheiten der Speziestheorie herausgearbeitet. In der Speziestheorie möchte man Konstruktionen ausführen, welche von keinen Auswahlen abhängen. Dieses Problem wird in einem allgemeinen Kontext für universelle Morphismen gelöst. An Beispielen wird die in der Arbeit behandelte Theorie erklärt.

In the first chapter, we define Steinhaus set as a set that meets every isometric copy of another set at exactly one point. We show that there is no Steinhaus set for any four-point subset in a plane.In the second chapter, we define the orbit tree of a permutation group of natural numbers, and further introduce compressed orbit trees. We show that any rooted finite tree can be realized as a compressed orbit tree of some permutation group. In the third chapter, we investigate certain classes of closed permutation groups of natural numbers with respect to their universal and surjectively universal groups. We characterize two-sided invariant groups, and prove that there is no universal group for countable groups, nor universal group for two-sided invariant groups in permutation groups of natural numbers.

I study sets of attractors and non-attractors of finite iterated function systems. I provide examples of compact sets which are attractors of iterated function systems as well as compact sets which are not attractors of any iterated function system. I show that the set of all attractors is a dense Fs set and the space of all non-attractors is a dense Gd set it the space of all non-empty compact subsets of a space X. I also investigate the small trans-finite inductive dimension of the space of all attractors of iterated function systems generated by similarity maps on [0,1].

Thesis (M.S.)--Massachusetts Institute of Technology, Dept. of Civil Engineering, 1980. / MICROFICHE COPY AVAILABLE IN ARCHIVES AND ENGINEERING. / Bibliography: leaves 100-102. / by Steven B. Pitschke. / M.S.