Construction of the Circle in UniMath

DOI10.1016/J.JPAA.2021.106687MaRDI QIDQ6326548arXivFDO

Authors Marc Bezem, Ulrik Buchholtz, Daniel R. Grayson, Michael Shulman

Publication date 4 October 2019

Mathematics Subject Classification ID

Logic in computer science (03B70) Categorical logic, topoi (03G30) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38)

Abstract: We show that the type $mathrmTmathbbZ$ of $mathbbZ$-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 stand-alone construction of the circle not using higher inductive types.

This page was built for publication: Construction of the Circle in UniMath

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6326548)