Abstract
We give an interpretation of quotient types within in a dependent type theory with an impredicative universe of propositions (Calculus of Constructions). In the model, type dependency arises only at the propositional level, therefore universes and large eliminations cannot be interpreted. In exchange, the model is much simpler and more intuitive than the one proposed by the author in [10]. Moreover, we interpret a choice operator for quotient types that, under certain restrictions, allows one to recover a representative from an equivalence class. Since the model is constructed syntactically, the interpretation function from the syntax with quotient types to the model gives rise to a procedure which eliminates quotient types by replacing propositional equality by equality relations defined by induction on the type structure (“book equalities”).
Supported by a EU HCM fellowship, contract number ERBCHBICT930420
Preview
Unable to display preview. Download preview PDF.
References
Thorsten Altenkirch. Constructions, normalization, and inductive types. PhD thesis, University of Edinburgh, 1994.
Hendrik Barendregt. Functional programming and lambda calculus. Handbook of Theoretical Computer Science, Volume B.
Michael Beeson. Foundations of Constructive Mathematics. Springer, 1985.
Errett Bishop and Douglas Bridges. Constructive Analysis. Springer, 1985.
J. Cartmell. Generalized algebraic theories and contextual categories. PhD thesis, Univ. Oxford, 1978.
Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76:95–120, 1988.
Robert Constable et al. Implementing Mathematics with the Nuprl Development System. Prentice-Hall, 1986.
Herman Geuvers and Benjamin Werner. On the Church-Rosser property for expressive type systems. LICS '94.
M. J. C. Gordon and T. F. Melham. Introduction to HOL. Cambridge, 1993.
Martin Hofmann. Elimination of extensionality for Martin-Löf type theory. LNCS 806.
Bart Jacobs. Quotients in Simple Type Theory. submitted.
Bart Jacobs. Comprehension categories and the semantics of type theory. Theoretical Computer Science, 107:169–207, 1993.
J. Lambek and P. Scott. Introduction to Higher-Order Categorical Logic. Cambridge, 1985.
I. Moerdijk and S. Mac Lane. Sheaves in Geometry and Logic. Springer, 1992.
B. Nordström, K. Petersson, and J. M. Smith. Programming in Martin-Löf's Type Theory, An Introduction. Clarendon Press, Oxford, 1990.
Wesley Phoa. An introduction to fibrations, topos theory, the effective topos, and modest sets. Technical Report ECS-LFCS-92-208, LFCS Edinburgh, 1992.
Andrew Pitts. Categorical logic. In Handbook of Theoretical Computer Science. Elsevier Science, 199? to appear.
Jan Smith. The independence of Peano's fourth axiom from Martin-Löfs type theory without universes. Journal of Symbolic Logic, 53(3), 1988.
Thomas Streicher. Semantics of Type Theory. Birkhäuser, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hofmann, M. (1995). A simple model for quotient types. In: Dezani-Ciancaglini, M., Plotkin, G. (eds) Typed Lambda Calculi and Applications. TLCA 1995. Lecture Notes in Computer Science, vol 902. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014055
Download citation
DOI: https://doi.org/10.1007/BFb0014055
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59048-4
Online ISBN: 978-3-540-49178-1
eBook Packages: Springer Book Archive