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].

@article{AbelC20,
  title = {Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality},
  author = {Andreas Abel and Thierry Coquand},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 16, Issue 2},
  year = {2020},
  doi = {10.23638/lmcs-16(2:14)2020}
}