arXiv:1911.08174cs.LO
Normalization fails in type theory with an impredicative universe of propositions and a proof-irrelevant propositional equality. The counterexample to normalization is adapted from Girard's counterexample against normalization of System F equipped with a decider for type equality. It refutes Werner's normalization conjecture [LMCS 2008].
Linked by 3 identifiable commenters in 3 comments across 3 threads, from Jan 2020 to Jun 2026.
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
The normalization issue is not about quotients at all. It's https://arxiv.org/abs/1911.08174 "Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality"
Connected through shared HN threads, not inferred similarity or a recommendation.
A few notes, because this is obviously vibe coded, and does not work in many ways. 1. Yon's documentation mentions "Homotopy type theory:" > the runnable HoTT fragment is refl/pair/fst/snd These are basic features of martin-lof type theory, not homotopy type theory. The…
omegafixedpointView on HNParent context