It's not bad, but man the way the author throws around multivariate (e.g. non-curried) functions all over the place is sooo confusing. I remember reading a λ-ca

It's not bad, but man the way the author throws around multivariate (e.g. non-curried) functions all over the place is sooo confusing. I remember reading a λ-calculus book that would do that and it's really not fun to try and parse (see the bottom of pg. 7). But I will say it's very cool to see how HoTT derives all the basic tools you'd use in propositional calculus (A: A -> A, :(A -> (B -> C)) -> ((A->B) -> (A->C)), and so on).