Re: Grothendieck toposes

[Steve Vickers <s.j.vickers@cs.bham.ac.uk>]

On 03/11/2016 08:45, Patrik Eklund wrote:
> ...
>
> PS Why not also try something out about the empty type. The only thing
> in mathematics that axiomatically is, not just exists, but is, is the
> empty set, and then we put brackets around, and create natural
> numbers. From natural numbers we then create everything else in
> mathematics. Couldn't the empty type be something similar? But we
> shouldn't lean on the HoTT community because they don't comply with
> mathematics in their HoTTematics. They are two dofferent worlds. Set
> theory is untyped, so math is weak on types.
Dear Patrik,

You're too embedded in the world-view that maths is set theory.

It is a miracle* that maths could be built up from the empty set using
just axioms for collections, so that every mathematical construct is a
set of sets of sets of ... .

A century later, some of us look back on the miracle of set theory and
try to appraise it with the benefit of more hindsight.

Actually, maths is _strong_ on types. We implicitly use types all the
time. If we talk about natural numbers, we don't assume any particular
way of _constructing_ them within set theory. We work with rules _using_
them, and that is a type-theoretic standpoint.

If set theory is weak on types (and it is), then that is showing the
limitations of set theory, not that in some way "HoTTematics" doesn't
comply with mathematics.

All the best,

Steve.

* Apologies to Marta here: but a miracle is just something to be
marvelled at because you'd previously thought it impossible, right?
Minor miracles are the stuff of life, since our rationality is never
complete enough to know for sure what's possible and what's not. In
mathematics we can see just from the historical evidence that Bishop's
constructive analysis was a miracle. Toposes are a miracle - in fact
topologists still think it's impossible, or they would have changed
their definition of topology. And I think elementary topos theory is a
bit of a miracle too - that the infinitary constructions inherent in
topology can be captured in finitely axiomatizable systems.


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]