Sökning: "Peter LeFanu Lumsdaine"

Hittade 3 avhandlingar innehållade orden Peter LeFanu Lumsdaine.

  1. 1. A Proof and Formalization of the Initiality Conjecture of Dependent Type Theory

    Författare :Menno de Boer; Peter LeFanu Lumsdaine; Alexander Berglund; Bas Spitters; Stockholms universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Dependent type theory; Category theory; Contextual categories; Initiality; Formalization; Mathematics; matematik; matematisk logik; Mathematical Logic;

    Sammanfattning : 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. LÄS MER

  3. 2. Localic Categories of Models and Categorical Aspects of Intuitionistic Ramified Type Theory

    Författare :Johan Lindberg; Erik Palmgren; Peter LeFanu Lumsdaine; Henrik Forssell; Benno van den Berg; Stockholms universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Topos theory; predicative topos theory; ramified type theory; type theory; localic groupoids; Mathematics; matematik;

    Sammanfattning : This thesis contains three papers, all in the general area of categorical logic, together with an introductory part with some minor results and proofs of known results which does not appear to be (easily) available in the literature.In Papers I and II we investigate the formal system Intuitionistic Ramified Type Theory (IRTT), introduced by Erik Palmgren, as an approach to predicative topos theory. LÄS MER

  4. 3. Representation theorems for abelian and model categories

    Författare :Anna Giulia Montaruli; Peter LeFanu Lumsdaine; Gregory Arone; Marek Zawadowski; Stockholms universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Category Theory; Logic; Algebra; Homotopy Theory; matematik; Mathematics;

    Sammanfattning : In this PhD thesis we investigate a representation theorem for small abelian categories and a representation theorem for left proper, enriched model categories, with the purpose of describing them concretely in terms of specific well-known categories.For the abelian case, we study the constructivity issues of the Freyd-Mitchell Embedding Theorem, which states the existence of a full embedding from a small abelian category into the category of modules over an appropriate ring. LÄS MER