Me too bud. But I think it's something I should try approaching once I've given category theory a solid try. As I understand it, Homotopy Type Theory (HoTT) / U

Me too bud. But I think it's something I should try approaching once I've given category theory a solid try. As I understand it, Homotopy Type Theory (HoTT) / Univalent Foundations is a way of building up a theory of mathematics from type theory.