HoTT describes any infinity-topos. When folks say "all of mathematics can be rederived constructively", they mean that all of constructive mathematics can be de

HoTT describes any infinity-topos. When folks say "all of mathematics can be rederived constructively", they mean that all of constructive mathematics can be described relative to any topos. Classical mathematics is retrieved either by choosing a Boolean topos, or by developing Boolean algebras inside topos theory. It is a standard theorem that all constructive results are classical, and that all classical results are either constructively true or not-false. A not-false theorem can't be proven true, but it definitely would lead to a contradiction if it were false. To get a taste of what's constructive, imagine taking a subset of the finite set {0,1}. We construct the subset by enumerating its elements; a computer program might print out elements one-by-one. So, if we start a program and it prints 0, 1, ...; we know that the subset contains all of the elements and we're done. But if we start a program and it prints 0, 0, 0, ...; only printing zeros, then we have to prove that it halts in order to prove that the subset is finite. Constructively, subsets of finite sets aren't necessarily finite.