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://g

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 https://git.app.uib.no/hott/hott-set-theory