Generalizations of Hedberg’s Theorem

Abstract

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 to consider constant endofunctions. For such a function, we can look at the type of its fixed points. We show that this type has at most one element, which is a nontrivial lemma in the absence of UIP. As an application, a new notion of anonymous existence can be defined. One further main result is that, if every type has a constant endofunction, then all equalities are decidable. All the proofs have been formalized in Agda.

Citation

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

• Conference Name: TLCA: International Conference on Typed Lambda Calculi and Applications
• Start Date: Jun 26, 2013
• End Date: Jun 28, 2013
• Publication Date: 2013
• Deposit Date: Jul 15, 2020
• Pages: 173-188
• Series Title: Lecture Notes in Computer Science
• Series Number: 7941
• Book Title: Typed Lambda Calculi and Applications: 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June
• ISBN: 9783642389450
• DOI: https://doi.org/10.1007/978-3-642-38946-7_14
• Public URL: https://nottingham-repository.worktribe.com/output/4769460
• Publisher URL: https://link.springer.com/chapter/10.1007%2F978-3-642-38946-7_14