Choice axioms and Postnikov completeness
Abstract
Building on work of Anel and Barton [M. Anel and R. Barton, 2024], we will introduce the construction of a hypercompletion modality [E. Rijke et al., 2020] in HoTT under the assumption that countable choice holds. Central results have been formalized in Cubical Agda and will be referenced where appropriate.
Fields of Study & Subjects
Advanced Algebra and Logic
Advanced Topology and Set Theory
Publication details
- Volume
- 10
- Issue
- 1
- Pages
- 22–39
- Publication date
- 19 June 2026
- Language
- EN