Notions of Anonymous Existence in Martin-Löf Type Theory

Research output: Contribution to journalArticle

Standard

Notions of Anonymous Existence in Martin-Löf Type Theory. / Kraus, Nicolai ; Escardo, Martin; Coquand, Thierry; Altenkirch, Thorsten.

In: Logical Methods in Computer Science, Vol. 13, No. 1, 24.03.2017, p. 1-36.

Research output: Contribution to journalArticle

Harvard

APA

Vancouver

Author

Kraus, Nicolai ; Escardo, Martin ; Coquand, Thierry ; Altenkirch, Thorsten. / Notions of Anonymous Existence in Martin-Löf Type Theory. In: Logical Methods in Computer Science. 2017 ; Vol. 13, No. 1. pp. 1-36.

Bibtex

@article{f668eb4fad81423ab7b87fde44f680fc,
title = "Notions of Anonymous Existence in Martin-L{\"o}f Type Theory",
abstract = "As the groupoid model of Hofmann and Streicher proves, identity proofs inintensional Martin-L{\"o}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.",
keywords = "weakly constant functions, coherence conditions, homotopy type theory, Hedberg{\textquoteright}s theorem, anonymous existence, bracket types, squash types, truncation, factorization",
author = "Nicolai Kraus and Martin Escardo and Thierry Coquand and Thorsten Altenkirch",
year = "2017",
month = mar
day = "24",
doi = "10.23638/LMCS-13(1:15)2017",
language = "English",
volume = "13",
pages = "1--36",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
publisher = "IfCoLog",
number = "1",

}

RIS

TY - JOUR

T1 - Notions of Anonymous Existence in Martin-Löf Type Theory

AU - Kraus, Nicolai

AU - Escardo, Martin

AU - Coquand, Thierry

AU - Altenkirch, Thorsten

PY - 2017/3/24

Y1 - 2017/3/24

N2 - As the groupoid model of Hofmann and Streicher proves, identity proofs inintensional 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.

AB - As the groupoid model of Hofmann and Streicher proves, identity proofs inintensional 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.

KW - weakly constant functions

KW - coherence conditions

KW - homotopy type theory

KW - Hedberg’s theorem

KW - anonymous existence

KW - bracket types

KW - squash types

KW - truncation

KW - factorization

U2 - 10.23638/LMCS-13(1:15)2017

DO - 10.23638/LMCS-13(1:15)2017

M3 - Article

VL - 13

SP - 1

EP - 36

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 1

ER -