Dr NICOLAI KRAUS NICOLAI.KRAUS@NOTTINGHAM.AC.UK
Professor of Theoretical Computer Science
Notions of anonymous existence in Martin-Löf type theory
Kraus, Nicolai; Escardo, Martin; Coquand, Thierry; Altenkirch, Thorsten
Authors
Martin Escardo
Thierry Coquand
THORSTEN ALTENKIRCH THORSTEN.ALTENKIRCH@NOTTINGHAM.AC.UK
Professor of Computer Science
Abstract
As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-L\"of type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do have unique identity proofs. A key ingredient in these constructions are weakly constant endofunctions on identity types. We study such endofunctions on arbitrary types and show that they always factor through a propositional type, the truncated or squashed domain. Such a factorization is impossible for weakly constant functions in general (a result by Shulman), but we present several non-trivial cases in which it can be done. Based on these results, we define a new notion of anonymous existence in type theory and compare different forms of existence carefully. In addition, we show possibly surprising consequences of the judgmental computation rule of the truncation, in particular in the context of homotopy type theory. All the results have been formalized and verified in the dependently typed programming language Agda.
Citation
Kraus, N., Escardo, M., Coquand, T., & Altenkirch, T. (in press). Notions of anonymous existence in Martin-Löf type theory. Logical Methods in Computer Science, 13(1),
Journal Article Type | Article |
---|---|
Acceptance Date | Mar 24, 2017 |
Online Publication Date | Mar 24, 2017 |
Deposit Date | Nov 1, 2016 |
Publicly Available Date | Mar 24, 2017 |
Journal | Logical Methods in Computer Science |
Print ISSN | 1860-5974 |
Electronic ISSN | 1860-5974 |
Publisher | Logical Methods in Computer Science |
Peer Reviewed | Peer Reviewed |
Volume | 13 |
Issue | 1 |
Keywords | homotopy type theory, Hedberg’s theorem, anonymous existence, weakly constant functions, factorization, truncation, squash types, bracket types, coherence conditions |
Public URL | https://nottingham-repository.worktribe.com/output/823981 |
Publisher URL | https://lmcs.episciences.org/3217 |
Related Public URLs | http://www.lmcs-online.org/index.php |
Additional Information | Publisher site says the following https://doi.org/10.23638/LMCS-13(1:15)2017 Source : oai:arXiv.org:1610.03346 Volume: Volume 13, Issue 1 Published on: March 24, 2017 Submitted on: March 24, 2017 Keywords: Computer Science - Logic in Computer Science,03B15,F.4.1 2020-09-21 NW |
Contract Date | Nov 1, 2016 |
Files
Notions of anonymous existence in martin-Löf type theory VoR
(525 Kb)
PDF
Copyright Statement
Copyright information regarding this work can be found at the following address: http://creativecommons.org/licenses/by/4.0
You might also like
Monads need not be endofunctors
(2015)
Journal Article
Normalisation by evaluation for dependent types
(2016)
Presentation / Conference Contribution
Normalisation by evaluation for type theory, in type theory
(2017)
Journal Article
Relative monads formalised
(2014)
Journal Article
When is a function a fold or an unfold?
(2001)
Presentation / Conference Contribution
Downloadable Citations
About Repository@Nottingham
Administrator e-mail: discovery-access-systems@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