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

Article English OPEN
Kraus, Nicolai ; Escardo, Martin ; Coquand, Thierry ; Altenkirch, Thorsten
  • Publisher: IfCoLog

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.
  • References (15)
    15 references, page 1 of 2

    [1] Steve Awodey and Andrej Bauer. Propositions as [types]. Journal of Logic and Computation, 14(4):447{ 471, 2004. doi: 10.1093/logcom/14.4.447.

    [2] Steve Awodey and Michael Warren. Homotopy theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society, 146:45{55, 2009. doi: 10.1017/S0305004108001783.

    [3] Robert Lee Constable. Constructive mathematics as a programming logic I: Some principles of theory. In Annals of Mathematics, volume 24, pages 21{37. Elsevier Science Publishers, B.V. (North-Holland), 1985. Reprinted from Topics in the Theory of Computation, Selected Papers of the International Conference on Foundations of Computation Theory, FCT '83.

    [4] Radu Diaconescu. Axiom of choice and complementation. Proc. Amer. Math. Soc., 51:176{178, 1975. doi: 10.1090/S0002-9939-1975-0373893-X.

    [5] Michael P. Fourman and Andre Scedrov. The \world's simplest axiom of choice" fails. Manuscripta Math., 38(3):325{332, 1982. doi: 10.1007/BF01170929.

    [6] Michael Hedberg. A coherence theorem for Martin-Lof's type theory. Journal of Functional Programming, 8(4):413{436, 1998. doi: 10.1017/S0956796898003153.

    [7] Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. In Venice Festschrift, pages 83{111. Oxford University Press, 1996.

    [8] William A. Howard. The formulas-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pages 479{ 490. Academic Press, 1980.

    [9] Nicolai Kraus. A direct proof of Hedberg's theorem, March 2012. Blog post at homotopytypetheory. org/2012/03/30.

    [10] Nicolai Kraus. The truncation map j j : N ! kN k is nearly invertible, October 2013. Blog post at

  • Similar Research Results (1)
  • Metrics
    No metrics available
Share - Bookmark