We study a transfinite construction we call tower construction in classical type theory. The construction is inductive and applies to partially ordered types. It yields the set of all points reachable from a starting point with an increasing successor function and a family of admissible suprema. Based on the construction, we obtain type-theoretic versions of the theorems of Zermelo (well-orderings), Hausdorff (maximal chains), and Bourbaki and Witt (fixed points). The development is formalized in Coq assuming excluded middle.
CITATION STYLE
Smolka, G., Schäfer, S., & Doczkal, C. (2015). Transfinite constructions in classical type theory. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9236, pp. 391–404). Springer Verlag. https://doi.org/10.1007/978-3-319-22102-1_26
Mendeley helps you to discover research relevant for your work.