Avancerad sökning

Hittade 2 avhandlingar som matchar ovanstående sökkriterier.

1. 1. A Model of Type Theory in Cubical Sets

   Författare :Simon Huber; Göteborgs universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES; Models of dependent type theory; cubical sets; Univalent Foundations;

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

3. 2. Formalizing Univalent Set-Level Structures in Cubical Agda

   Författare :Max Zeuner; Anders Mörtberg; Martin Escardo; Stockholms universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES;

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