Showing changes from revision #83 to #84:
Added | Removed | Changed
As of 6 June 2022, the HoTT web is regarded as deprecated. Every single one of the articles on the HoTT web has been ported to the main nLab web. All further HoTT-related editing should happen on the main nLab web.
Set theory vs homotopy type theory is a completely different issue from predicative and constructive mathematics.
The former difference is between how equality and logic are treated in the foundations: are there one or two notions of equality, and one or two notions of logic.
The latter difference is between the strength of the theory in set-level mathematics, ranging from strictly predicative mathematics, which only has dependent product types for identity types, centers of contraction, and subsingletons, all the way to mathematics with a choice set operator, where from every witness of an inhabited set one could get a term of the set. This could be done in pure set theories, non-pure material set theories, structural set theories, and in homotopy type theory with univalent universes. This is relevant to doing actual mathematics, but not really relevant when it comes to the treatment of equality and logic in the foundations.