Inductive Data Types: Well-ordering Types Revisited
Healfdene Goguen and Zhaohui LuoAbstract: 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.
Previous | Index | Next