“The function x^2” isn’t a silent conversion between objects of different types. It’s really exactly one thing: the function x->x^2. It's just shorthand. Also

“The function x^2” isn’t a silent conversion between objects of different types. It’s really exactly one thing: the function x->x^2. It's just shorthand. Also note that intuitionistic type theory is only one kind of type theory. There’s nothing about assuming the existence of real numbers that implies you are not using type theory. Intuitionistic type theory is useful because computer programs must construct their values… the Curry-Howard correspondence is between the types system in a computer program and statements in intuitionistic logic.