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

Nicolai Kraus, Martin Escardo, Thierry Coquand, Thorsten Altenkirch

Research output: Contribution to journalArticlepeer-review

7 Citations (Scopus)
43 Downloads (Pure)

Abstract

As the groupoid model of Hofmann and Streicher proves, identity proofs in
intensional Martin-Löf 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.
Original languageEnglish
Article number15
Pages (from-to)1-36
Number of pages36
JournalLogical Methods in Computer Science
Volume13
Issue number1
DOIs
Publication statusPublished - 24 Mar 2017

Keywords

  • weakly constant functions
  • coherence conditions
  • homotopy type theory
  • Hedberg’s theorem
  • anonymous existence
  • bracket types
  • squash types
  • truncation
  • factorization

Fingerprint

Dive into the research topics of 'Notions of anonymous existence in Martin-Löf type theory'. Together they form a unique fingerprint.

Cite this