Treating the Riemann integral in a constructive setting is easy and straightforward. Treating the closely related but much more powerful [Henstock-Kurzweil integral](https://en.wikipedia.org/wiki/Henstock%E2%80%93Kurzweil_integral) constructively is *almost* easy, except for the dependence on Cousin's lemma where every proof seems to involve the excluded middle.


In a constructive (or slightly stronger intuitionistic) setting, is there a way to:


* define the HK integral
* prove that the HK integral is unique
* define another notion of integrability which constructively implies HK-integrability and is classically equivalent to Lebesgue integrability
* and prove that every derivative, even if discontinuous, is HK-integrable?


One approach would be restricting the choice of gauge to Baire functions, since under fairly general assumptions the gauge can be chosen to be Baire 2. This would require proving Cousin's lemma only for Baire functions, which looks more promising than proving the full Cousin’s lemma constructively.


I have seen a paper on [the reverse mathematics of Cousin’s lemma](https://arxiv.org/abs/2011.13060v1), but that is not in a constructive setting.



Is there a purely constructive presentation of the HK integral?
A few months later, I ended up proving it in constructive analysis with open induction and no countable choice. Since the open induction principle follows from Brouwer's bar theorem (it in turn implies the fan theorem so adding it as an axiom is necessary), it is available in the internal language of any sheaf topos over a locally countably compact topological space, including sheaves over any manifold with corners, which is good enough for every application I care about.


This is a proof from a draft of some notes I've been working on, with rudimentary use of Coq to check that the proof isn't completely wrong.


So let's state open induction:


An **open** subset $S$ of a closed real interval $[a,b]$ is said to be **inductive** if it satisfies that $[a,r) \subset S$ implies $[a,r] \subset S$. The **open induction principle** states that any inductive subset $S$ of $[a,b]$ must be the entire set.


Now to the theorem and proof.


(Cousin's theorem) For any gauge $\delta : [a,b] \to \mathbb{R}+$, there exists a $\delta$-fine tagged partition of $[a,b]$.


Proof:


Let $S$ be the set of points $r$ such that there exists a $\delta$-fine tagged partition on $[a,s]$ of length n for some $s \geq r$.
The set $S$ is clearly open, since it is downwards closed and any point in it is included in the open ray $ [a,b] \cap [a,t\_n + \delta(t\_n) ) \subset S$ for any associated partition.


Furthermore, it is inductive. For any $r$, suppose $[a,r) \subset S$. By that assumption (and using that either $r > a + \tfrac{2}{3}\delta(a)$ or $r \in [a, a + \delta(a)) \subset S$ to handle edge cases) we have a partition of length $n$ with $x\_n \geq r - \tfrac{1}{2} \mathrm{min}(\delta(a), \delta(r)) > a$.


Then, setting $\Delta\_n = t\_n + \delta(t\_n) - x\_n > 0$, then either $x\_n > b - \Delta\_n$ or $x\_n < b $. In the first case $b < t\_n + \delta(t\_n)$, so we can just replace $x\_n$ with $b$ and get a partition of $[a,b]$ that includes $r$. If $x\_n < b$, then we can make a partition of length $n+1$, since either we have $r < x\_n + \delta(x\_n)$ in which case we can set $t\_{n+1} = x\_n$ or we have $r > x\_n$ in which case we can set $t\_{n+1} = r$. In both cases, we can set $x\_{n+1} = \mathrm{min}(b, t\_{n+1} + \delta(t\_{n+1})) > x\_n$. So $[a,r] \subset S$ in all cases, and $S$ is inductive.


By open induction, $S = [a,b]$.


I'm planning to host the notes somewhere and add the proof to the wikipedia article on Cousin's lemma once I'm done with minor edits.


