the audience here tends to have more of a Computer Science background rather than a traditional Mathematics background, and HoTT feels more like a CS theory than like traditional math. When I read about the kind of reasoning that lead to ZFC, I get frustrated because that style of thinking feels unnatural to me. HoTT feels more like how I think, when I’m trying to solve problems. Not that I could productively do math research in either system - I’m not a mathematician at all! It’s just an aesthetic judgement.