I feel obliged to point out that HoTT is… really rather abstract. I'm just starting to learn about it now in my spare time, and I hold a master's degree in mathematics specialising in logic.