[fmap]

Sorry if I wasn't clear about this, but you can embed classical mathematics in a type theory with univalence. If you look into the HoTT book, there is a chapter on set theory in type theory. The general form of excluded middle is inconsistent, because it would collapse the structures on which univalence is built.

This means that classical mathematics still works as expected, so long as you have the assumption that you are working with things that are "set-like". Additionally you can make any type "set-like", since this amounts to manually collapsing its equality type.

However... the truth is that most of the time excluded middle is unnecessary (in a type theory). Having nice equality types is so much more useful that, honestly, you are not making an informed decision.

[fmap]

Answer to auggierose's comment above: Yes you can prove that sqrt(2) is irrational.

This is actually a great example, because it doesn't need excluded middle. Equality of rational numbers is decidable, which means that classical reasoning is provable. And yes, even if it wasn't, it would still work.

Edit: Ok, this was apparently confusing, so let me repeat it here. Yes, the same proof works. This form of excluded middle is entirely unproblematic.

[Chattered]

There might be some confusion. The typical proof of the irrationality of root 2 is phrased as a proof-by-contradiction, and I've come across folk who mistakenly think that this technique is exclusive to classical mathematics.

In fact, the standard proof-by-contradiction that sqrt(2) is irrational is also intuitionistically valid. The important point for this case is that we're proving a negative property (irrationality), so this sort of proof by contradiction is fine.

The standard example of a classical proof I use is the one showing that there exist irrationals x and y such that x^y is rational. The dead easy proof asks whether x^y is rational for x=y=sqrt(2). If it is, we're done. Otherwise, we just take x=sqrt(2)^sqrt(2) and y=sqrt(2).

But note that we don't actually know for sure which x and y work, so this is definitely classical. An intuitionistic proof here would have to tell us directly what x and what y work.

[auggierose]

Good point. So then the question becomes: can you prove in HoTT that there exist irrational x, y such that x^y is rational?

[fmap]

Yes. You can translate the classical proof, assuming excluded middle for propositions.

[auggierose]

Sigh. It is really hard to get straight answers out of constructivists / type theorists.

So let's say I am writing a theorem proving system based on HoTT (with univalence). Can I then do the classic proof of the irrationality of the square root 2 in that system? Then this would be classical mathematics as I expect it.

[auggierose]

Answer to the answer to my comment :-) :

This is exactly the answer I expected. It was a little bit of a trap, I have to admit that.

I didn't ask for any proof of the irrationality of square root 2. I asked specifically for the classic proof. Which I cannot do. So it is not classic mathematics as usual.

An honest answer to this whole thread would have been: "No, you cannot do classical mathematics as you were used too. You have to give stuff up, but I think that you will gain other stuff in exchange, and in my opinion this other stuff is more valuable than the stuff you gave up."

[ek]

Note that fmap writes: "Equality of rational numbers is decidable, which means that classical reasoning is provable. And yes, even if it wasn't, it would still work."

What is meant by "even if it wasn't, it would still work" goes back to something he said earlier: type theory embeds an infinite hierarchy of axioms of choice and laws of excluded middles. If you want to do propositional-like reasoning in homotopy type theory, you can assume AC or LEM for homotopy (-1)-types, corresponding to propositional logic.

In type theory you are encouraged to drop the law of the excluded middle and the axiom of choice, because of the fact that doing so gives you potentially more expressive ways of doing things as we have said, but you have gotten the impression that you have to, which you don't.

Also, the claim in this thread was that the results from classical mathematics are provable using homotopy type theory, not that they are provable in the same way (though that holds as well, as I've said above; it's just that the mathematics might not look as clean as if you did it in a more idiomatic way). This kind of a value proposition is not exactly new: category theory loses certain axioms over set theory and mathematicians adapted to the point that category theory is now the language of modern algebra.

I want to point out that I suggested that you read the introduction to the book because it provides these same answers to the questions you are wondering about. I still suggest you do so, as it goes into more detail on what we have said here in a way that I am not able to quite as well.

[auggierose]

I already read the introduction a couple of months ago, pretty much on the day when they officially announced that the book is available.

From what I understand: If you are a type theorist / constructivist, then certain constructions will not be provably equivalent, although their classical counterparts are. Some of those classically trivial equivalences might be recovered though via the univalence axiom. Is that correct or totally wrong? Furthermore it seems to me from the discussions with fmap, that if I am a classical mathematician, I cannot use HoTT (unless I am willing to compromise and give up some of my power).

[ek]

Your understanding of univalence seems essentially correct to me.

At this point we are mostly debating what "can use" means -- it's probably enough to say that unless you reframe your thinking, perhaps radically, probably it will be hard for you to be able to use HoTT to get work done. It is possible to do classical mathematics within HoTT, in the normal way, but it would not be very fun.

[auggierose]

Also I see that you are interested in SMT solvers. Isn't it a fact that automation becomes HARDER when using type theory, not EASIER?

[ek]

Yes :) My interest in homotopy type theory is only auxiliary to my research. Designing dependent type systems in a way that balances tractability with expressiveness is a pretty hard thing to do. SMT solvers are nice because you can treat them as oracles and "see what happens". I'm not an expert on decision procedures, and I'd characterize myself more as a user of solvers than a developer of them, though of course once you get deep enough in, that line blurs.