3 ms·
Some constructivists may also take offense with proof irrelevance (and the resulting loss of normalization [1] or its incompatibility with HoTT), which you can
by foooobar 5y ago
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 https://arxiv.org/abs/1911.08174
- xvilka 5y agoThere is also a problem of HoTT and equality reflection incompatibility[1]. [1] https://www2.mathematik.tu-darmstadt.de/~streicher/barc_corr.pdf https://www2.mathematik.tu-darmstadt.de/~streicher/barc_corr...