Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

I am a CSer and I am reading the HoTT book and found that doing math with computer is fascinating.

I found that constructive math compared with classical math is beautiful because:

  • type theoretic foundation is far more beautiful that set theoretic foundation
  • proof relevant math
  • machined checked proof

but one thing that bugged me is that some classical structures is so complicated in constructive math, and "classically equivalent notions bifurcate", for example

  • we have two kinds of real number and
  • we have 3 kinds of compactness (HoTT p.391)

Is this means that constructiveness brings us more insight into math, or just it's inability without the law of exclude in the middle? Can we have machine-checked proof in classical mathematics?

share|cite|improve this question
The bifurcation/trifurcation/$\infty$-furcation is not a bug, it's a feature. You get more precise results! You do care in real life whether your reals are computable to precision $n$ in $O(n)$, or in $O(n^2)$, or in some Ackermann time, or never. (That said, I wish the bifurcation of constructive mathematics itself into constructive and univalent wouldn't exist...) – darij grinberg Dec 22 '13 at 16:58
May I suggest an edit? After "I found that constructive math compared with classical math is beautiful" just write "for a variety of reasons" and skip the dot points. In my opinion, they merely distract from the actual question. Also, I would change the title to: Constructive mathematics and the "bifurcation" of classically equivalent notions. Or something along those lines. – goblin Dec 22 '13 at 16:58
There's a recent blog post by Andrej Bauer which addresses your issues too:… – Egbert Jan 18 '14 at 13:33
@Egbert Thanks! I have already read this post, and there are still many mysteries about hott for me. Maybe it is just too hard for an ordinary programmer like me. Nonetheless I will try to understand the book because the idea is really fascinating – Minghao Liu Jan 18 '14 at 17:27
Don't hesitate to ask more questions. That's what the site is for :) – Egbert Jan 18 '14 at 17:54
up vote 1 down vote accepted

An important aspect of the Univalent Foundations is that it is compatible with classical mathematics. In fact, Voevodsky's simplicial set model of Martin-Lof type theory with the univalence axiom models the law of excluded middle too. So if you insist on doing things classically in Homotopy Type Theory, you may do so to your hearts content. You will only loose a bit of generality, i.e. your constructions will not work in every model of the type theory but only in the classical ones. But the computer assisted theorem proving won't be lost by just assuming LEM. However, when you have a computer proof that involves the axiom of choice of the law of excluded middle and you try to execute your proof (as if it were a program) the computer will get stuck on the instances where you have applied AC or LEM.

As for the various notions of real numbers or compactness, consider it a richness or a deficiency. It depends on your purposes, which you haven't explained.

share|cite|improve this answer
Thanks for the reply!! I recently have read more about hott and have other questions. If univalence axiom has no computational meaning now, how could it possible to do hott with computer like in Coq? – Minghao Liu Jan 17 '14 at 17:19
The cubical sets model, which addresses computational aspects of the univalence axiom, has recently been announced on the homotopytypetheory mailing list. Currently, Coq can't compute with univalence, but that might soon change :) How it is possible to do HoTT in Coq? The same way anything is done in Coq: see – Egbert Jan 17 '14 at 18:08

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.