Morphoid Type Theory is a type theoretic foundation for mathematics that provides a notion of isomorphism at every type in correspondence with the standard notions of isomorphism in mathematics.

I have also written a blog post on why I believe that this is relevant to AI.