# About constructive mathematics and Homotopy type theory

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?

-
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: math.andrej.com/2014/01/13/… – 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