/sci/ - Science & Math

It was born dead. The hope was not unjustified, but it turns out to be rather empty. As a side product, though, we got some geometry and physicists spoke with mathematicians again for some time - that's qt.
Not sure for what the grand money would have been spend if it was never tapped on.

>>8246352
Homotopy Type Theory is a particular type theory, a variant of Intuitionistic type theory (and as such capable of expressing fundamental mathematics, and thus general mathematics), and with semantics in higher category theory, and with primitive concepts that make encoding of homotopy theory possible.

Univalent foundations is the perspective of taking homotopy types as primitive concepts (as realized in Homotopy Type Theory), e.g. as opposed to sets, and as such it's a system that can be tried and implemented (via Homotopy Type Theory, say). The creator is a (weird edgy Russian) fields medal winning homotopy theorist.

The people in the former subject (comp sci people) do basic formal how to realize this stuff math. One of their main challanges is to realize the Univalence Axiom as a constructive principle, give meaning to it.
The latter one guy does and thinks homotopy type theoretically, abstract math. He came up with that axiom, and in higher category, stating it just means "I'll only consider systems where it holds". Just like in set theory, if you require well-foundedness for your sets, then you just disregard all set concepts that doesn't have it (like non-well-founded set theory).
He's more on the categorical semantics side and not tied to the above type theory.

>>8246363
I don't think there is or can be quick enough progress to make it really interesting not directly involved with the people who work on it. To be quite honest.