[FOM] formal proofs

[Urs Schreiber]

On 10/21/14, Timothy Y. Chow <tchow at alum.mit.edu> wrote:
> Urs Schreiber wrote:
>
>> A good example of this is the formal proof, in HoTT, of the
>> Blakers-Massy theorem
>> (http://ncatlab.org/nlab/show/Blakers-Massey+theorem) by Lumsdaine,
>> Finster and Licata. The full formalization is here:
>>
>> https://github.com/dlicata335/hott-agda/blob/master/homotopy/BlakersMassey.agda
>>
>> I'd think that with traditional foundations even stating this theorem
>> formally is impossible for all practical purposes, let alone formally
>> checking its proof.
>
> This is a nice gauntlet!  Before a traditionalist embarks on a project to
> refute this claim, let me clarify what is at stake.
>
> Question for Urs: Suppose a traditionalist were to thoroughly refute your
> claim above.  Would that "score any points" for the traditional side in
> this debate?  Or is this just a casual remark on your part, which if
> refuted would not cause you to change your mind on any substantive issue?


This was not a casual remark, this was a reply to the question that
has been repeatedly asked here, as to what the point of homotopy type
theory is.

It had been mentioned here before that homotopy type theory [1] offers
some advantages for formal set-based mathematics, such as providing
quotient types and isomorphism invariance. What seems not to have been
mentioned much before here is that the key point of homotopy type
theory however is that it goes way beyond this in that it provides a
native (i.e. direct, synthetic, see below) formalization not just of
constructive set theory, but of homotopy theory [2] (aka algebraic
topology). And the neat thing is: of homotopy theory in its modern and
most powerful incarnation in the guise of infinity-toposes [3].

Just like plain dependent type theory is the internal language of
locally cartesian closed categories, so homotopy type theory is the
internal language of locally cartesian closed infinity-categories, and
homotopy type theory with univalent type universes is the internal
language of infinity-toposes [4, 14]. This means that homotopy type
theory provides a "structural" foundation of the kind that William
Lawvere had found in topos theory [5], but refined to homotopy theory
in the refined guise of infinity-topos theory.

My statement that the mathematics of homotopy theory and algebraic
topology is beyond the scope of what may practicably be implemented in
tradtional set-based foundations was not meant to be provocative.
Looking at the mathematics that has been implemented in set-based
foundations over the years [6] and extrapolating this progress into
the future, it seems uncontroversial to me that the formalization of
just the basics of simplicial homotopy theory [7] and higher topos
theory [8] in traditional set-based mathematics is prohibitively
tedious, and that using traditional set-based mathematics to engage in
the formalization of proof of theorems of practical interest in these
fields is out of the question, not in principle of course, but for all
practical purposes.

And yet, homotopy type theory natively knows about all this.

For instance the formal proof [9] of the Blakers-Massey theorem [10]
does not need to begin by first formalizing what a simplicial set is,
what a Kan fibrancy condition is, what the infinite tower of homotopy
groups is, what weak homotopy equivalences are, what homotopy pushouts
are, how they reflect in long exact sequences of homotopy groups;
because all this is native to homotopy type theory. Accordingly, the
proof [9], on top of being a formal proof, is elegantly transparent
and of actual practical interest. Moreover, since the formal HoTT
proof [9] generalizes the traditional statement to more general
infinity-toposes, it is actually a genuine new mathetical result of
genuine interest in modern homotopy theory, to practicing
mathematicians not concerned about foundations. This seems to be a
kind of achievement unheard of [6] within the traditional
formalization of set-based mathematics.

The reason why this may happen with homotopy type theory, the reason
why homotopy type theory provides not just any but provides a
practical foundation for mathematics including modern homotopy
theory/algebraic topology, is that it provides a "synthetic" language
for these topics, which allows to formally speak about the basic
concepts natively without the need to first formalize several
textbooks worth of material starting from bare set theory to even get
started.

To my mind these are statements of the obvious to anyone who looked
into the matter. The fact that they are not more widely appreciated is
not due to this being possibly controversial, I believe, but because
the intersection of the sets of researchers who genuinely appreciate
modern homotopy theory in the guise of higher topos theory and those
who appreciate formal logic, type theory and what it means to have an
internal language of a higher topos is very small.

Indeed, also various of practitioners homotopy type theory care only
about the truncation of the theory down to set theory, to "hsets"
[11]. The crucial relation of homotopy type theory to higher topos
theory was Steve Awodey's vision [12]. It has been realized notably by
Mike Shulman [13,14], Peter Lumsdaine [15] and others and deserves to
be more widely known.

Mike Shulman's 2012 course notes [16] are possibly still the best
introduction on this matter. Anyone trying to get an idea of what the
point of homotopy type theory is as a new practical foundation for
modern high-level mathematic rooted in homotopy theory and higher
topos theory could do worse than starting with these notes.


[1] http://ncatlab.org/nlab/show/homotopy+type+theory
[2] http://ncatlab.org/nlab/show/homotopy+theory
[3] http://ncatlab.org/nlab/show/(infinity,1)-topos
[4] http://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory
[5] http://ncatlab.org/nlab/show/ETCS
[6] https://plus.google.com/+UrsSchreiber/posts/YS6asZLgbbj
[7] http://ncatlab.org/nlab/show/Simplicial+homotopy+theory
[8] http://ncatlab.org/nlab/show/Higher+Topos+Theory
[9] https://github.com/dlicata335/hott-agda/blob/master/homotopy/BlakersMassey.agda
[10] http://ncatlab.org/nlab/show/Blakers-Massey+theorem
[11] http://ncatlab.org/nlab/show/set+theory#ReferencesInHomotopyTypeTheory
[12] http://ncatlab.org/nlab/show/homotopy+type+theory#Awodey
[13] http://ncatlab.org/nlab/show/homotopy+type+theory#Shulman12
[14] http://ncatlab.org/homotopytypetheory/show/model+of+type+theory+in+an+(infinity,1)-topos
[15] http://ncatlab.org/nlab/show/higher+inductive+type#ShulmanLumsdaine12
[16] http://ncatlab.org/nlab/show/homotopy+type+theory#ShulmanCourse