Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Types for Proofs and Programs

TYPES 1995: Types for Proofs and Programs pp 153–164Cite as

Conservativity of equality reflection over intensional type theory

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1158))

Abstract

We investigate the relationship between intensional and extensional formulations of Martin-Löf type theory. We exhibit two principles which are not provable in the intensional formulation: uniqueness of identity and functional extensionality. We show that extensional type theory is conservative over the intensional one extended by these two principles, meaning that the same types are inhabited, whenever they make sense. The proof is non-constructive because it uses set-theoretic quotienting and choice of representatives.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Thorsten Altenkirch, Veronica Gaspes, Bengt Nordström, and Björn von Sydow. A User's Guide to ALF. Chalmers University of Technology, Sweden, May 1994. Available on the WWW: file://ftp.cs.chalmers.se/pub/users/alti/alf.ps.Z.

    Google Scholar 

  2. Peter Dybjer. Internal type theory. In Proc. BRA TYPES workshop, Torino, June 1995, Springer LNCS, 1996. To appear.

    Google Scholar 

  3. Solomon Feferman. Theories of finite type. In Jon Barwise, editor, Handbook of Mathematical Logic, chapter D.4. North-Holland, 1977.

    Google Scholar 

  4. Martin Hofmann. Syntax and sematnics of dependent types. In P. Dybjer and A. M. Pitts, editors, Semantics and Logics of Computation. Cambridge University Press, 199?

    Google Scholar 

  5. Martin Hofmann. Elimination of extensionality for Martin-Löf type theory. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs. Springer, 1994. LNCS 806.

    Google Scholar 

  6. Martin Hofmann. Extensional Concepts in Intensional Type Theory. PhD thesis, Univ. of Edinburgh, 1995.

    Google Scholar 

  7. Martin Hofmann and Thomas Streicher. A groupoid model refutes uniqueness of identity proofs. In Proceedings of the 9th Symposium on Logic in Computer Science (LICS), Paris, 1994.

    Google Scholar 

  8. Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis-Napoli, 1984.

    Google Scholar 

  9. B. Nordström, K. Petersson, and J. M. Smith. Programming in Martin-Löf 's Type Theory, An Introduction. Clarendon Press, Oxford, 1990.

    Google Scholar 

  10. Thomas Streicher. Semantical Investigations into Intensional Type Theory. Habilitationsschrift, LMU München, 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fachbereich Mathematik, TH Darmstadt, Schloßgartenstraße 7, D-64289, Darmstadt, Germany

    Martin Hofmann

Authors
  1. Martin Hofmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Stefano Berardi Mario Coppo

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hofmann, M. (1996). Conservativity of equality reflection over intensional type theory. In: Berardi, S., Coppo, M. (eds) Types for Proofs and Programs. TYPES 1995. Lecture Notes in Computer Science, vol 1158. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61780-9_68

Download citation

  • DOI: https://doi.org/10.1007/3-540-61780-9_68

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61780-8

  • Online ISBN: 978-3-540-70722-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation