Inductive Data Types: Well-ordering Types Revisited

Healfdene Goguen and Zhaohui Luo

Abstract: We consider Martin-Löf's well-ordering type constructor in the context of an impredicative type theory. We show that the well-ordering types can represent various inductive types faithfully in the presence of the filling-up equality rules or v-rules. We also discuss various properties of the filling-up rules.

LFCS report ECS-LFCS-92-209

Previous | Index | Next