Links und Funktionen

You are here: Home / Publikationen / A Simple Model for Quotient Types


Martin Hofmann (1995)

A Simple Model for Quotient Types

In: Typed Lambda Calculi and Applications, Second International Conference on Typed Lambda Calculi and Applications, TLCA '95, Edinburgh, UK, April 10-12, 1995, Proceedings, ed. by Mariangiola Dezani-Ciancaglini and Gordon D. Plotkin, vol. 902, pp. 216-234, Springer. Lecture Notes in Computer Science (ISBN: 3-540-59048-X).

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).

Document Actions