I'm looking for references on constructive Lie algebra theory, e.g. the sort of theory you could develop in [Martin-Löf type theory][1] or internal to some topos with a NNO. Obviously excluded middle is not allowed in this setting, but I'm willing to accept countable choice (though no stronger choice axioms).

So far, I've found a PhD thesis on this topic from 1990:

*Merrin, S. D. (1990). Some constructive results in the theory of Lie algebras (Order No. 9029729). Available from ProQuest Dissertations & Theses Global. (303904437).*
 

  [1]: https://en.wikipedia.org/wiki/Intuitionistic_type_theory

I'd also be happy to get some references on Lie algebras from a more computational perspective (even if the author doesn't explicitly use constructive foundations).