Is there a purely constructive presentation of the HK integral? Treating the Riemann integral in a constructive setting is easy and straightforward. Treating the closely related but much more powerful Henstock-Kurzweil 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, but that is not in a constructive setting.
 A: Firstly, the following paper deals with the HK-integral and constructive math, see [2] below for details.
Taschner R., The swap of integral and limit in constructive mathematics.
Secondly, the general HK integral may be (too) difficult to salvage, as the associated versions of Cousin's lemma (even the restrictions you mention) seem fundamentally non-constructive.
Thirdly, the HK integral restricted to absolutely integrable functions is the Lebesgue integral (on suitable domains).  Hence, there should be a constructive treatment of this restriction.  In particular, in the case of bounded functions, one can replace the use of Cousin's lemma by Vitali's covering theorem (see Section 3.5 in [1]), where the latter is 'more constructive' than the former.  Also, since constructive measure theory exists, there is a 'constructive way around' Vitali's covering theorem, central as the latter is to Lebesgue measure theory (see again [1]).
References
[1] Dag Normann and Sam Sanders, the logical and computational properties of the Vitali covering theorem, arxiv: https://arxiv.org/abs/1902.02756
[2] Taschner R., The swap of integral and limit in constructive mathematics, Math. Log. Quart. 56, No. 5, 533 – 540 (2010) / DOI 10.1002/malq.200910107
A: 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.
