Viewing a single comment thread. View all comments

Matsarj t1_ixjliwb wrote

So I'm pretty familiar with homotopy theory but don't know any type theory, homotopy or otherwise. What does determining whether types are homotopy equivalent get you in terms of ML applications?

1

LazyHater t1_ixjq0v8 wrote

In "laymans" terms, it gives you a) an environment for ML models to verify their proofs and b) and rich space for ML to study relations between different fields of mathematics, logic, philosophy, ethics, and everything else by default at that point.

propositions are implementations of types so just being able to say when propositions are equivalent in like a rigorous way is good for science anyways.

3