@nprofile1q... I'm mostly doing algebraic geometry, so well-founded trees and so on don't really appear in the mathematics I'm used to. I do like constructive mathematics (probably in something like IZF, although I like the ideas of type theory) and I'm always a bit appalled by those well-founded trees, because I associate them with something like Zorn's lemma, which IIRC proves their existence in classical set theory?

I'm always a bit surprised that many constructive-friendly type theorists don't seem to have an issue with W-types, is there a reason for this?