[FOM] New umbrella?

[Paul Levy]

So to summarize your argument, every time I prove a theorem in HoTT, I  
know that I have proved *something* about sheaves on an arbitrary  
infinity-site.

But in order to find out *what* I have proved, I have to work out, in  
all its "tedious" detail, the semantics of my theorem.  (Though not, I  
grant, of its proof, and any lemmas involved, since that is all  
covered by the soundness property.)

If I'm genuinely interested in the properties of sheaves on an  
infinity-site, I have no choice but to perform this latter step.

And if, on the other hand, I'm not interested in these sheaves, then  
the argument you presented can't convince me to use HoTT.

Paul


--
Paul Blain Levy
School of Computer Science, University of Birmingham
+44 121 414 4792
http://www.cs.bham.ac.uk/~pbl