Blar i Department of Informatics på forfatter "Shulman, Michael"
-
Construction of the circle in UniMath
Bezem, Marc; Buchholtz, Ulrik; Grayson, Daniel R.; Shulman, Michael (Journal article; Peer reviewed, 2021)We 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 ...