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 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.