Dr NICOLAI KRAUS NICOLAI.KRAUS@NOTTINGHAM.AC.UK
Research Fellow
Generalizations of Hedberg’s Theorem
Kraus, Nicolai; Escard�, Mart�n; Coquand, Thierry; Altenkirch, Thorsten
Authors
Mart�n Escard�
Thierry Coquand
THORSTEN ALTENKIRCH THORSTEN.ALTENKIRCH@NOTTINGHAM.AC.UK
Professor of Computer Science
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.
Citation
Kraus, N., Escardó, M., Coquand, T., & Altenkirch, T. (2013). Generalizations of Hedberg’s Theorem. In Typed Lambda Calculi and Applications: 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June (173-188). https://doi.org/10.1007/978-3-642-38946-7_14
Conference Name | TLCA: International Conference on Typed Lambda Calculi and Applications |
---|---|
Start Date | Jun 26, 2013 |
End Date | Jun 28, 2013 |
Publication Date | 2013 |
Deposit Date | Jul 15, 2020 |
Pages | 173-188 |
Series Title | Lecture Notes in Computer Science |
Series Number | 7941 |
Book Title | Typed Lambda Calculi and Applications: 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June |
ISBN | 9783642389450 |
DOI | https://doi.org/10.1007/978-3-642-38946-7_14 |
Public URL | https://nottingham-repository.worktribe.com/output/4769460 |
Publisher URL | https://link.springer.com/chapter/10.1007%2F978-3-642-38946-7_14 |
You might also like
Type-theoretic approaches to ordinals
(2023)
Journal Article
A rewriting coherence theorem with applications in homotopy type theory
(2022)
Journal Article
Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory
(2020)
Conference Proceeding
Shallow Embedding of Type Theory is Morally Correct
(2019)
Journal Article
From Cubes to Twisted Cubes via Graph Morphisms in Type Theory
(2019)
Presentation / Conference
Downloadable Citations
About Repository@Nottingham
Administrator e-mail: digital-library-support@nottingham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search