3 ms·

Homotopy type theory probably. Uses in modern theorem prover languages include verification of systems/hardware and formalization of math.

• orangea 4y ago
  How can homotopy type theory, as opposed to non-homotopy type theory, help us with "verification of systems/hardware and formalization of math" outside of homotopy theory itself? My perspective has always been that it can't.
  • m_j_g 4y ago
    From my experience ability to turn equivalences to equlities and vice versa is very usefull. Without this you are ending in setoid hell - intracable mess of isomorphism. I suspect that also Higher Inductive Types have lots of potential to simplify practical verification effords (apart from obvious usecases of quotients and truncations)
    • orangea 4y ago
      It is my understanding that HITs are just as easy to integrate into non-homotopy type theories as they are to HoTTs.