3 ms·

I wonder if there's anyone here working on Homotopy Type Theory that can explain what it is, and how it is used in modeling? I skimmed the PDF of the book but

by wenc 8y ago

I wonder if there's anyone here working on Homotopy Type Theory that can explain what it is, and how it is used in modeling? I skimmed the PDF of the book but am drawing blank as to its connection to an application. Perhaps it's used for verification of concepts, similar to how formal methods in CS (e.g. TLA+) are used to conceptually check algorithms?

Darmani 8y ago
One application: It makes it easier to do mechanized reasoning to optimize SQL queries. https://arxiv.org/pdf/1607.04822.pdf https://arxiv.org/pdf/1607.04822.pdf
- tzs 8y ago
  Abstract: https://arxiv.org/abs/1607.04822 https://arxiv.org/abs/1607.04822
empath75 8y ago
It’s basically a new foundation for math based on types rather than sets.
- galaxyLogic 8y ago
  What is the basic difference between types and sets? From the software engineering point of view a type is something of which you can say whether something is a member of the type. And the same thing can be set about sets.
  - empath75 8y ago
    https://golem.ph.utexas.edu/category/2013/01/from_set_theory_to_type_theory.html https://golem.ph.utexas.edu/category/2013/01/from_set_theory...
  - fmihaila 8y ago
    The difference lies in the means you have at your disposal to settle the membership question. Even within "Set Theory" (as an umbrella term), there are several axiomatizations of sets that define in different ways what a set is, how sets come into existence, what it means for an element to belong to a set, and what are the allowed ways to conclude that it does or does not. The link posted in a sibling comment by @empath75 goes into more detail.
deleted 8y ago
[deleted]
T-R 8y ago
HoTT was a popular topic in the Haskell ecosystem a little while back, so worth digging around there for info: - https://softwareengineering.stackexchange.com/questions/262377/what-are-the-practical-implications-of-homotopy-type-theory-in-programming https://softwareengineering.stackexchange.com/questions/2623... - https://www.reddit.com/r/haskell/comments/6nxgkc/similarities_and_differences_between_homotopy/ https://www.reddit.com/r/haskell/comments/6nxgkc/similaritie... - https://bartoszmilewski.com/category/homotopy-type-theory/ https://bartoszmilewski.com/category/homotopy-type-theory/
chadcmulligan 8y ago
This is interesting https://www.youtube.com/watch?v=E9RiR9AcXeE https://www.youtube.com/watch?v=E9RiR9AcXeE a bit of the history and why it was needed.
orbifold 8y ago
Personally I don't think it has any practical applications, but rather that this continues the trend of using the military to fund fundamental research. The main interest would probably be that HoTT allows for automatic theorem proving of more interesting theorems compared to other axiomatisations. It was originally designed to be able to do higher homotopy theory synthetically. The Lean theorem prover has actually dropped HoTT support. There is a certain chance that interest will vane after the founder Voevodsky died.

by wenc 8y ago

Darmani 8y ago

One application: It makes it easier to do mechanized reasoning to optimize SQL queries. https://arxiv.org/pdf/1607.04822.pdf https://arxiv.org/pdf/1607.04822.pdf

tzs 8y ago
Abstract: https://arxiv.org/abs/1607.04822 https://arxiv.org/abs/1607.04822

empath75 8y ago

It’s basically a new foundation for math based on types rather than sets.

galaxyLogic 8y ago
What is the basic difference between types and sets? From the software engineering point of view a type is something of which you can say whether something is a member of the type. And the same thing can be set about sets.
- empath75 8y ago
  https://golem.ph.utexas.edu/category/2013/01/from_set_theory_to_type_theory.html https://golem.ph.utexas.edu/category/2013/01/from_set_theory...
- fmihaila 8y ago
  The difference lies in the means you have at your disposal to settle the membership question. Even within "Set Theory" (as an umbrella term), there are several axiomatizations of sets that define in different ways what a set is, how sets come into existence, what it means for an element to belong to a set, and what are the allowed ways to conclude that it does or does not. The link posted in a sibling comment by @empath75 goes into more detail.

deleted 8y ago

[deleted]

T-R 8y ago

HoTT was a popular topic in the Haskell ecosystem a little while back, so worth digging around there for info: - https://softwareengineering.stackexchange.com/questions/262377/what-are-the-practical-implications-of-homotopy-type-theory-in-programming https://softwareengineering.stackexchange.com/questions/2623... - https://www.reddit.com/r/haskell/comments/6nxgkc/similarities_and_differences_between_homotopy/ https://www.reddit.com/r/haskell/comments/6nxgkc/similaritie... - https://bartoszmilewski.com/category/homotopy-type-theory/ https://bartoszmilewski.com/category/homotopy-type-theory/

chadcmulligan 8y ago

This is interesting https://www.youtube.com/watch?v=E9RiR9AcXeE https://www.youtube.com/watch?v=E9RiR9AcXeE a bit of the history and why it was needed.

orbifold 8y ago

Personally I don't think it has any practical applications, but rather that this continues the trend of using the military to fund fundamental research. The main interest would probably be that HoTT allows for automatic theorem proving of more interesting theorems compared to other axiomatisations. It was originally designed to be able to do higher homotopy theory synthetically. The Lean theorem prover has actually dropped HoTT support. There is a certain chance that interest will vane after the founder Voevodsky died.