On Dec 13, 2014, at 6:06 AM, Bas Spitters <b.a.w.s...@gmail.com> wrote:Especially, it is not so clear to me how these relate to the
platonistic ideas of Grassmann and Cantor in the introduction.
am surprised not to see the connection with higher toposes mentioned
at all. Is it intentional?
On Dec 13, 2014, at 6:16 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:Also observe slide 11 of the Bernays lectures [3]: given what you say
one might think that an approach true to the spirit of HoTT would be
to try to find synthetic axioms characterizing the infinity-topos over
the Nisnevich site and then proceed to formulate A1-homotopy theory
synthetically from there. But this is not at all what Vladimir is
after, according to this slide. Instead of making use of the synthetic
homotopy theory intrinsic to HoTT, his proposal is to truncate HoTT
down to hSets and then re-formalize whatever it takes in the resulting
set-theoretic mathematics.
Regarding proving things synthetically versus 'analytically' from the hSets, one could envisage a formal proof in eg Coq using the latter as being accepted more easily by the wider mathematics community. The recent discussion on the fom mailing list around Blakers-Massey in Coq highlighted the attitudes some might have towards synthetic proofs of facts originally proved about objects built out of sets.
Best,
David
On Dec 13, 2014, at 7:06 PM, Michael Shulman <shu...@sandiego.edu> wrote:The constructive cubical model can be carried out internally to any
1-topos. As far as I know no one has worked out exactly what higher
category the resulting semantics live in, but it ought to be a sort of
"higher exact completion" of the original 1-topos. (Similarly, your
original model in simplicial sets can be carried out internally to any
1-topos that satisfies AC).