[amathstudent]

I'm curious - can anyone point me to an overview/exposition of this that is more hand-wavy than the book? I'm interested understanding the ideas in this work, because proofs as objects would be a major step forward, but I don't even know much about the existing systems of foundations (ZFC etc), nevermind type theory...

[sjy]

Did you read the Introduction from pp1-12 of HoTT? I thought it was a pretty good overview.

[amathstudent]

I tried. I was hoping for something more like: "a field is something you can add, subtract, multiply, & divide in" and less like: "a field is a set that is a commutative group with respect to two different operations (excepting 0), linked by the distributive law".

I need something to hold on to when reading the more formal treatment.

[tel]

I highly suggest Robert Harper's lectures from the Oregon Programming Languages Summer School. I watched the OPLSS'12 lectures, but I'm sure they're great any year.