Abstract We revisit the famous notion of sheaves through the lens of type theory and side-effects. Using the language of $$\textsf{MLTT}$$ MLTT , we show that they inductively approximate idealized functional objects as decision trees, realizing a generalized form of continuity. We materialize this intuition in $$\textsf{MLTT}^{\textsf{F}}$$ MLTT F , a case-study sheaf extension of $$\textsf{MLTT}$$ MLTT with a Cohen real and leverage it to show uniform continuity of all $$\textsf{MLTT}$$ MLTT functionals of type $$({\mathbb {N}}\rightarrow {\mathbb {B}}) \rightarrow {\mathbb {N}}$$ ( N → B ) → N . The latter results were mechanized in Rocq.

The axiom of choice (AC) states that every total relation contains a function. It enjoys a pivotal role in both classical and constructive dialects of mathematics. In the former, it is seen as a useful closure property invoked especially in set-theoretic contexts, in the latter it is seen either as a tautology, following from a constructive reading of totality proofs, or as a taboo, as by an extensional reading of totality proofs it enforces full classical logic. It has therefore been debated how much of AC should be accepted in constructive foundations and authors like Richman argued for "Constructive mathematics without choice" where even countable choice, not immediately jeopardising constructive reasoning, is avoided. With this paper, we propose a continuation of Richman’s programme of more radical extent and systematically study constructive foundations absent of countable, unique, or quantifier-free choice principles as well as the spurious fragments of (the actual) AC in form of extensionality principles: "Constructive mathematics without any choice" We argue that such a minimalistic setting is advantageous, for instance for studies in constructive reverse mathematics and synthetic computability theory. Apart from these programmatic considerations and a careful encyclopedia of choice principles, we revisit and refine several results from the literature: We show that already the partition principle (a consequence of AC of unknown strength) implies the excluded middle, that already logically decidable (inductive) equality of propositions implies proof irrelevance, and that function inversion principles such as the Cantor-Bernstein theorem not only rely on the excluded middle but also on unique choice. To the best of our knowledge, the latter is the first reverse mathematics result regarding the full axiom of unique choice, enabled by our minimal setting. Implementing such a minimalistic foundation, the proofs of all our results have been mechanised with the Rocq prover.

Continuity principles stating that all functions are continuous play a central role in some schools of constructive mathematics. However, there are different ways to formalise the property of being continuous in constructive foundations. We analyse these continuity properties from the perspective of constructive reverse mathematics. We work in constructive type theory, which can be seen as a minimal foundation for constructive reverse mathematics. We treat continuity of functions F : (Q → A) → R, i.e. with question type Q, answer type A, and result type R. Concretely, we discuss continuity defined via moduli, making the relevant list L : LQ of questions explicit, dialogue trees, making the question-answer process explicit as inductive tree, and tree functions, making the question-answer process explicit as function. We prove equivalences where possible and isolate necessary and sufficient axioms for equivalence proofs. Many of the results we discuss are already present in the works of Hancock, Pattinson, Ghani, Kawai, Fujiwara, Brede, Herbelin, Escardó, and others. Our main contribution is their formulation over a uniform foundation, the observation that no choice axioms are necessary, the generalisation to arbitrary types from natural numbers where possible, and a mechanisation in the Coq/Rocq proof assistant.