oneestrong

I don't know anything about homotopy types, but I think that they are trying to build a system in which automated proofs can be computed more easily. So the appeal is for applying computer methods for proofs. Also it tries to use the language of homotopy to suggest that some ideas category theory and homotopy theory can be translated to see if they give a new perspective of old problems. I don't know if the road to computer proofs via homotopy types is going to give fruits or not, but I think it should be tested in that field: creating computer proofs for theorems. https://math.stackexchange.com/questions/1158383/examples-of...

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.