Blar i Department of Informatics på tidsskrift "Journal of Pure and Applied Algebra"
Viser treff 1-1 av 1
-
Construction of the circle in UniMath
(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 ...