Certainly not to the synthetic homotopy theory branch with which we communicate all the time.

I refer to mathematicians who do not know type theory and want to have a convenient language of working with what we would call structures on types of higher h-level. 

For example, there are people like that in the geometric representation theory. 

They don’t take us seriously so far because we can not define (infty,1)-categories. As soon as we find a language that can be used to define them and work with them directly without going through sets they will all start to turn their heads in our direction.

And this is a necessary pre-condition for talking seriously about the UF as a new foundation of mathematics. 

Vladimir.





On Jun 3, 2016, at 5:12 PM, Andrew Polonsky <andrew....@gmail.com> wrote:

Dear Vladimir,

We are also isolated from many and many mathematicians who are trying to find a way to express ideas that in my opinion are most naturally expressed in the UF in various theories formulated inside the set theory.

In this paragraph, are you referring to what Martin called "synthetic homotopy theory/infinity-toposes" branch of the HoTT community, or to a disparate body of mathematical research with different objectives?

Greetings,
Andrew