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 -