In this licentiate thesis we present a proof of the initiality conjecture for Martin-Löf’s type theory with 0, 1, N, A+B, ∏AB, ∑AB, IdA(u,v), countable hierarchy of universes (Ui)iєN closed under these type constructors and with type of elements (ELi(a))iєN. We employ the categorical semantics of contextual categories. The proof is based on a formalization in the proof assistant Agda done by Guillaume Brunerie and the author. This work was part of a joint project with Peter LeFanu Lumsdaine and Anders Mörtberg, who are developing a separate formalization of this conjecture with respect to categories with attributes and using the proof assistant Coq over the UniMath library instead. Results from this project are planned to be published in the future. We start by carefully setting up the syntax and rules for the dependent type theory in question followed by an introduction to contextual categories. We then define the partial interpretation of raw syntax into a contextual category and we prove that this interpretation is total on well-formed input. By doing so, we define a functor from the term model, which is built out of the syntax, into any contextual category and we show that any two such functors are equal. This establishes that the term model is initial among contextual categories. At the end we discuss details of the formalization and future directions for research. In particular, we discuss a memory issue that arose in type checking the formalization and how it was resolved. / <p>Licentiate defense over Zoom.</p>

We construct a category of short hammocks and show that it has the weak homotopy type of mapping spaces. In doing so we tackle the problem of applying the nerve to large categories without the use of multiple universes. We also explore what the mapping space is. The main tool in showing the connection between hammocks and mapping spaces will be the use of homotopy groupoids, homotopy groupoid actions and the homotopy fiber of their corresponding bar constructions. / <p>QC 20141208</p>

No description available.

Les questions <EM>"Qu'est-ce qu'une preuve?"</EM> et <EM>"Quand deux preuves sont-elles identiques?"</EM> sont fondamentales pour la théorie de la preuve. Mais pour la logique classique propositionnelle --- la logique la plus répandue --- nous n'avons pas encore de réponse satisfaisante. C'est embarrassant non seulement pour la théorie de la preuve, mais aussi pour l'informatique, où la logique classique joue un rôle majeur dans le raisonnement automatique et dans la programmation logique. De même, l'architecture des processeurs est fondée sur la logique classique. Tous les domaines dans lesquels la recherche de preuve est employée peuvent bénéficier d'une meilleure compréhension de la notion de preuve en logique classique, et le célèbre problème NP-vs-coNP peut être réduit à la question de savoir s'il existe une preuve courte (c'est-à-dire, de taille polynomiale) pour chaque tautologie booléenne. Normalement, les preuves sont étudiées comme des objets syntaxiques au sein de systèmes déductifs (par exemple, les tableaux, le calcul des séquents, la résolution, ...). Ici, nous prenons le point de vue que ces objets syntaxiques (également connus sous le nom d'arbres de preuve) doivent être considérés comme des représentations concrètes des objets abstraits que sont les preuves, et qu'un tel objet abstrait peut être représenté par un arbre en résolution ou dans le calcul des séquents. Le thème principal de ce travail est d'améliorer notre compréhension des objets abstraits que sont les preuves, et cela se fera sous trois angles différents, étudiés dans les trois parties de ce mémoire: l'algèbre abstraite (chapitre 2), la combinatoire (chapitres 3 et 4), et la complexité (chapitre 5).

We define and study the fundamental pro-finite 2-groupoid of varieties X defined over a field k. This is a higher algebraic invariant of a scheme X, analogous to the higher fundamental path 2-groupoids as defined for topological spaces. This invariant is related to previously defined invariants, for example the absolute Galois group of a field, and Grothendieck’s étale fundamental group. The special case of Brauer-Severi varieties is considered, in which case a “sections conjecture” type theorem is proved. It is shown that a Brauer-Severi variety X has a rational point if and only if its étale fundamental 2-groupoid has a special sort of section.

This thesis is about the problem of compositionality in distributional semantics. Distributional semantics presupposes that the meanings of words are a function of their occurrences in textual contexts. It models words as distributions over these contexts and represents them as vectors in high dimensional spaces. The problem of compositionality for such models concerns itself with how to produce distributional representations for larger units of text (such as a verb and its arguments) by composing the distributional representations of smaller units of text (such as individual words). This thesis focuses on a particular approach to this compositionality problem, namely using the categorical framework developed by Coecke, Sadrzadeh, and Clark, which combines syntactic analysis formalisms with distributional semantic representations of meaning to produce syntactically motivated composition operations. This thesis shows how this approach can be theoretically extended and practically implemented to produce concrete compositional distributional models of natural language semantics. It furthermore demonstrates that such models can perform on par with, or better than, other competing approaches in the field of natural language processing. There are three principal contributions to computational linguistics in this thesis. The first is to extend the DisCoCat framework on the syntactic front and semantic front, incorporating a number of syntactic analysis formalisms and providing learning procedures allowing for the generation of concrete compositional distributional models. The second contribution is to evaluate the models developed from the procedures presented here, showing that they outperform other compositional distributional models present in the literature. The third contribution is to show how using category theory to solve linguistic problems forms a sound basis for research, illustrated by examples of work on this topic, that also suggest directions for future research.

