Sökning: "homotopy type theory"

Visar resultat 1 - 5 av 18 avhandlingar innehållade orden homotopy type theory.

1. 1. Univalent Types, Sets and Multisets : Investigations in dependent type theory

   Författare :Håkon Robbestad Gylterud; Erik Palmgren; Nicola Gambino; Stockholms universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; type theory; homotopy type theory; dependent types; constructive set theory; databases; formalisation; agda; Mathematics; matematik;

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

3. 2. Homotopy Theory and TDA with a View Towards Category Theory

   Författare :Sebastian Öberg; Wojciech Chachólski; David Blanc; KTH; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Homotopy theory; Topological Data Analysis; Category theory; Mapping spaces; Homotopy commutative diagrams; Matematik; Mathematics;

   Sammanfattning : This thesis contains three papers. Paper A and Paper B deal with homotopy theory and Paper C deals with Topological Data Analysis. All three papers are written from a categorical point of view.In Paper A we construct categories of short hammocks and show that their weak homotopy type is that of mapping spaces. LÄS MER

4. 3. Cubical Intepretations of Type Theory

   Författare :Simon Huber; Göteborgs universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Dependent Type Theory; Univalence Axiom; Models of Type Theory; Identity Types; Cubical Sets;

   Sammanfattning : The interpretation of types in intensional Martin-Löf type theory as spaces and their equalities as paths leads to a surprising new view on the identity type: not only are higher-dimensional equalities explained as homotopies, this view also is compatible with Voevodsky's univalence axiom which explains equality for type-theoretic universes as homotopy equivalences, and formally allows to identify isomorphic structures, a principle often informally used despite its incompatibility with set theory. While this interpretation in homotopy theory as well as the univalence axiom can be justified using a model of type theory in Kan simplicial sets, this model can, however, not be used to explain univalence computationally due to its inherent use of classical logic. LÄS MER

5. 4. On Induction, Coinduction and Equality in Martin-Löf and Homotopy Type Theory

   Författare :Andrea Vezzosi; Chalmers tekniska högskola; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES; Conversion; Parametricity; Higher Inductive Types; Sized Types; Dependent Types; Type Theory; Guarded Types;

   Sammanfattning : Martin Löf Type Theory, having put computation at the center of logical reasoning, has been shown to be an effective foundation for proof assistants, with applications both in computer science and constructive mathematics. One ambition though is for MLTT to also double as a practical general purpose programming language. LÄS MER

7. 5. Exact completion and type-theoretic structures

   Författare :Jacopo Emmenegger; Erik Palmgren; Alexander Berglund; Maria Emilia Maietti; Stockholms universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; exact completion; type theory; setoid; weak limits; cartesian closure; inductive types; Mathematics; matematik;

   Sammanfattning : This thesis consists of four papers and is a contribution to the study of representations of extensional properties in intensional type theories using, mainly, the language and tools from category theory. Our main focus is on exact completions of categories with weak finite limits as a category-theoretic description of the setoid construction in Martin-Löf's intensional type theory. LÄS MER