Re: [HoTT] doing "all of pure mathematics" in type theory

[Michael Shulman <shulman@sandiego.edu>]

In my opinion there are several separate issues standing in the way of
a wider use of proof assistants.  One has to do with the design of the
underlying formal systems.  In this respect Book HoTT (the formal
system of the homotopy type theory book, with univalence and higher
inductive types added in an "ad hoc" way on top of intensional
Martin-Lof type theory) is a step forward over systems such as CiC and
MLTT on which Coq and Agda are based, due to various factors such as a
nice treatment of quotients, automatic isomorphism-invariance,
inductive and free constructions, etc.

However, Book HoTT is also a step backwards, because the presence of
non-computational "axioms" means that "execution" gets stuck whenever
you try to use univalence.  So you can prove automatically that
anything true about a group G is true about an isomorphic group H, but
if you then try to take some specific statement about some specific
group G and transfer it to a specific statement about a specific group
H along a specific isomorphism, what you'll get will be an unreadable
statement littered with explicit transports across univalence-induced
paths in the universe, rather than the "real" statement about H that
should be obtained from actually *applying* that specific isomorphism.
(To be fair, plenty of people using a system like Coq pre-HoTT had to
add their own axioms, such as function extensionality and UIP, and
when you want classical logic that's unavoidably an axiom.  But at
least the underlying type theory of Coq and Agda can "compute".)  More
modern homotopy type theories, which are generally based on cubical
structures, allow univalence to be "executed" by the system.  However,
these systems lack (so far) all the intended categorical semantics
(see below), and haven't yet been implemented in "real world" proof
assistants (though there are prototypes now in use and development).

In addition, as Noah mentioned, two-level theories with a stricter
kind of equality (which do *not* exist in UniMath, HoTT/Coq, or
HoTT/Agda -- this point is about having two different equalities on
the same type, not two different classes of types with different
equality behavior) are likely to make many things easier, but haven't
been implemented in real-world proof assistants either (apart from
some sneaky coding with typeclasses).

So overall, I would say that the underlying design of homotopy type
theories is not yet "in order" to achieve its hoped-for maximal
benefit in a proof assistant by the working mathematician, though
there are promising signs and progress is being made.

All the issues discussed above are what I would call "mathematical",
or perhaps more broadly "theoretical".  But a separate issue standing
in the way of wider use of proof assistants is what I would call
"engineering".  No matter how fancy we make the underlying formal
system, I believe it will always remain true (for the foreseeable
future) that a proof assistant needs a lot more detailed information
than an ordinary mathematician would care to provide, or need to see,
in writing and understanding a proof.  This is where we need things
like tactics, implicit arguments, elaboration, proof automation, etc.
to fill in the gaps and make the system usable in practice.  Here
there's been a lot of progress over the past decades, but I think
there's a long way to go too, and choosing a better underlying
foundation (like any form of HoTT, cubical or otherwise) may improve
things a bit but is not really a game-changer.

However, there's something completely different that I do believe has
the potential to be a game-changer.  There's already a very different
"gigantic wave crashing through mathematics": homotopy theory and
higher category theory.  Homotopy type theory gives type theory and
formalization the potential to ride that wave.  The real point here is
that when something is formalized in type theory -- constructively --
it is automatically true internally in all models of type theory, and
for homotopy type theory those models include higher categories.  Note
that the use of constructive logic has nothing to do with any
philosophical belief; classical logic can still be "true" in the "real
world", and yet constructive reasoning is valuable because it makes a
theorem true internally in more categories.

I think it's fairly hopeless to convince a classical mathematician
that they should put in a lot of work to convince a computer of the
truth of *something they already knew*.  But I have much more hope of
convincing them that they should tweak their proofs slightly, and
perhaps use a computer to help verify the validity of the tweaks, in
order that *essentially the same proof* will allow them to conclude a
*vastly more general theorem*.  Moreover, when working with higher
categories the advantage is even more pronounced, because homotopy
type theories introduce a totally new kind of proof that can be much
simpler than all the previously available options -- and the immediate
feedback involved in using a proof assistant is one of the best ways
to *learn* that style of proof.

In short, I think there's a huge public relations opportunity here for
type theory and computer formalization, which sadly even Voevodsky
missed out on.  Rather than selling it as a way to be absolutely sure
of proofs we already believe in (as important as that might be), we
should sell it as a framework for *entirely new proofs* that bring the
otherwise fiendishly complicated and technical world of higher
category theory "down to earth".  The experts in higher category
theory are familiar with the fact that in many respects it is "more
natural" and "better behaved" than ordinary category theory; but there
are thick barriers to entry preventing many of us from getting to that
point of expertise.  With synthetic mathematics in homotopy type
theory, we can envision one day teaching higher category theory to
undergraduates.

-- 
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQx_b2QkEL-HqMXQNJ_QA83KjdAnFe7RmmiPRRQX6tYk-A%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.