4 ms·

Well, it is a start. Fourteen pages anyone? Once we are down to five pages I'll give it a(nother) shot.

• agumonkey 9y ago
  you should read it, it's an easy one, at least it's how I feel after reading 3 pages (usually I stop long before that)
  • dvt 9y ago
    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).
• oneestrong 9y ago
  In example 2.2, to distinguish between an element and a function a better example is to consider a constant such as 7 can be an element of R or a constant function. With type theory notation, 1:R versus \x:R.1, another important point is that you have to specify the arity of the function, so that 1:R, \(x:R).1, \(x:R,y:R).1, \(x:C,y:C).1 are four different types, the first a constant, the second a constant function of one real variable, and the last a function of arity two whose variable type is the C the complex field. I'm reading page four, perhaps type theory can distinguish among pure function, lazy functions, side-effect functions and other types of functions that are implemented by a procedure which can be lazy or not. So pi:R,(\x:R.pi) and (\x:Haskell-Action()).pi in which the last is a non pure lazy program for computing all digits of pi, are two different types, that is they belong to different universes.