Comment by gylterud

I would suggest Bishop’s Constructive Analysis.

And a plug: I have a formalisation of models of constructive set theory in Homotopy Type Theory here: https://git.app.uib.no/hott/hott-set-theory