Does HoTT Provide a Foundation for Mathematics? by James Ladyman (University of Bristol, UK)

Talk at: FOMUS 2016. For all Talks and more information, slides etc. see: fomus.weebly.com/
Does HoTT Provide a Foundation for Mathematics? by James Ladyman (University of Bristol, UK)
Abstract: Homotopy Type Theory (HoTT) is a putative new foundation for mathematics grounded in constructive intensional type theory, that offers an alternative to the foundations provided by ZFC set theory and category theory. This paper explains and motivates an account of how to define, justify and think about HoTT in a way that is self-contained, and argues that so construed it is a candidate for being an autonomous foundation for mathematics. We first consider various questions that a foundation for mathematics might be expected to answer, and find that the standard formulation of HoTT as presented in the `HoTT Book' does not answer many of them. More importantly, the presentation of HoTT given in the HoTT Book is not 'autonomous' since it explicitly depends upon other fields of mathematics. In particular, an important rule for the treatment of identity in HoTT is path induction, which is commonly explained by appeal to the homotopy interpretation of the theory’s types, tokens, and identities as (respectively) spaces, points, and paths. However, if HoTT is to be an autonomous foundation then such an interpretation cannot play a fundamental role. We offer a derivation of path induction, motivated from pre-mathematical considerations, without recourse to homotopy theory. We use this as part of an alternative presentation of HoTT that does not depend upon ideas from other parts of mathematics, and in particular makes no reference to homotopy theory (but is compatible with the homotopy interpretation), and argue that it is a candidate autonomous foundation for mathematics. Our elaboration of HoTT is based on an interpretation of types as mathematical concepts, which accords with the intensional nature of the type theory.
This workshop was organised with the generous support of the Association for Symbolic Logic (ASL), the Association of German Mathematicians (DMV), the Berlin Mathematical School (BMS), the Center of Interdisciplinary Research (ZiF), the Deutsche Vereinigung für Mathematische Logik und für Grundlagenforschung der Exakten Wissenschaften (DVMLG), the German Academic Merit Foundation (Stipendiaten machen Programm), the Fachbereich Grundlagen der Informatik of the German Informatics Society (GI) and the German Society for Analytic Philosophy (GAP).

[@rogierbrussee3460]

There is a mathematically very important distinction between A and B are isomorphic and A and B are _uniquely_ isomorphic. In mathematical practice, one can only safely identify two structures, if the isomorphism between A and B is unique. The non uniqueness of isomorphisms is in fact easily detectable: the group of self isomorphisms (automorphisms) of A is non trivial. This is already apparent for basically the simplest mathematical object: the Booleans. As a finite set the booleans is just two element set and it is manifestly has a automorphism T F. However as a Boolean algebra, it no longer has an automorphism and it is unique, and it is completely harmless to change its representation (in fact this actually done in practice: in most computer hardware a boolean is represented by F 0 , T 1 but in some others it is represented by F 0 T ~0 = 0b111111...111 = -1).

[@K1indar0]

I got lot at 17:45. Not having been introduced to dependent types, this "path induction" device is quite impenetrable.

[@peterwaksman9179]

Mathematicians are getting further away from the foundations of mathematics, not closer. Does an infinity groupoid explain the difference between cardinals and ordinals?

[@3a146]

Oh of course, cardinal is a truncation, while ordinal is a simulation. See TUF Program 2013, sec10.2, 10.3. You can take truncation and simulation either verbally or formally, just don’t mix.

[@dialecticalmonist3405]

"Internal / External" is far more comprehensible than "propositional" or "logical".
For example, I have no idea what a "proposition" is supposed to mean as a function of math or semantics. I have a very clear idea of how "internal" is relatable to "external". That has a dualistic notion (structural), whereas "proposition" is a circular, abstract term, and "logic" only concerns consistency, not meaning.
The reason so many people hate math, is because mathematicians are horrible at conveying meaning and are very poor thinkers overall in the modern day.
Math is a LANGUAGE. Nothing more. It is not some devine idea.
Logic is a language too.
It is a language with the same intuitions and assumptions of any other language.
He is trying to explain the MEANING of ideas. That is what a philosopher should try to do.

[@3a146]

I am from a physics background and empty space/inhabited space is what works for me.

[@JosiahWarren]

Sorry this is unwatchable. I stoped watching after you keep using the term token to describe the term term. Term is the right term for term for god sake. Dont get me started about witness

[@CrucialFlowResearch]

It's really not that big of a deal to say token instead of term