univalent foundations wikipedia page

[Vladimir Voevodsky]

Hi,

I have started a few days ago the “Univalent foundations” page at wikipedia. So far it is almost entirely written by me. Please have a look and add something!

Vladimir.

[Bas Spitters]

I am surprised not to see the connection with higher toposes mentioned
at all. Is it intentional?
As you have been working on simplicial sheaves for years, I imagine
that this may have had some influence on your thinking.

Some of the ideas on higher toposes were there in Oberwolfach.
For me the project was perhaps most clearly outlined in Mike's courses in 2012:
http://home.sandiego.edu/~shulman/hottminicourse2012/
(Especially the very last slide of the last lecture)
Although it can also be found in section 3 of this paper by Steve (2010).
However, the precise connection with the UA is not mentioned there:
http://www.andrew.cmu.edu/user/awodey/preprints/TTH.pdf

From the analogy with the project to use toposes as a foundation for
(constructive) mathematics, some of the other ideas seem to follow. I
would point to:
https://en.wikipedia.org/wiki/Topos#Elementary_topoi_.28topoi_in_logic.29
in addition to the reference to Grothendieck who gave us both
Grothendieck toposes and oo-groupoids, but not the connection with
logic. Especially, it is not so clear to me how these relate to the
platonistic ideas of Grassmann and Cantor in the introduction.

> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Urs Schreiber]

On 12/13/14, Bas Spitters <b.a.w.s...@gmail.com> wrote:

> I am surprised not to see the connection with higher toposes mentioned
> at all. Is it intentional?

Curious that you say so, this still seems to be a well-kept secret
within the HoTT community. But Vladimir has made it quite clear that
he is not into higher toposes and abstract homotopy theory and would
rather have what he regards as his own, namely UF, be separated from
HoTT.

For instance in the remarkable message [1] he wrote:

> the name of the book as it stands is becoming a household name that overshadows the UF

and then described the situation as "painful" to him. Or in the very
message preceding the present thread [2] he wrote:

> Either we say as it really is that HoTT started with the construction of a univalent model of the Martin-Lof type theory by Vladimir Voevodsky in 2009 and move the stuff about abstract homotopy theory and Quillen model structures in a section describing one of the branches of HoTT or we remove any mention about proof assistants and formalization of mathematics from the page and I start distancing myself from HoTT.


I suppose that's precisely why Vladimir is now writing a Wikipedia
entry on his own project, in order to set the record straight. Not to
mention higher toposes would then be part of the whole point of this
page.

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.

This may be confusing and the public perceptionn is confused about
this. But Vladimir himself has complained most explicitly about this
confusion: he is not into HoTT as a topic in abstract homotopy theory
and higher topos theory.

Not only does he find this confusion painful, according to the above
messages, but I think it is clear that this confusion also has a
negative social effect on those fine young contributors to genuine
HoTT, whose names keep being overshadowed -- in the public but also
apparently in the experct community perception.

When the HoTT community more fully realizes and admits this state of
affairs, it might help the dynamics of both projects.


[1] https://groups.google.com/d/msg/homotopytypetheory/zEixM1M3ZDQ/m5eYwwfs0i8J

[2] https://groups.google.com/d/msg/homotopytypetheory/a3aTb0Fwagk/yzHaSALa5rMJ

[3] https://github.com/vladimirias/2014_Paul_Bernays_Lectures/blob/master/2014_09_Bernays_3%20presentation.pdf?raw=true

[Vladimir Voevodsky]

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.

For this see my Bernays lectures (linked at the page).

 am surprised not to see the connection with higher toposes mentioned
at all. Is it intentional?

So far the only connection to higher toposes is through Michael Shulman’s paper that is linked at the page. All other connections are, as far as I know, purely speculative. 

Vladimir.

[Vladimir Voevodsky]

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.

It would be more correct to say not “to truncate HoTT to hSets” but “to use only the hSets part of HoTT” but otherwise it is correct. 

