Nicolai Kraus ; Martín Escardó ; Thierry Coquand ; Thorsten Altenkirch - Notions of Anonymous Existence in Martin-Löf Type Theory

lmcs:3217 - Logical Methods in Computer Science, March 24, 2017, Volume 13, Issue 1 - https://doi.org/10.23638/LMCS-13(1:15)2017
Notions of Anonymous Existence in Martin-Löf Type TheoryArticle

Authors: Nicolai Kraus ; Martín Escardó ; Thierry Coquand ; Thorsten Altenkirch

    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.


    Volume: Volume 13, Issue 1
    Published on: March 24, 2017
    Accepted on: March 24, 2017
    Submitted on: March 24, 2017
    Keywords: Computer Science - Logic in Computer Science,03B15,F.4.1
    Funding:
      Source : OpenAIRE Graph
    • Homotopy Type Theory: Programming and Verification; Funder: UK Research and Innovation; Code: EP/M016994/1
    • Theory And Applications of Induction Recursion; Funder: UK Research and Innovation; Code: EP/G03298X/1
    • Formalization of Constructive Mathematics; Funder: European Commission; Code: 247219

    Classifications

    Publications

    Has review
    • 1 zbMATH Open

    3 Documents citing this article

    Consultation statistics

    This page has been seen 3175 times.
    This article's PDF has been downloaded 839 times.