[SomeStupidPoint]

My background may be showing, but it may be hard to appreciate HoTT without understanding the role of homotopies in topology. My (limited) understanding of the material is that it's an attempt to introduce a homotopy structure on the type system, and then use that to talk about logical equality (mumblemumble) being the same as homotopy equivalence.

It's then using that equivalence structure between the proofs to reason about constructing proofs, as you can reason about the constructions that are possible out of classes of proofs. And that's basically where I get lost, because I don't quite know enough type theory to understand the structure they're trying to build, so I can't quite get the specific motivations. (The obvious high-level one is better formal reasoning.)

I haven't been following HoTT super closely for a year or two, getting sidetracked into the background, but last I checked there wasn't a ton of simple material on it -- it was sort of read the book, read the Coq proofs/framework, and figure it out. (Though, this easily could have changed.)