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

翻译：常规化理论在类型理论中失败,存在不确定的主张世界和与证据无关的主张平等。对正常化的反例来自Girard对F系统正常化的反例,后者配备了一种类型的平等的决策者。它驳斥了Werner的正常化猜想[LMCS2008]。