Preliminaries
Sets as Predicates
Orders
Extensional Types and Types with Choice
Specialized Tower Construction
Linearity of Specialized Towers
Well-Ordering of Specialized Towes
Instances of the Special Tower Construction
Hausdorff
Zermelo
Existence of Well-Ordered Extensions
General Tower Construction
Linearity of General Towers
Fixed Point Theorem
Well-Ordering of General Towers
Instances of the General Tower Construction
Bourbarki-Witt
General Hausdorff
This page has been generated by
coqdoc