[FOM] HoTT as foundations: a short account

[Paul B Levy]

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