Showing changes from revision #81 to #82:
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.
Honestly, I don’t really care about classical foundational axioms such as axiom K, UIP, excluded middle, or the axiom of choice.
But there are two problems with the dominant foundational frameworks in mathematics. In any kind of set theory, there are two notions of logic: the external logic using the primitive notion of proposition and predicate, and the internal logic using subsingletons and families of subsingletons; there is no need to have two logics in the theory, only one suffices. In any kind of dependent type theory with judgmental equality, there are two notions of equality, judgmental equality and the identity type; there is no need to have two equalities in the theory, only one suffices. However, the only people who have worked on a foundational framework with only one notion of logic and only one notion of equality are two Dutchmen from the University of Amsterdam, Benno van den Berg and Martijn den Besten, with their objective type theory, which has neither an external logic nor judgmental equality.