@inproceedings{10.1007/978-3-642-38946-7_14,
    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.},
    Address = {Berlin, Heidelberg},
    Author = {Kraus, Nicolai and Escard{\'o}, Mart{\'\i}n and Coquand, Thierry and Altenkirch, Thorsten},
    BookTitle = {Typed Lambda Calculi and Applications},
    Editor = {Hasegawa, Masahito},
    File = {Generalizations of Hedberg’s Theorem - hedberg - a - i.pdf},
    ISBN = {978-3-642-38946-7},
    Pages = {173--188},
    Publisher = {Springer Berlin Heidelberg},
    Title = {Generalizations of Hedberg's Theorem},
    Year = {2013},
    date-added = {2020-11-14 09:18:40 +0100},
    date-modified = {2020-11-14 09:18:40 +0100},
    doi = {10.1007/978-3-642-38946-7_14}
}

@inproceedings{10.1007/978-3-642-38946-7_14, 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.}, Address = {Berlin, Heidelberg}, Author = {Kraus, Nicolai and Escard{\'o}, Mart{\'\i}n and Coquand, Thierry and Altenkirch, Thorsten}, BookTitle = {Typed Lambda Calculi and Applications}, Editor = {Hasegawa, Masahito}, File = {Generalizations of Hedberg’s Theorem - hedberg - a - i.pdf}, ISBN = {978-3-642-38946-7}, Pages = {173--188}, Publisher = {Springer Berlin Heidelberg}, Title = {Generalizations of Hedberg's Theorem}, Year = {2013}, date-added = {2020-11-14 09:18:40 +0100}, date-modified = {2020-11-14 09:18:40 +0100}, doi = {10.1007/978-3-642-38946-7_14} }