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?