Return to Answer

edited body

Source Link

edited Jul 18, 2019 at 18:22

HoTT differs from ZFC in several aspects and it is useful to separate them:

ZFC is a structuralmaterial set theory while HoTT is a materialstructural one. This means that we cannot ask whether one set belongs to another (that is, there is not predicate $\in$). This implies that the notion of a subset also does not make sense. Subsets of a set $X$ must be replaced with (equivalence classes) of injective maps into $X$ (as you suggested). This is not a big problem in practice, it is just a different style of working with sets. If you want to learn more about differences between these approaches to set theory, Michael Shulman, Comparing material and structural set theories is a very nice source.
HoTT is constructive by default, but this does not mean that you cannot use classical logic. Actually, you can simply add the law of excluded middle and the axiom of choice to HoTT if you want to. The resulting theory will be consistent and very close to ZFC.
The basic objects of ZFC are sets while the basic objects of HoTT are homotopy types. If you are not interested in homotopy theory, you can simply ignore types which are not sets. The only problem is that the universe of sets (and groups, and so on) is not a set. This issue is not a big problem in practice since usually you do not need to talk about equality between sets (and the only difference between sets and types is that the equality between elements of a type is not a proposition, so it does not really work like ordinary equality).

HoTT differs from ZFC in several aspects and it is useful to separate them:

ZFC is a structural set theory while HoTT is a material one. This means that we cannot ask whether one set belongs to another (that is, there is not predicate $\in$). This implies that the notion of a subset also does not make sense. Subsets of a set $X$ must be replaced with (equivalence classes) of injective maps into $X$ (as you suggested). This is not a big problem in practice, it is just a different style of working with sets. If you want to learn more about differences between these approaches to set theory, Michael Shulman, Comparing material and structural set theories is a very nice source.
HoTT is constructive by default, but this does not mean that you cannot use classical logic. Actually, you can simply add the law of excluded middle and the axiom of choice to HoTT if you want to. The resulting theory will be consistent and very close to ZFC.
The basic objects of ZFC are sets while the basic objects of HoTT are homotopy types. If you are not interested in homotopy theory, you can simply ignore types which are not sets. The only problem is that the universe of sets (and groups, and so on) is not a set. This issue is not a big problem in practice since usually you do not need to talk about equality between sets (and the only difference between sets and types is that the equality between elements of a type is not a proposition, so it does not really work like ordinary equality).

HoTT differs from ZFC in several aspects and it is useful to separate them:

ZFC is a material set theory while HoTT is a structural one. This means that we cannot ask whether one set belongs to another (that is, there is not predicate $\in$). This implies that the notion of a subset also does not make sense. Subsets of a set $X$ must be replaced with (equivalence classes) of injective maps into $X$ (as you suggested). This is not a big problem in practice, it is just a different style of working with sets. If you want to learn more about differences between these approaches to set theory, Michael Shulman, Comparing material and structural set theories is a very nice source.
HoTT is constructive by default, but this does not mean that you cannot use classical logic. Actually, you can simply add the law of excluded middle and the axiom of choice to HoTT if you want to. The resulting theory will be consistent and very close to ZFC.
The basic objects of ZFC are sets while the basic objects of HoTT are homotopy types. If you are not interested in homotopy theory, you can simply ignore types which are not sets. The only problem is that the universe of sets (and groups, and so on) is not a set. This issue is not a big problem in practice since usually you do not need to talk about equality between sets (and the only difference between sets and types is that the equality between elements of a type is not a proposition, so it does not really work like ordinary equality).

Source Link

created Jul 18, 2019 at 15:40

HoTT differs from ZFC in several aspects and it is useful to separate them:

ZFC is a structural set theory while HoTT is a material one. This means that we cannot ask whether one set belongs to another (that is, there is not predicate $\in$). This implies that the notion of a subset also does not make sense. Subsets of a set $X$ must be replaced with (equivalence classes) of injective maps into $X$ (as you suggested). This is not a big problem in practice, it is just a different style of working with sets. If you want to learn more about differences between these approaches to set theory, Michael Shulman, Comparing material and structural set theories is a very nice source.
HoTT is constructive by default, but this does not mean that you cannot use classical logic. Actually, you can simply add the law of excluded middle and the axiom of choice to HoTT if you want to. The resulting theory will be consistent and very close to ZFC.
The basic objects of ZFC are sets while the basic objects of HoTT are homotopy types. If you are not interested in homotopy theory, you can simply ignore types which are not sets. The only problem is that the universe of sets (and groups, and so on) is not a set. This issue is not a big problem in practice since usually you do not need to talk about equality between sets (and the only difference between sets and types is that the equality between elements of a type is not a proposition, so it does not really work like ordinary equality).