Generalizations of Hedberg's theorem

Nicolai Kraus, Martín Escardó, Thierry Coquand, Thorsten Altenkirch

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationTyped Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings
Number of pages16
Publication statusPublished - 2013
Event11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013 - Eindhoven, Netherlands
Duration: 26 Jun 201328 Jun 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7941 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013


  • anonymous existence
  • bracket types
  • constant endofunctions
  • Hedberg's Theorem
  • homotopy type theory
  • propositional equality
  • squash types
  • truncation

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Generalizations of Hedberg's theorem'. Together they form a unique fingerprint.

Cite this