I am too dumb to even know what this is ... even after looking at it.

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.

I know plenty of mathematics yet the introduction is not very helpful to someone new to category theory, only someone new to homotopy.