Construction of the Circle in UniMath
Autor: | Bezem, Marc, Buchholtz, Ulrik, Grayson, Daniel R., Shulman, Michael |
---|---|
Rok vydání: | 2019 |
Předmět: | |
Druh dokumentu: | Working Paper |
Popis: | 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. Comment: 27 pages; many improvements thanks to referee comments; added Shulman as co-author, who helped write a new section on the interpretation in higher toposes |
Databáze: | arXiv |
Externí odkaz: |