×

Construction of the circle in UniMath. (English) Zbl 07357172

Summary: We show that the type \(\mathrm{T}\mathbb{Z}\) of \(\mathbb{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 stand-alone construction of the circle not using higher inductive types.

MSC:

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

Software:

UniMath
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Brunerie, Guillaume; de Boer, Menno; Lumsdaine, Peter LeFanu; Mortberg, Anders, Initiality for Martin-Löf type theory (2020), A formalization in Agda of the proof
[2] Brunerie, Guillaume; de Boer, Menno; Lumsdaine, Peter LeFanu; Mortberg, Anders, Initiality for Martin-Löf type theory, Talk at HoTTEST Seminar, Sept. 10, 2020
[3] Hou, Kuen-Bang (Favonia), Implementation of higher inductive types in HoTT-Agda · Zbl 1452.55016
[4] Kapulkin, Chris; Lumsdaine, Peter LeFanu, The simplicial model of univalent foundations (after Voevodsky), J. Eur. Math. Soc. (2012), in press · Zbl 1452.03038
[5] Lumsdaine, Peter LeFanu; Shulman, Michael, Semantics of higher inductive types, Math. Proc. Camb. Philos. Soc., 169, 1, 159-208 (2020) · Zbl 1470.18007
[6] Lurie, Jacob, Higher Topos Theory, Annals of Mathematics Studies, vol. 170 (2009), Princeton University Press · Zbl 1175.18001
[7] Shulman, Michael, All \(( \infty, 1)\)-toposes have strict univalent universes (2019)
[8] Shulman, Michael, Proof sketch of circle induction
[9] Shulman, Michael, The univalence axiom for elegant Reedy presheaves, Homology, Homotopy, and Applications, 17, 2, 81-106 (2015) · Zbl 1352.55010
[10] Sojakova, Kristina, Higher Inductive Types as Homotopy-Initial Algebras, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL ’15, 31-42 (2015), Association for Computing Machinery: Association for Computing Machinery Mumbai, India · Zbl 1345.03017
[11] The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics (2013), Institute for Advanced Study · Zbl 1298.03002
[12] Voevodsky, Vladimir, A C-system defined by a universe category, Theory Appl. Categ., 30, 37, 1181-1215 (2015) · Zbl 1436.03311
[13] Voevodsky, Vladimir, C-system of a module over a Jf-relative monad · Zbl 1507.18009
[14] Voevodsky, Vladimir, C-systems defined by universe categories: presheaves, Theory Appl. Categ., 32, 3, 53-112 (2017) · Zbl 1453.03067
[15] Voevodsky, Vladimir, HoTT is not an interpretation of MLTT into abstract homotopy theory (2015)
[16] Voevodsky, Vladimir, Martin-Löf identity types in the C-systems defined by a universe category (2015) · Zbl 1436.03311
[17] Voevodsky, Vladimir, Products of families of types and (n, A)-structures on C-systems, Theory Appl. Categ., 31, 36, 1044-1094 (2016) · Zbl 1380.03072
[18] Voevodsky, Vladimir, Subsystems and regular quotients of C-systems, (A Panorama of Mathematics: Pure and Applied; Conference on Mathematics and Its Applications. A Panorama of Mathematics: Pure and Applied; Conference on Mathematics and Its Applications, Kuwait City, 2014. A Panorama of Mathematics: Pure and Applied; Conference on Mathematics and Its Applications. A Panorama of Mathematics: Pure and Applied; Conference on Mathematics and Its Applications, Kuwait City, 2014, Contemp. Math., vol. 658 (2016), Amer. Math. Soc.: Amer. Math. Soc. Providence, RI), 127-137 · Zbl 1452.03040
[19] Voevodsky, Vladimir, The (n, A)-structures on the C-systems defined by universe categories, Theory Appl. Categ., 32, 4, 113-121 (2017) · Zbl 1383.03056
[20] Voevodsky, Vladimir, Unimath - its present and its future, A talk, with slides and video available at
[21] Voevodsky, Vladimir; Ahrens, Benedikt; Grayson, Daniel, UniMath — a computer-checked library of univalent mathematics
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.