Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Kraus, Nicolai; Escardo, Martin; Coquand, Thierry; Altenkirch, Thorsten (2016)
Publisher: IfCoLog
Languages: English
Types: Article
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.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • [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 homotopytypetheory.org/2013/10/28.
    • [11] Nicolai Kraus. The general universal property of the propositional truncation. In Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau, editors, 20th International Conference on Types for Proofs and Programs (TYPES 2014), volume 39 of Leibniz International Proceedings in Informatics (LIPIcs), pages 111{145, Dagstuhl, Germany, 2015. Schloss Dagstuhl{Leibniz-Zentrum fuer Informatik. doi: 10.4230/LIPIcs.TYPES.2014.111.
    • [12] Nicolai Kraus. Truncation Levels in Homotopy Type Theory. PhD thesis, School of Computer Science, University of Nottingham, Nottingham, UK, 2015.
    • [13] Nicolai Kraus, Mart n Escardo, Thierry Coquand, and Thorsten Altenkirch. Generalizations of Hedberg's theorem. In Masahito Hasegawa, editor, Typed Lambda Calculus and Applications (TLCA), volume 7941 of Lecture Notes in Computer Science, pages 173{188. Springer-Verlag, 2013. doi: 10.1007/978-3-642-38946-7 14.
    • [14] Nicolai Kraus, Mart n Escardo, Thierry Coquand, and Thorsten Altenkirch. Notions of anonymous existence in Martin-Lof type theory (electronic appendix: Agda formalization), 2016.
    • [15] Per Martin-Lof. An intuitionistic theory of types: predicative part. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium '73, Proceedings of the Logic Colloquium, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73{118. North-Holland, 1975.
  • No related research data.
  • Discovered through pilot similarity algorithms. Send us your feedback.

Share - Bookmark

Funded by projects

Cite this article