Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality

Andreas Abel 0001, Thierry Coquand. Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality. Logical Methods in Computer Science, 16(2), 2020. [doi]

Abstract

Abstract is missing.