/sci/ - Science & Math

don't know how to help but bump

>>9594959
No idea, but is it worth while to study hott? where does it lead to/when is it used?

>>9596107
>where does it lead to/when is it used?
Nowhere/never.

>>9596133
Then what the point?

>>9596140
>pure math
>what is the point

um...

>>9596107
>when is it used
← found that kid

>>9594959
>Can't you port over the bar construction?
The problem lies essentially in realizing the relevant simplicial object. HoTT, or at least "book HoTT", is constructive in such a way that writing down an infinite object like the bar complex would take an infinite amount of data. This is one of the major current problems with HoTT, and is also why we don't have native infinity categories (but see work of Riehl Shulman for one hack).

>>9596757
>>9596339
Even pure math has a point, category theory is used to find correspondences between different areas of math and abstract them, group theory is used to classify the finite simple groups, set theory is used to create a basis for other math. Inter universal testicular theory is used to prove the abc conjecture. But this has nothing?

>>9597350
I remember attending one of Voevodsky's lectures on the subject, and he said that he went from his old stuff to working on univalent foundations because his proofs started becoming more complicated and he wanted an automatic proof checker. Apparently, there's some programs-as-proofs correspondence that goes through HoTT.

>>9597350
Homotopy type theory is the language of higher category theory. When you work with sets, a proof of equality of two elements of the set carries with it no additional information other than the fact that two elements are equal. But when you work with categories, two things can be equal in multiple ways, both canonically and non-canonically. This is because we identify two things when there are morphisms going between them. The choice of morphism can affect the identification.

Proofs in HoTT are thought of as being objects of a given type, one that must be constructed, and one that can be referenced in later proofs. This means that you can encode data about the construction of a canonical object within the theorem and pass this data from theorem to theorem. This feature of homotopy type theory, called proof-relevance, facilitates bookkeeping of canonical objects when working in categories.

This may not seem like much, but imagine writing a long proof with many canonical choices or working with a (weak) 2-category, where you have morphisms of morphisms, and you can only identify morphisms up to bijections between morphisms. Or (weak) 3-categories, where you have morphisms of morphisms of morphisms.

This has caused mathematicians a lot of agony. HoTT offers a way out. The fact that there's an infinity-groupoid structure on types means that there's this natural way of thinking of types as spaces, which is a plus.

>>9596812
Thanks. Will do!

>>9597420
iirc, just the definition of a weak 3-category is p agonizing

>>9597420
>>9597399
Thanks.