3 ms·

What’s HoTT?

• AnimalMuppet 6y ago
  Homotopy type theory (https://en.wikipedia.org/wiki/Homotopy_type_theory https://en.wikipedia.org/wiki/Homotopy_type_theory). Some people think it's the new mathematical theory of everything. I'm more skeptical.
  • bopbeepboop 6y ago
    My perspective is that it’s a useful idea for abstraction — which combined with category theory’s ability for composition is cool beans, at least in computer science. The square in a category diagram is a legit object — and we can have type theories with the same features. That’s useful for computational equivalence (eg, spec matches implementation) and path bundling to prevent case explosion. About what you’d expect from adding homotopies to type theory.