While I consider the quest for “synthetic everything” to be fascinating I want to disentangle it from the fact that we can provide powerful practical tools for working mathematicians using the univalent formalization of sets and categories that is already available today. 

Vladimir.

[David Roberts]

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

[Michael Shulman]

On Sat, Dec 13, 2014 at 3:03 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> So far the only connection to higher toposes is through Michael Shulman’s
> paper that is linked at the page. All other connections are, as far as I
> know, purely speculative.

Some other known connections include:

* My other preprint "The univalence axiom for elegant Reedy
presheaves" (http://arxiv.org/abs/1307.6248), which has been accepted
for publication modulo revisions.

* 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).

* The recently posted Lumsdaine-Warren coherence theorem can be
applied to model categories based on localizations of the injective
model structure on simplicial presheaves. Any (oo,1)-topos, and
indeed any locally cartesian closed (oo,1)-category, can be presented
by such a model category; this was proven separately by Cisinski and
Gepner-Kock. Thus, any (oo,1)-topos admits a model of type theory
except possibly for universes, and one does always have "weakly a la
Tarski" universes. This construction is summarized at
http://ncatlab.org:8080/homotopytypetheory/show/model+of+type+theory+in+an+%28infinity%2C1%29-topos.

So there is a lot more known that is not just speculative.

Mike

[Vladimir Voevodsky]

> Thus, any (oo,1)-topos admits a model of type theory
> except possibly for universes,

This might be important for HoTT but has only a marginal interest for the UF.

In the type theories used in the UF, the universe is of primary importance and there are no base types.

In fact, in the “purist” version of the type theory that is used in the UF the universe is the only generating type.

Because of this fact the only models that have a direct relevance for the UF are the ones that include a univalent universe.

Vladimir.

[Vladimir Voevodsky]

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).

This is a very interesting claim that I do not quite understand. Cubical model is a collection of several sets with a bunch of partially defined operations. These sets are build from the set of sets of bounded size using various constructive operations. 

This model is used to construct an interpretation of the Martin-Lof type theory i.e. an interpretation of the syntax. 

In the topos you will first need this “set of sets”. This can be done if the topos is a Grothendieck topos. Then there will be a model in the topos i.e. an object of the topos with some operations on it.

But what does it have to do with interpreting syntax of the Martin-Lof type theory? For that we need a model in sets. Can we just take the sets of global sections of the objects that we have in the topos? 

Vladimir.

[Michael Shulman]

On Sat, Dec 13, 2014 at 4:42 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> But what does it have to do with interpreting syntax of the Martin-Lof type
> theory? For that we need a model in sets.

I don't know what you mean. Even the simplicial model is not a "model
in sets" but in some other category, namely simplicial sets. The same
notion of "model" that applies there applies to models in other
categories, such as cubical sets, simplicial objects in a topos, or
cubical objects in a topos.

[Vladimir Voevodsky]

Let me ask it in a different way. In the simplicial model the universe is interpreted as the Kan simplicial set of Kan simplicial sets (with the well ordering or with the Zermelo structure).

If I internalize the cubical model to a Grothendieck topos T, how will the universe be interpreted in this model?

Vladimir.

[Michael Shulman]

As the cubical object of cubical objects, obtained by carrying out the
construction of the cubical model's universe internally to T.

[Bas Spitters]

Mike, would you claim that the construction could be carried out in V_{w+w}?
I don't see how, but you may have a solution in mind.
V_{w+w} is one of the examples Thomas gives of a topos without a universe.
http://www.mathematik.tu-darmstadt.de/~streicher/NOTES/UniTop.pdf

[Bas Spitters]

I am trying to understand in broad terms the connection with the work
of Grassman.
Apparently, Lawvere sees it as a precursor to category theory.
Unfortunately, I seem to be unable to find a copy online.

Does anyone have more information about what is in this text?

