Cedille Cast #9: Impredicativity, proof-irrelevance, and normalization

This video explores a very recent result by Abel and Coquand concerning the combination of impredicativity and a strong form of proof irrelevance, and how this result relates to Cedille. Specifically, this combination of features, which exists both in Cedille and in the Lean proof assistant, results in a failure of strong normalization (though not of consistency) of the type theory.