Sökning: "Simon Huber"

Hittade 2 avhandlingar innehållade orden Simon Huber.

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. 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