The point of the ZFC axioms was never to write down actual formalizations of complicated proofs. It was to provide a small, parsimonious foundation for all of mathematics with a minimal number of "obvious" commitments, to give us confidence that the mathematics we're doing is consistent, and to provide a basis for metamathematical investigations. (Roughly speaking - this compresses a lot of history. Also ZFC may not be the optimal set theory for doing this, and its choice as the standard foundation is somewhat historically contingent.)
A good analogy is the idea of a Turing machine in theoretical CS. It's an idealized model for studying the theory of computation. To object that it's impractical to write a complicated program like a computer algebra system using the Turning machine formalism misses the point.
> The key idea of univalence is an axiom that says equivalence is equivalent to equality; and that if we only want equivalence as our standard, that we can substitute proofs of equivalence for proofs of equality.
I just said I don't want equivalence to be equivalent to equality!
> The main insight is that topology of diagrams determines the semantics of your logic; which helps us explore concepts like abstraction and proof simplification. (This relates to topos theory — which creeps up in CS fairly often.)
OK, so what are the concrete fruits of this? What new metamathematical statements - recognizable to an ordinary mathematician with no particular interest in topos theory or HoTT - has this led to?
A good analogy is the idea of a Turing machine in theoretical CS. It's an idealized model for studying the theory of computation. To object that it's impractical to write a complicated program like a computer algebra system using the Turning machine formalism misses the point.
> The key idea of univalence is an axiom that says equivalence is equivalent to equality; and that if we only want equivalence as our standard, that we can substitute proofs of equivalence for proofs of equality.
I just said I don't want equivalence to be equivalent to equality!
> The main insight is that topology of diagrams determines the semantics of your logic; which helps us explore concepts like abstraction and proof simplification. (This relates to topos theory — which creeps up in CS fairly often.)
OK, so what are the concrete fruits of this? What new metamathematical statements - recognizable to an ordinary mathematician with no particular interest in topos theory or HoTT - has this led to?