Skip to main content

Research Repository

Advanced Search

All Outputs (1)

Generalizations of Hedberg’s Theorem (2013)
Conference Proceeding
Kraus, N., Escardó, M., Coquand, T., & Altenkirch, T. (2013). Generalizations of Hedberg’s Theorem. In Typed Lambda Calculi and Applications: 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June (173-188). https://doi.org/10.1007/978-3-642-38946-7_14

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.