[foooobar]

Some constructivists may also take offense with proof irrelevance (and the resulting loss of normalization [1] or its incompatibility with HoTT), which you can only really avoid by avoiding Prop.

[1] https://arxiv.org/abs/1911.08174

[xvilka]

There is also a problem of HoTT and equality reflection incompatibility[1].

[1] https://www2.mathematik.tu-darmstadt.de/~streicher/barc_corr...