Generalizations of Hedberg’s Theorem
(2013)
Presentation / Conference Contribution
Kraus, N., Escardó, M., Coquand, T., & Altenkirch, T. (2013, June). Generalizations of Hedberg’s Theorem. Presented at TLCA: International Conference on Typed Lambda Calculi and Applications, Eindhoven, The Netherlands
As the groupoid interpretation by Hofmann and Streicher shows, uniqueness of identity proofs (UIP) is not provable. Generalizing a theorem by Hedberg, we give new characterizations of types that satisfy UIP. It turns out to be natural in this context... Read More about Generalizations of Hedberg’s Theorem.