Till sidans topp

Sidansvarig: Webbredaktion
Sidan uppdaterades: 2012-09-11 15:12

Tipsa en vän
Utskriftsversion

The Univalence Axiom in C… - Göteborgs universitet Till startsida
Webbkarta
Till innehåll Läs mer om hur kakor används på gu.se

The Univalence Axiom in Cubical Sets

Artikel i vetenskaplig tidskrift
Författare M. Bezem
Thierry Coquand
Simon Huber
Publicerad i Journal of Automated Reasoning
Volym 63
Nummer/häfte 2
Sidor 159-171
ISSN 0168-7433
Publiceringsår 2019
Publicerad vid Institutionen för data- och informationsteknik, datavetenskap, programmeringslogik (GU)
Institutionen för data- och informationsteknik (GU)
Sidor 159-171
Språk en
Länkar dx.doi.org/10.1007/s10817-018-9472-...
Ämnesord Dependent type theory, Univalence axiom, Cubical sets, Computer Science
Ämneskategorier Data- och informationsvetenskap

Sammanfattning

In this note we show that Voevodsky's univalence axiom holds in the model of type theory based on cubical sets as described inBezem et al. (in: Matthes and Schubert (eds.) 19th international conference on types for proofs and programs (TYPES 2013), Leibniz international proceedings in informatics (LIPIcs), Schloss Dagstuhl-Leibniz-Zentrum fur Informatik, Dagstuhl, Germany, vol26, pp 107-128, 2014. 10.4230/LIPIcs.TYPES.2013.107. http://drops.dagstuhl.de/opus/volltexte/2014/4628) and Huber (A model of type theory in cubical sets. Licentiate thesis, University of Gothenburg, 2015). We will also discuss Swan's construction of the identity type in this variation of cubical sets. This proves that we have a model of type theory supporting dependent products, dependent sums, univalent universes, and identity types with the usual judgmental equality, and this model is formulated in a constructive metatheory.

Sidansvarig: Webbredaktion|Sidan uppdaterades: 2012-09-11
Dela:

På Göteborgs universitet använder vi kakor (cookies) för att webbplatsen ska fungera på ett bra sätt för dig. Genom att surfa vidare godkänner du att vi använder kakor.  Vad är kakor?