TY - GEN
T1 - Generalizations of Hedberg's theorem
AU - Kraus, Nicolai
AU - Escardó, Martín
AU - Coquand, Thierry
AU - Altenkirch, Thorsten
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
KW - anonymous existence
KW - bracket types
KW - constant endofunctions
KW - Hedberg's Theorem
KW - homotopy type theory
KW - propositional equality
KW - squash types
KW - truncation
UR - http://www.scopus.com/inward/record.url?scp=84884513264&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-38946-7_14
DO - 10.1007/978-3-642-38946-7_14
M3 - Conference contribution
AN - SCOPUS:84884513264
SN - 9783642389450
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 173
EP - 188
BT - Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings
T2 - 11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013
Y2 - 26 June 2013 through 28 June 2013
ER -