> The disadvantage of set theory is that its principles are very difficult to translate into the programming language of a proof assistant.

I don't think that's true. There's an Isabelle theory for ZF, and the ZF axioms are actually simpler than the axiomatic system that Coq uses, the Calculus of Inductive Constructions.

Backing up for a second, I'm just not sure how HoTT will make using proof assistants so much simpler. I've done a couple of largish (> 1000 lines) proof developments in Coq. The hardest part never seemed to me to be that mismatch between CIC and ZF. The hard part was that proofs are actually hard to do in a careful and complete way. The proofs I did in math class were easy because we left out a lot of the details.

Let me give an example. This is from the HoTT book, Book version: first-edition-611-ga1a258c, page 368:

"The field of rationals Q is constructed along the same lines as well, namely as the quotient

Q : ≡ ( Z × N ) / ≈

where

( u, a ) ≈ ( v, b ) : ≡ ( u ( b + 1 ) = v ( a + 1 )) .

In other words, a pair ( u, a ) represents the rational number u/ ( 1 + a ) . There can be no division by zero because we cunningly added one to the denominator a. Here too we have a canonical choice of representatives, namely fractions in lowest terms. Thus we may apply Lemma 6.10.8 to obtain a set Q, which again has a decidable equality.

We do not bother to write down the arithmetical operations on Q as we trust our readers know how to compute with fractions even in the case when one is added to the denominator. Let us just record the conclusion that there is an entirely unproblematic construction of the or- dered field of rational numbers Q, with a decidable equality and decidable order. It can also be characterized as the initial ordered field."

If you have experience with using proof assistants, you know how handwavy this is compared to the work required to actually get this done. Here's that development in Coq right now:

https://github.com/coq/coq/tree/trunk/theories/QArith

Does HoTT really make these things simpler to write and prove? If so, what is the evidence?

"Does HoTT really make these things simpler to write and prove? If so, what is the evidence?"

There are people who can answer that question (or at least try to, after all I can not guarantee satisfaction), I am not one of them, and based on previous conversations on this topic, very few of them are here. (Not necessarily zero, but few.)

I would suggest searching Math Overflow for an answer to your question, and failing that, post it. http://mathoverflow.net/search?q=hott (And if you do, please drop a reply to me with a link. I'd be interested to at least read the result, though I'm well out of my depth to be commenting on it.)

I'm no expert, but I believe the hope is that quotients are easier to work with in HoTT than they would be elsewhere since you can treat the resulting "cosets" as true objects instead of structure with proof.

Also, it should be much easier to transport proofs from type to type according to isomorphisms that are discovered.

I'm hardly versed enough to say whether those things are (a) true (b) actually occurring (c) powerful enough to be worth the potential headaches HoTT incurs or (d) deserving of acclaim, but it's at least my understanding.

As far as quotients go, I have used setoids before for that purpose. Maybe HoTT makes quotients even more convenient.

http://coq.inria.fr/V8.2pl1/refman/Reference-Manual030.html

Yes, my understanding is that quotients should be much more convenient to use than setoids. Univalance means you can more or less ignore equality in the quotient after you define it---proofs should just be transportable.

The problem is not whether HoTT is easier than ZF. The problem is that ZF is impossible to be used in a proof assistant because it uses classical logic. HoTT uses intuitionistic logic where all proofs are constructive.

Non-constructive proofs aren't problematic for theorem provers---they just have no computable interpretation.

You can just assert the Law of Excluded Middle if you like whenever and all of the programs "downstream" will still be checkable. You can even technically provide computable semantics to Pierce's law via call/cc.

I'm curious - can anyone point me to an overview/exposition of this that is more hand-wavy than the book? I'm interested understanding the ideas in this work, because proofs as objects would be a major step forward, but I don't even know much about the existing systems of foundations (ZFC etc), nevermind type theory...

Did you read the Introduction from pp1-12 of HoTT? I thought it was a pretty good overview.

I tried. I was hoping for something more like: "a field is something you can add, subtract, multiply, & divide in" and less like: "a field is a set that is a commutative group with respect to two different operations (excepting 0), linked by the distributive law".

I need something to hold on to when reading the more formal treatment.

I highly suggest Robert Harper's lectures from the Oregon Programming Languages Summer School. I watched the OPLSS'12 lectures, but I'm sure they're great any year.

The Mizar project has been verifying a good share of math results for decades, not to demerit HoTT but to clarify the article.

They are almost certainly aware of Mizar. Mizar's foundation is ZFC+Tarski's axiom. If you are developing a foundation based on homotopy theory/type theory you probably don't care about results formalized in Mizar. Also the type theory people in general prefer constructivist mathematics, and would reject Axiom of Choice and friends being in the foundation.

But doesn't Mizar void the argument that we need a new foundation as set theory has not been conducive to mechanized proofs?

I think this is right (not an HoTT expert), it voids it. I'd say that what type theory brings in, that didn't come for free in set theory (ZFC or Mizar's Tarski-Grodendiek extension), is the Curry-Howard correspondence that has the slogan "propositions as types, proofs as programs". With that correspondence you can see the same thing as a program (in a typed lambda calculus depending of the type theory of interest), or as a proof in a corresponding logic.

I don't think the argument is that it's impossible to mechanize proofs outside of HoTT---just that it's prettier and perhaps better there.

"Prettier" is subjective.

Absolutely. Never claimed otherwise.

Vladimir Voevodsky is making an interesting step when he says that rewrite steps in math are clearly homeomorphisms. I would like to see some more formal examples of that. It sounds like a promising path.

Concerning the replacement of ZFC by Russell types -- contrary to lambda calculus' functions -- I have not run often enough in illustrations that demonstrate the usefulness of Russell types.

I am personally much more vouching for a replacement of Zermelo and Fränkel's sets by Alonzo Church's functions than Bertrand Russell's types at this point. It is probably just an issue of lack of familiarity, though.

Is there anyone approaching the issue from the other side? Meaning, if I have a good understanding of programming and type theory, using that to explain homotopy theory?

I think many people are approaching it that way. Ultimately you can end up using higher inductive types as "synthetic homotopy", i.e. homotopy theory which is by construction valid to the definition instead of carefully isolated from other constructions.

So you can certainly just take the type theory and start to get at pretty large stuff in actual homotopy theory.