Construction of the Circle in UniMath

DOI10.1016/J.JPAA.2021.106687arXiv1910.01856MaRDI QIDQ6326548FDOQ6326548

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

Publication date: 4 October 2019

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.

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)

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)