I wouldn't expect homotopy type theory to lead us any closer to artificial general intelligence, but who knows. Maybe this will lead to some opportunities for AI to interact more closely with mathematics in the end.
HoTT and type theories in general, do have some apparent advantages when it comes to making it practical for humans to express proofs in a way which computers can understand, but the entire practice of that is not something which could be said to be extremely well-developed thus far, and so everything is to some degree a big experiment.
As a synthetic approach to homotopy theory, it's a beautiful piece of work, the latest approach in a line of approaches to that. You could say that HoTT is to traditional homotopy theory what axiomatic geometry (where lines are objects unto themselves) is to Cartesian geometry (where lines are collections of points). Homotopy theorists have built various abstractions for capturing that, and HoTT gives a very satisfying one.
As an informal foundations for thinking about mathematics, it's intriguing and certainly has some new ideas about how to approach the definitions of various familiar mathematical objects. Especially for the sorts of things that are normally defined using quotients, those come out looking quite a bit different, since rather than forming equivalence classes in the usual way, we can construct "higher inductive types" which guarantee certain "paths" or "proofs of equality" between particular points/terms, and come equipped with an "induction principle" for defining maps out of the type (or what is the same activity, proving properties about it), and which insist that we say where those paths are sent in the destination, basically guaranteeing that certain equalities-made-tangible are conserved.
Type theories generalise the propositions of logic and sets of set theory into what they call "types" and those types give each mathematical statement a kind of interpretation as a sort of collection of its own proofs, which was formerly usually thought of as a set. HoTT adds a kind of geometry to this set, putting paths between proofs that are in some sense "equal", and that construction can be iterated to give paths-between-paths (surfaces), and so on to higher dimensions.
HoTT shows us that we can divide the types of type theory into levels of which the first few are propositions, sets, and (categorical) groupoids.
I would say most of HoTT grew out of the consequences of noticing this interpretation of what was already a very beautiful and "natural" type theory (Martin-Löf type theory, MLTT) whose original intent was merely to serve as a foundations for mathematics. It gives that theory a more general model than it previously had and turns what from a purely logical perspective might have been seen before as quirky idiosyncrasies to be put up with in exchange for the other very nice theoretical properties of the system, into things which are geometrically obvious from the perspective of thinking about homotopy types of spaces.
Unfortunately, plain Martin-Löf type theory isn't quite adequate on its own -- there is a fairly natural axiom called the univalence axiom, that falls out as an expectation regarding this interpretation of types as homotopy types. It gives us the nice property that types which are in some sense equivalent (or isomorphic), have these "paths" between them, making them "equal" in a containing universe type. This immediately gives us the ability to transport theorems about one construction to another, which is formally not something that could be done in first order logic and set theory. Formally, you would have to prove the theorem again for each isomorphic thing, because first order logic has no way of knowing that mathematicians only allow properties that respect isomorphism in the first place.
This Univalence axiom is also a problem, however. Axioms spoil the computational properties of a type system, as they are stuck terms under evaluation. But it's only just barely not a theorem. So there are a bunch of new type theories now (cubical type theories), which aim to restructure the rules of the type theory such that the univalence axiom becomes a result obtainable directly from the logical rules, and not an axiom. I'm not sure that a clear winner amongst those has fallen out of that yet, but there's a lot of promising work, and fairly practical systems at least from the perspective of a type theorist or computer scientist, if not the average mathematician.
For the average mathematician, there is some reasonable hope that research along these lines might provide a formal system that can actually be used, rather than merely thought about. Most proofs of modern mathematics are not formalised in the sense that a machine could check them, they're written in such a way where the intent is to convince other human mathematicians that a proof is formalisable in principle. To do otherwise while working under something like ZFC, or what is perhaps the real culprit, first order logic, would be not only 99.9% boring but also incredibly time-consuming. But at the same time, there's a lot of frustration that's happening with mathematics branching out into smaller and smaller areas, with the set of possible referees for some papers getting to the point that it can be hard to know whether to believe that things have been sufficiently checked.
There's some hope though that the fact that you don't have to repeat the proofs over and over for isomorphic things in HoTT, and that type theories in general are far more usable to begin with, might mean that an actually-ergonomic formal system for the average mathematician is within reach.
Will any of that affect how we think about artificial intelligence? Well, if the project to turn mathematicians on to computerised proofs is successful, it might help turn a larger fraction of mathematics into something that is more amenable to applying AI-based search to, and provide such AI systems with lots of worked examples of human mathematics.
HoTT and type theories in general, do have some apparent advantages when it comes to making it practical for humans to express proofs in a way which computers can understand, but the entire practice of that is not something which could be said to be extremely well-developed thus far, and so everything is to some degree a big experiment.
As a synthetic approach to homotopy theory, it's a beautiful piece of work, the latest approach in a line of approaches to that. You could say that HoTT is to traditional homotopy theory what axiomatic geometry (where lines are objects unto themselves) is to Cartesian geometry (where lines are collections of points). Homotopy theorists have built various abstractions for capturing that, and HoTT gives a very satisfying one.
As an informal foundations for thinking about mathematics, it's intriguing and certainly has some new ideas about how to approach the definitions of various familiar mathematical objects. Especially for the sorts of things that are normally defined using quotients, those come out looking quite a bit different, since rather than forming equivalence classes in the usual way, we can construct "higher inductive types" which guarantee certain "paths" or "proofs of equality" between particular points/terms, and come equipped with an "induction principle" for defining maps out of the type (or what is the same activity, proving properties about it), and which insist that we say where those paths are sent in the destination, basically guaranteeing that certain equalities-made-tangible are conserved.
Type theories generalise the propositions of logic and sets of set theory into what they call "types" and those types give each mathematical statement a kind of interpretation as a sort of collection of its own proofs, which was formerly usually thought of as a set. HoTT adds a kind of geometry to this set, putting paths between proofs that are in some sense "equal", and that construction can be iterated to give paths-between-paths (surfaces), and so on to higher dimensions.
HoTT shows us that we can divide the types of type theory into levels of which the first few are propositions, sets, and (categorical) groupoids.
I would say most of HoTT grew out of the consequences of noticing this interpretation of what was already a very beautiful and "natural" type theory (Martin-Löf type theory, MLTT) whose original intent was merely to serve as a foundations for mathematics. It gives that theory a more general model than it previously had and turns what from a purely logical perspective might have been seen before as quirky idiosyncrasies to be put up with in exchange for the other very nice theoretical properties of the system, into things which are geometrically obvious from the perspective of thinking about homotopy types of spaces.
Unfortunately, plain Martin-Löf type theory isn't quite adequate on its own -- there is a fairly natural axiom called the univalence axiom, that falls out as an expectation regarding this interpretation of types as homotopy types. It gives us the nice property that types which are in some sense equivalent (or isomorphic), have these "paths" between them, making them "equal" in a containing universe type. This immediately gives us the ability to transport theorems about one construction to another, which is formally not something that could be done in first order logic and set theory. Formally, you would have to prove the theorem again for each isomorphic thing, because first order logic has no way of knowing that mathematicians only allow properties that respect isomorphism in the first place.
This Univalence axiom is also a problem, however. Axioms spoil the computational properties of a type system, as they are stuck terms under evaluation. But it's only just barely not a theorem. So there are a bunch of new type theories now (cubical type theories), which aim to restructure the rules of the type theory such that the univalence axiom becomes a result obtainable directly from the logical rules, and not an axiom. I'm not sure that a clear winner amongst those has fallen out of that yet, but there's a lot of promising work, and fairly practical systems at least from the perspective of a type theorist or computer scientist, if not the average mathematician.
For the average mathematician, there is some reasonable hope that research along these lines might provide a formal system that can actually be used, rather than merely thought about. Most proofs of modern mathematics are not formalised in the sense that a machine could check them, they're written in such a way where the intent is to convince other human mathematicians that a proof is formalisable in principle. To do otherwise while working under something like ZFC, or what is perhaps the real culprit, first order logic, would be not only 99.9% boring but also incredibly time-consuming. But at the same time, there's a lot of frustration that's happening with mathematics branching out into smaller and smaller areas, with the set of possible referees for some papers getting to the point that it can be hard to know whether to believe that things have been sufficiently checked.
There's some hope though that the fact that you don't have to repeat the proofs over and over for isomorphic things in HoTT, and that type theories in general are far more usable to begin with, might mean that an actually-ergonomic formal system for the average mathematician is within reach.
Will any of that affect how we think about artificial intelligence? Well, if the project to turn mathematicians on to computerised proofs is successful, it might help turn a larger fraction of mathematics into something that is more amenable to applying AI-based search to, and provide such AI systems with lots of worked examples of human mathematics.