A Model of Type Theory in Cubical Sets.
A Model of Type Theory in Cubical Sets.
We present a model of type theory with dependent product, sum, and identity, in cubical sets. We describe a universe and explain how to transform an equivalence between two types into an equality. We also explain how to model propositional truncation and the circle. While not expressed internally in type theory, the model is expressed in a constructive metalogic. Thus it is a step towards a computational interpretation of Voevodsky's Univalence Axiom.
- University of Bergen Norway
- Schloss Dagstuhl – Leibniz Center for Informatics Germany
- Leibniz Association Germany
:Matematikk og Naturvitenskap: 400::Matematikk: 410::Logikk: 416 [VDP], Univalent Foundations, models of dependent type theory, VDP::Matematikk og Naturvitenskap: 400::Matematikk: 410::Logikk: 416, univalent foundations, cubical sets, Models of dependent type theory, 004
:Matematikk og Naturvitenskap: 400::Matematikk: 410::Logikk: 416 [VDP], Univalent Foundations, models of dependent type theory, VDP::Matematikk og Naturvitenskap: 400::Matematikk: 410::Logikk: 416, univalent foundations, cubical sets, Models of dependent type theory, 004
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).0 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!