Dans cette thèse, nous présentons les relations entre le principe de réflexion MRP introduit par Moore, les propriétés d'arbres généralisées ITP et ISP introduites par Weiß, ainsi que les propriétés square introduites par Jensen et développées par Schimmerling. Le résultat principal de cette thèse est que MRP+MA entraine ITP(λ, ω2) pour tout cardinal λ ≥ ω2. Ce résultat implique par conséquent que les méthodes actuelles pour prouver la consistance de MRP+MA nécessitent au moins l'existence d'un cardinal supercompact. Il s'avère que MRP seul ne suffit pas à démontrer ce résultat, et nous donnons la démonstration que MRP n'entraine pas la propriété d'arbre plus faible, à savoir TP(ω2, ω2). De plus MRP+MA n'entraine pas le principe d'arbre plus fort ISP(ω2, ω2). Enfin nous étudions les relations entre MRP et des versions faibles de square. Nous montrons que MRP implique la négation de square(λ, ω) et MRP+MA implique la négation de square(λ, ω1) pour tout λ ≥ ω2.

By extending Husserl’s own historico-critical study to include the conceptual mathematics of more contemporary times – specifically category theory and its emphatic development since the second half of the 20th century – this paper claims that the delineation between mathematics and philosophy must be completely revisited. It will be contended that Husserl’s phenomenological work was very much influenced by the discoveries and limitations of the formal mathematics being developed at Göttingen during his tenure there and that, subsequently, the rôle he envisaged for his material a priori science is heavily dependent upon his conception of the definite manifold. Motivating these contentions is the idea of a mathematics which would go beyond the constraints of formal ontology and subsequently achieve coherence with the full sense of transcendental phenomenology. While this final point will be by no means proven within the confines of this paper it is hoped that the very fact of opening up for the possibility of such an idea will act as a supporting argument to the overriding thesis that the relationship between mathematics and phenomenology must be problematised.

Submitted by Eunice Novais (enovais@uepg.br) on 2018-09-03T20:15:34Z No. of bitstreams: 2 license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5) Pedro J Miranda.pdf: 2542145 bytes, checksum: bb9638f5d6706faee0cb0ad113f1d1de (MD5) / Made available in DSpace on 2018-09-03T20:15:34Z (GMT). No. of bitstreams: 2 license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5) Pedro J Miranda.pdf: 2542145 bytes, checksum: bb9638f5d6706faee0cb0ad113f1d1de (MD5) Previous issue date: 2018-08-02 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / Esta tese tem por principal objetivo formalizar e modelar a emergência e a Lei de Proporcionalidade Intrínseca (LPI). Ambos os conceitos são trabalhados e precisados metafisicamente e, então, matematizados. Tal formalização matemática é realizada por meio da Teoria de Categorias utilizando constructos, functores underlying e a categoria dos conjuntos. A Lei de Proporcionalidade Intrínseca é o conjunto das operações internas e suas propriedades que estão nos objetos de um constructo que compõe uma emergência. A aplicação direta desse resultado ocorre em sistemas biológicos concebidos como todos substanciais vivos. A decomposição de um sistema biológico de diversos modos suscita uma aplicação deste modelo: como é possível que diferentes decomposições de um mesmo sistema gerem categorias com propriedades tão diferentes? Esse fenômeno é modelado e explicado pela aplicação direta da emergência e da LPI. Essa aplicação é mediada por meio de Biologia Relacional concebida pelo biólogo matemático Robert Rosen. Além disso, construímos neste trabalho uma Teoria de Nocautes e a aplicamos em um estudo de caso ecológico. / This thesis has as main aim the formalization and the modeling of the emergence and of the Intrinsic Proportionality Law (IPL). Both concepts are initially worked and metaphysically specified for then, in a second moment, be turned into a mathematical concept. Such mathematical formalization is made by means of Category Theory, utilizing constructs, underlying functors and the category of sets. The Intrinsic Proportionality Law is a set of operations and its properties that are within objects of a construct that composes an emergence. The direct application of this result is made on biological systems conceived as living substantial wholes. The decomposition of such a system, by several ways, evokes an application: how is it possible that different decompositions of the same system generate categories with different properties? This phenomenon is modeled and explained by the direct application of emergence and IPL. Such application is mediated by means of Relational Biology, which was conceived by the mathematical biologist Robert Rosen. Additionally, we also built in this work a Knockout Theory and applied it in an ecological study case.

This thesis is devoted to the study of higher representation theory as introduced in [Rou4]. As this theory is in its early days, it is essential to seek out modules that can rightfully be named building blocks and allow one to express as much of the structure of arbitrary modules as possible in their terms. We contribute towards this undertaking in the case of additive higher representation theory. Inspiration is drawn from Soergel bimodules which categorify the Hecke algebra. We introduce functorially cyclic modules as well as (strongly) universal cell modules. Examples include the minimal categorifications of [Rou4]. Properties of such modules are discussed and universal properties in terms of representable 2-functors are established. This leads to constructions and classifications in terms of split Frobenius objects, using a new variant of the Barr-Beck theorem for additive categories. Furthermore, we encounter a new class of modules so called coinvariant modules which arise from automorphism group actions. We also construct canonical cofiltrations and demonstrate why the Jordan-Hölder theory of [Rou4] does not readily generalise. Throughout, we comment on the succession [MaMi1]-[MaMi5] that tackles the same questions, however arrives at different conclusions. As applications, we first show that the 2-category of singular Soergel bimodules of [Wi2] arises naturally within the additive higher representation theory of Soergel bimodules. Second, we establish (weak) equivalences between certain associated universal cell modules together with a categorification of cell module homomorphisms of the Hecke algebra. Third, we show that singular Soergel bimodules constructed with a faithful representation categorify the Schur algebroid, generalising the main result of [Li]. Fourth given a group and a subgroup, we recover the additive monoidal category of representations of the subgroup from the corresponding category for the group without invoking Tannakian formalism.