I've been reading Andrej Bauer's blog post on "Univalent foundations subsume classical mathematics," which explains how Univalent Foundations and Homotopy Type Theory (HoTT) extend classical mathematics by incorporating types stratified by homotopy-theoretic complexity. The post discusses that logic and sets are seen as lower-level types in this extended framework, but it also introduces higher types such as groupoids and beyond.

My question pertains to the necessity and utility of these higher types in HoTT:

1. Redundancy Concern: In traditional set theory, particularly within Zermelo-Fraenkel (ZF) or Zermelo-Fraenkel with the Axiom of Choice (ZFC), we are able to construct a vast array of mathematical structures. Given this capability, what additional structures or benefits do higher types in HoTT (beyond logic and sets) provide? Are they not redundant since every mathematical construction achievable in HoTT seems also constructible in ZFC?

2. Unique Constructions: Are there specific examples of mathematical structures that cannot be constructed within the ZF or ZFC framework but can be realized using the higher types in HoTT? If so, what are these structures, and how do higher types facilitate their construction?

Thank you for your insights

I've been reading Andrej Bauer's blog post on "Univalent foundations subsume classical mathematics," which explains how Univalent Foundations and Homotopy Type Theory (HoTT) extend classical mathematics by incorporating types stratified by homotopy-theoretic complexity. The post discusses that logic and sets are seen as lower-level types in this extended framework, but it also introduces higher types such as groupoids and beyond.

My question pertains to the necessity and utility of these higher types in HoTT:

1. Redundancy concern: In traditional set theory, particularly within Zermelo-Fraenkel (ZF) or Zermelo-Fraenkel with the Axiom of Choice (ZFC), we are able to construct a vast array of mathematical structures. Given this capability, what additional structures or benefits do higher types in HoTT (beyond logic and sets) provide? Are they not redundant since every mathematical construction achievable in HoTT seems also constructible in ZFC?

2. Unique constructions: Are there specific examples of mathematical structures that cannot be constructed within the ZF or ZFC framework but can be realized using the higher types in HoTT? If so, what are these structures, and how do higher types facilitate their construction?

Thank you for your insights.