Showing cs.LOShow all
3 papers · 1 filter
cs.LO2026
Extension Types for Free
Nicolai Kraus
Extension types are a concept in dependent type theory that has appeared in various contexts. The idea is to have types whose terms are partially determined, e.g. via a strict boun…
cs.LO2026
Generalized Decidability via Brouwer Trees
Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh +1
In the setting of constructive mathematics, we suggest and study a framework for decidability of properties, which allows for finer distinctions than just "decidable, semidecidable…
cs.LO2024
On symmetries of spheres in univalent foundations
Pierre Cagne, Ulrik Buchholtz, Nicolai Kraus +1
Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form . The case of the circle has a slick answer: th…