Lawvere, Grassmann's Dialectics and Category Theory, Hermann Gunther
Grassmann (1809-1877): Visionary Mathematician, Scientist and
Neohumanist Scholar, Proceedings of the 1994 Conference to commemorate
150 years of Grassmann's "Ausdehnungslehre", Gert Schubring (Ed),
Boston Studies in the Philosophy of Science, 187: 255-264, Kluwer
Academic Publishers, (1996).

[Thomas Streicher]

> >> If I internalize the cubical model to a Grothendieck topos T, how will the universe be interpreted in this model?

Of course, one needs a universe in the topos. It certainly cannot be
done in V_{w+w} or the free (boolean) topos with a nno.
But most toposes of interest are heavily based on sets and they do
have universes as shown in my paper Universes in Toposes.

Thomas

[Thomas Streicher]

> Of course, one needs a universe in the topos. It certainly cannot be
> done in V_{w+w} or the free (boolean) topos with a nno.
> But most toposes of interest are heavily based on sets and they do
> have universes as shown in my paper Universes in Toposes.

Maybe a word of clarification is in place here. One can do
Grothendieck or realizability toposes or alike over more general base
toposes than Set. Usually it suffices to have an elementary topos SS
with nno as a base. Then these toposes over SS are constructed as
fibrations over SS from the fundamental fibration of SS (over SS). This
was done by Benabou in the 1970s and can be found e.g. in Celeyrette's
These. Avoiding fibrations speak it can be found in Johnstone's 1977 book.

But of course such Grothendieck toposes over an arbitrary base SS
(with nno) don't have universes since they have to be inherited from SS.

BTW Grothendieck would never have used the somewhat frivolous notation
Set as one finds it nowadays. He always would have replaced Set by
some Grohendieck universe since he never gave up set-theoretic foundations.
The somewhat naive notation Set was introduced - I think - when
elementary toposes came up around 1970. For a logician this notation
is a bit shocking becuase it is a confession of utmost naivit'e (Platonism).
Of course, it can always be cleaned up replacing it by some Grothendieck
universe. Or, when working over arbitrary bases, as a shorthand for
the fundamental fibration over the base.

Besides the many good things arising from topos theory started around
1970 I can't suppress that also some damage was done by an exaggerate
anti-logical attitude and by the neglection of the phenomenon of
universes which also was introduced about that time (by Martin-Loef)
but neglected by the topos people. The reason seems to have been that
set theory was considered as somewhat reactionary or otherwise
connected with the establishment. (But that's only an impression and
Andr'e can explain this much better!)

I am not saying that one shouldn't use Set as a notation but one
should be aware what it means (as discussed above). It's a metaphor
for using Groth. universes or the fundamental fibration. Of course, it
can also be understood as a metaphor for some other universe in a topos
which, however, should have enough closure properties.

Thomas

[Michael Shulman]

Yes, of course one needs a universe in a 1-topos in order to obtain a
universe in a higher topos constructed from it. I was thinking of
Grothendieck 1-toposes.

[Vladimir Voevodsky]

The main source is:

A New Branch of Mathematics: The Ausdehnungslehre of 1844
• by

• Hermann Grassmann,
• Lloyd C. Kannenberg (Translator),
• Lloyd C. Kannenberg (Editor)


Unfortunately I was able to find an electronic copy of it. There is an electronic copy of the main text in German.

Vladimir.

[Bas Spitters]

Interesting. Lawvere [1] seems to have found the following ideas in
the same text by Grassmann:
- a precursor to adjoint functors and
- an interpretation of Grassmann's "Becoming according to a simple law
of change" as an equation which is naturally interpreted in affine
categories. Lawvere connects this last point to the `laws of becoming'
(dynamical systems). http://ncatlab.org/nlab/show/becoming

It is unclear to me whether or how these ideas connect to your reading
of Grassmann.

[1] Lawvere, Grassmann’s Dialectics and Category Theory
http://link.springer.com/chapter/10.1007%2F978-94-015-8753-2_21