Vis enkel innførsel

Construction of the circle in UniMath

dc.contributor.authorBezem, Marc
dc.contributor.authorBuchholtz, Ulrik
dc.contributor.authorGrayson, Daniel R.
dc.contributor.authorShulman, Michael
dc.date.accessioned2022-03-11T13:08:47Z
dc.date.available2022-03-11T13:08:47Z
dc.date.created2020-12-22T10:25:26Z
dc.date.issued2021
dc.identifier.issn0022-4049
dc.identifier.urihttps://hdl.handle.net/11250/2984689
dc.description.abstractWe 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.isoengen_US
dc.publisherElsevieren_US
dc.rightsNavngivelse 4.0 Internasjonal*
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/deed.no*
dc.titleConstruction of the circle in UniMathen_US
dc.typeJournal articleen_US
dc.typePeer revieweden_US
dc.description.versionpublishedVersionen_US
dc.rights.holderCopyright 2021 The Author(s)en_US
dc.source.articlenumber106687en_US
cristin.ispublishedtrue
cristin.fulltextoriginal
cristin.qualitycode1
dc.identifier.doi10.1016/j.jpaa.2021.106687
dc.identifier.cristin1862636
dc.source.journalJournal of Pure and Applied Algebraen_US
dc.relation.projectNorges forskningsråd: 240810en_US
dc.identifier.citationJournal of Pure and Applied Algebra. 2021, 225 (10), 106687.en_US
dc.source.volume225en_US
dc.source.issue10en_US


Tilhørende fil(er)

Thumbnail
Filnavn:
1-s2.0-S0022404921000232-main.pdf
Størrelse:
505.5Kb
Format:
PDF
Beskrivelse:
PDF
Åpne

Denne innførselen finnes i følgende samling(er)

Vis enkel innførsel

Navngivelse 4.0 Internasjonal
Med mindre annet er angitt, så er denne innførselen lisensiert som Navngivelse 4.0 Internasjonal