@inproceedings { , title = {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.}, conference = { TLCA: International Conference on Typed Lambda Calculi and Applications}, doi = {10.1007/978-3-642-38946-7\_14}, isbn = {9783642389450}, pages = {173-188}, publicationstatus = {Published}, url = {https://nottingham-repository.worktribe.com/output/4769460}, year = {2024}, author = {Kraus, Nicolai and Escardó, Martín and Coquand, Thierry and Altenkirch, Thorsten} }