onr:"swepub:oai:gup.ub.gu.se/282297"
Search: onr:"swepub:oai:gup.ub.gu.se/282297" > The Univalence Axio...
- 1 of 1
- Previous record
- Next record
- To hitlist
The Univalence Axiom in Cubical Sets
- Bezem, M. (author)
-
- Coquand, Thierry, 1961 (author)
- Gothenburg University,Göteborgs universitet,Institutionen för data- och informationsteknik (GU),Department of Computer Science and Engineering (GU)
-
- Huber, Simon, 1984 (author)
- Gothenburg University,Göteborgs universitet,Institutionen för data- och informationsteknik, datavetenskap, programmeringslogik (GU),Department of Computer Science and Engineering, Computing Science, Programming Logic
- (creator_code:org_t)
- 2018-06-26
- 2019
- English.
- In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 63:2, s. 159-171
- Journal article (peer-reviewed)
Abstract
Subject headings
Close
- 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.
Subject headings
- NATURVETENSKAP -- Data- och informationsvetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences (hsv//eng)
Keyword
- Dependent type theory
- Univalence axiom
- Cubical sets
- Computer Science
Publication and Content Type
- ref (subject category)
- art (subject category)
Find in a library
- Journal of Automated Reasoning (Search for host publication in LIBRIS)
To the university's database
- 1 of 1
- Previous record
- Next record
- To hitlist
Find more in SwePub
- By the author/editor
- Bezem, M.
- Coquand, Thierry ...
- Huber, Simon, 19 ...
- About the subject
-
- NATURAL SCIENCES
- NATURAL SCIENCES
- and Computer and Inf ...
- Articles in the publication
- Journal of Autom ...
- By the university
- University of Gothenburg
Search outside SwePub
- Extend your search to:
- Google Book Search
- Google Scholar
Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.
- Copyright © LIBRIS - National Library Systems
- LIBRIS.kb.se
