Construction of the circle in UniMath

dc.contributor.author	Bezem, Marc
dc.contributor.author	Buchholtz, Ulrik
dc.contributor.author	Grayson, Daniel R.
dc.contributor.author	Shulman, Michael
dc.date.accessioned	2022-03-11T13:08:47Z
dc.date.available	2022-03-11T13:08:47Z
dc.date.created	2020-12-22T10:25:26Z
dc.date.issued	2021
dc.identifier.issn	0022-4049
dc.identifier.uri	https://hdl.handle.net/11250/2984689
dc.description.abstract	We show that the type TZ of Z-torsors has the dependent universal property of the circle, which characterizes it up to a unique homotopy equivalence. The construction uses Voevodsky’s Univalence Axiom and propositional truncation, yielding a standalone construction of the circle not using higher inductive types.	en_US
dc.language.iso	eng	en_US
dc.publisher	Elsevier	en_US
dc.rights	Navngivelse 4.0 Internasjonal	*
dc.rights.uri	http://creativecommons.org/licenses/by/4.0/deed.no	*
dc.title	Construction of the circle in UniMath	en_US
dc.type	Journal article	en_US
dc.type	Peer reviewed	en_US
dc.description.version	publishedVersion	en_US
dc.rights.holder	Copyright 2021 The Author(s)	en_US
dc.source.articlenumber	106687	en_US
cristin.ispublished	true
cristin.fulltext	original
cristin.qualitycode	1
dc.identifier.doi	10.1016/j.jpaa.2021.106687
dc.identifier.cristin	1862636
dc.source.journal	Journal of Pure and Applied Algebra	en_US
dc.relation.project	Norges forskningsråd: 240810	en_US
dc.identifier.citation	Journal of Pure and Applied Algebra. 2021, 225 (10), 106687.	en_US
dc.source.volume	225	en_US
dc.source.issue	10	en_US

Except where otherwise noted, this item's license is described as Navngivelse 4.0 Internasjonal