4 ms·
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 homot
by 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 agoFrom 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 agoIt is my understanding that HITs are just as easy to integrate into non-homotopy type theories as they are to HoTTs.