[FOM] HoTT as foundations: a short account
Paul B Levy
P.B.Levy at cs.bham.ac.uk
Mon Oct 27 12:24:33 EDT 2014
Dear all,
Following the previous days' discussion I've become more sympathetic
toards HoTT. Here is a brief account of what, in my view, HoTT offers
as a foundation of mathematics (rather than as a theory of homotopy, or
infinity-toposes, or whatever).
--
In traditional foundations, one can construct an endofunction
on the universe of sets that is not functorial on bijections. For
example: the function that sends {{}} to itself and every other set to
the empty set. Such a function is sometimes described as "evil",
in the sense that the two singleton sets {{}} and {{{}}}, differing only
in their implementation, are treated in different ways.
In ordinary mathematical practice, including category theory, we rarely
(I hesitate to say "never") consider such functions. The things that we
do to sets are usually independent of their particular implementation.
That means that mathematicians usually work in a special fragment of
traditional set theory in which it's impossible to define functions such
as the above function. To date, this fragment has not been precisely
defined (I think).
HoTT is a radically different foundation that takes this idea much
further. Not only is it impossible to construct functions like the
above, but we can actually prove a theorem: "every endofunction on the
universe of sets is functorial on bijections". One may debate whether
such a theorem is desirable, and it's obviously impossible in any
fragment of traditional set theory. But let's assume we do want it, and
consider what kind of conceptual framework we need in order to get it.
The basic concept is that of "type". For example, there is a type of
natural numbers, a type of sets, a type of categories and so forth.
(These examples have different size but I am ignoring that issue.) The
domain of a function will always be a type.
What we need to know about a type A is not just what its elements are.
We also need to know, for any two elements x and y, what ways there are
of identifying x with y. These "ways of identifying" must be respected
by any function with domain A, and they form another type, called id_A(x,y).
Here are some examples.
(1) If A is the type of natural numbers, there is just one way of
identifying x with y if x=y, and none otherwise.
(2) If A is the type of sets, then a way of identifying x with y is a
bijection.
(3) If A is the type of categories, then a way of identifying x with y
is an adjoint equivalence.
(4) HoTT also provides "higher inductive" types, where the elements and
the ways of identifying them are freely generated in some way.
If f is an endofunction on the type of sets, then the assumption that f
respects the ways of identifying means that it is functorial on
bijections. And that, very roughly, is how HoTT, a theory that embodies
these notions of type and function, allows us to prove our desired theorem.
Paul
--
Paul Blain Levy
School of Computer Science, University of Birmingham
http://www.cs.bham.ac.uk/~pbl
More information about the FOM
mailing list