Interesting, do you think these ideas will have applications in CS ?<p>I mean type theory is obviously useful, both to things like formal proofs and the definition of typed languages but do you think that thinking of types in terms of topological spaces and homotopy will lead to new insights in these or related areas ?