Notions of anonymous existence in Martin-Löf type theory
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...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Published: |
IfCoLog
2016
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/38092/ |
| _version_ | 1848795595762827264 |
|---|---|
| author | Kraus, Nicolai Escardo, Martin Coquand, Thierry Altenkirch, Thorsten |
| author_facet | Kraus, Nicolai Escardo, Martin Coquand, Thierry Altenkirch, Thorsten |
| author_sort | Kraus, Nicolai |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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. |
| first_indexed | 2025-11-14T19:34:35Z |
| format | Article |
| id | nottingham-38092 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T19:34:35Z |
| publishDate | 2016 |
| publisher | IfCoLog |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-380922020-05-04T18:17:31Z https://eprints.nottingham.ac.uk/38092/ Notions of anonymous existence in Martin-Löf type theory Kraus, Nicolai Escardo, Martin Coquand, Thierry Altenkirch, Thorsten 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. IfCoLog 2016-10-11 Article PeerReviewed Kraus, Nicolai, Escardo, Martin, Coquand, Thierry and Altenkirch, Thorsten (2016) Notions of anonymous existence in Martin-Löf type theory. Logical Methods in Computer Science . ISSN 1860-5974 (In Press) homotopy type theory Hedberg’s theorem anonymous existence weakly constant functions factorization truncation squash types bracket types coherence conditions |
| spellingShingle | homotopy type theory Hedberg’s theorem anonymous existence weakly constant functions factorization truncation squash types bracket types coherence conditions Kraus, Nicolai Escardo, Martin Coquand, Thierry Altenkirch, Thorsten Notions of anonymous existence in Martin-Löf type theory |
| title | Notions of anonymous existence in Martin-Löf type theory |
| title_full | Notions of anonymous existence in Martin-Löf type theory |
| title_fullStr | Notions of anonymous existence in Martin-Löf type theory |
| title_full_unstemmed | Notions of anonymous existence in Martin-Löf type theory |
| title_short | Notions of anonymous existence in Martin-Löf type theory |
| title_sort | notions of anonymous existence in martin-löf type theory |
| topic | homotopy type theory Hedberg’s theorem anonymous existence weakly constant functions factorization truncation squash types bracket types coherence conditions |
| url | https://eprints.nottingham.ac.uk/38092/ |