[FOM] New umbrella?
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