Failure of Normalization in Impredicative Type Theory with
Proof-Irrelevant Propositional EqualityArticle
Authors: Andreas Abel ; Thierry Coquand
NULL##NULL
Andreas Abel;Thierry Coquand
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].