Skip to main content

Research Repository

Advanced Search

Notions of anonymous existence in Martin-Löf type theory

Kraus, Nicolai; Escardo, Martin; Coquand, Thierry; Altenkirch, Thorsten

Authors

Martin Escardo

Thierry Coquand



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.

Journal Article Type Article
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
APA6 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),
Keywords homotopy type theory, Hedberg’s theorem, anonymous existence, weakly constant functions, factorization, truncation, squash types, bracket types, coherence conditions
Publisher URL https://lmcs.episciences.org/3217
Related Public URLs http://www.lmcs-online.org/index.php
Copyright Statement Copyright information regarding this work can be found at the following address: http://creativecommons.org/licenses/by/4.0
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

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



Downloadable Citations

;