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/ ]