It’s not exactly easy reading but take a look at Homotopy Type Theory w Univalent Foundations which is free online.