[FOM] New umbrella?

Paul Levy P.B.Levy at cs.bham.ac.uk
Sun Nov 2 10:18:12 EST 2014

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  

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 Blain Levy
School of Computer Science, University of Birmingham
+44 121 414 4792

More information about the FOM mailing list