Sökning: "cubical sets"

Hittade 2 avhandlingar innehållade orden cubical sets.

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

    Författare :Simon Huber; Göteborgs universitet; Göteborgs universitet; Gothenburg University; []
    Nyckelord :NATURVETENSKAP; NATURVETENSKAP; NATURAL SCIENCES; 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

  2. 2. Cubical Intepretations of Type Theory

    Författare :Simon Huber; Göteborgs universitet; Göteborgs universitet; Gothenburg University; []
    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