That final link is very insightful. Not to pick sides, but if Lean really doesn't have subject reduction when you use quotient types, that's a crazy property to drop (or lose accidentally).
I have a little experience of both Coq and Lean and have followed some of the discussion about Lean's handling of quotient types.
I have seen computer scientists emphasise to mathematicians that subject reduction should not be forfeit but I have yet to see a convincing argument/example for why not.
I don't suppose you can elaborate on why this may be / is so crazy, that someone with only a limited understanding of type theory might follow?
Setoids are also very relevant in constructive math, for similar reasons. Quotient types/sets basically conflate cases where one can easily normalize the elements of some equivalent class vs. cases where this cannot be done effectively, and that's not a good approach at all.
Lean's maths library development is essentially completely focussed on classical mathematics, which is why it has been so successful in drawing "working mathematicians" in. Such people do not care at all about the issues involving quotients, indeed quotients in Lean work just fine for them, and they don't care about constructibility either, because this is the prevailing culture in maths departments (although it is not, I am well aware, the prevailing culture in computer science departments). If you are interested in constructivism I would not recommend Lean. Many of the developments in mathlib are classical. That's why it's moving so quickly -- classical mathematics is much easier.
