Search for dissertations about: "Univalent Foundations"
Found 2 swedish dissertations containing the words Univalent Foundations.
-
1. A Model of Type Theory in Cubical Sets
Abstract : The intensional identity type is one if the most intricate concepts of dependent type theory. The recently discovered connection between homotopy theory and type theory gives a novel perspective on the identity type. READ MORE
-
2. Formalizing Univalent Set-Level Structures in Cubical Agda
Abstract : This licentiate thesis consists of two papers on formalization projects using Cubical Agda, a rather new extension of the Agda proof assistant with constructive support for univalence and higher inductive types. The common denominator of the two papers is that they are concerned with structures on types that are sets in the sense of Homotopy Type Theory or Univalent Foundations (HoTT/UF). READ MORE