[FOM] Friedman/Baez/getting HOT

[François Dorais]

Dear Sam,

On Tue, Apr 12, 2016 at 8:44 AM, Sam Sanders <sasander at cage.ugent.be> wrote:

> Hence two questions:
>
> a) What makes HoTT different from constructive/recursive math, i.e. why
> will enforcing a given paradigm not lead to more complicated theorems this
> time around?
>

I've been puzzled by this too. Here is what I observed through
experimentation.

First, there is one important issue. Homotopy type theory permits both
classical and intuitionistic logic. (As far as I know, it's still unclear
whether univalence is a constructive principle.) In the intuitionistic
setting, all the usual issues arise. Perusing the HoTT Book, you will find
lots of the usual discussion of constructive issues: Cauchy reals vs
Dedekind reals, limited omniscience, etc. So the usual constructive baggage
you describe does arise in homotopy type theory, but these issues arise in
typical ways so there is nothing new here. In the following, I will assume
classical homotopy type theory: with excluded middle for propositions and
the axiom of choice for sets. (Note that excluded middle and the axiom of
choice for all types are inconsistent with univalence, so the restriction
to propositions/sets is essential.)

First, the motto “isomorphic objects are identified” is correct though
perhaps misleading. To interpret this one must realize that identity types
in homotopy type theory are very rich, so "identified" means something more
complex than the usual binary equal/not-equal. (One should really say
"equivalent" rather than "isomorphic"; these two concepts are very close
but subtly different.) The expression A = B in homotopy type theory is a
type, which could be empty, have just one element, have several
distinguished elements, or even more complex structure. On its own A = B
doesn't say much (translated in set-theoretic language it's closer to {0 |
A = B} than it is to A = B). To assert that A and B are identified, one
must take a 'path' p : A = B. This path p not only an identification of A
and B but a means of translating anything about A into a corresponding
thing about B and back. This is process is known as 'transport' and the
tools to handle this in homotopy type theory are sophisticated.

To start with a simple example, for the two-point set 2 (with two
inhabitants 0,1 and no nontrivial identifications between them) the
identity type 2 = 2 has two elements: "refl", the identity isomorphism, and
"swap", the isomorphism that exchanges 0 and 1. Thus 2 = 2 is a two element
type and it is a type in the same way that 2 is a type. This leads to funny
looking expressions like 2 = (2 = 2), 2 = (2 = (2 = 2)) and so on, each of
which is a two-element type and therefore all "true" since they all
inhabited. When one considers constructs involving 2, say the type A^2 of
pairs from A coded as functions with domain 2, the path p : 2 = 2
transports to the two natural identifications A^2 with itself: the identity
and the one that exchanges the two elements of the pair.

Another simple example are the coproducts 1+2 and 2+1. These are different
on the definitional level but they are obviously the same underlying
three-element type. These can still be recognized as different since the
definition is what one "literally sees" but they can be identified in six
different ways. So the identity type 1+2 = 2+1 has six paths, which are
definitionally different and they cannot be identified by paths between
them. The difference with 2 = 2 is that there is no longer a canonical
choice like refl to identify the two types. The choice of a path p : 1+2 =
2+1 forces us to pay attention to exactly how these two types are
identified. This is sometimes important but often swept under the rug. This
is a burden in the latter case, but the fact that paths are actual objects
on the same level as elements of 1+2 and 2+1 allows us to generalize over p
in the same way we do other objects. So when the choice of path p : 1+2 =
2+1 is not relevant, we can leave p unspecified, which is similar to the
common device of "leaving implementation details to the reader".

Another example (which occurs quite a lot in our common research areas) is
a choice of pairing function N^2 -> N. This is just a path p : N^2 -> N and
transport along this path can be used to transport from the graph of a
function N -> N to its code as a subset of N, for example. In this case,
the language used in homotopy type theory is roughly equivalent, though it
is very common practice to sweep coding details under the rug. So, because
of our collective "laziness", it does seem that the use of paths would
cause some additional burden. However, with the automated tools that
homotopy type theory provides to handle paths, the additional burden would
seem less than what is currently being swept under the rug.

In many practical cases, the paths don't pose any additional burden since
they are actually the objects we care about. For example, the fact that
S_5/A_5 is isomorphic to Z/2Z is simply stated as the assertion that
S_5/A_5 = Z/2Z is inhabited by a path. The usual proof of such a fact
consists in constructing an isomorphism between the two groups, which is
the same task as constructing a path p : S_5/A_5 = Z/2Z in homotopy type
theory. So in this case, working in homotopy type theory simply means a
change in language not a change in substance. The additional transport
tools from homotopy type theory have some extra applications. As a
(trivial) example of transport, the fact that Z/2Z is commutative is
immediate from the fact that Z is commutative, this argument doesn't work
for S_5/A_5 since S_5 is not commutative, but we can transport
commutativity from Z/2Z to S_5/A_5 along the path p^-1. Of course, such
transport arguments are already done without the additional tools of
homotopy type theory but I appreciate the fact that homotopy type theory
provides a formal and automated language for ideas that are usually just
tacitly understood.

It is my understanding that there are some areas of mathematics, such as
homotopy theory, where the identification paths of homotopy type theory are
of fundamental importance and the additional tools for handling paths are
of great utility and substantially simplify much of the work.
Unfortunately, I am not familiar enough with such examples to measure this
effect. While one can claim that homotopy type theory was tailor made for
such areas, one can still speculate that the availability of these new
tools may prompt new discoveries and may eventually prove to be very useful
in unexpected areas of mathematics.

As these simple examples illustrate, paths do pose an additional burden
when working in homotopy type theory. However, this is mitigated by the
fact that in many cases, the burden is simply a different way to express
what is already being done. There are cases where this may lead to
additional complexity, but the highly automated tools for handling paths
seem to ease some of the burden. There are further cases where the paths
and the associated tools are genuinely useful. It's still to soon to say
whether or not the paths in homotopy type theory cause additional burden
for 'general mathematics'. My experiments suggest that the additional
burden is not overwhelming. Proponents of homotopy type theory have
developed many natural language phrases that accurately translate formal
type theoretic statements and appropriately deemphasizes the least relevant
aspects of the path luggage. From what I've seen, the natural language
homotopy type theory analogue of a statement is usually very close and
often identical to the original natural language statement. It does,
however, take some time to get familiar with the subtleties of meaning in
this language.

Let me mention a few additional features of homotopy type theory that, I
think, can help clarify the nature of identity types. One key feature of
univalence is that it leads to a rather well behaved type theory without
trivializing the identity type structure to look like "just another flavor
of set theory". In particular, one has function extensionality and the
existence of quotient types; two features that many other interesting type
theories lack. These two features are staples in all areas of mathematics,
so they are highly desirable. While set theory has both, the interplay
between the complex identity structure in homotopy type theory and
quotients is very interesting.

First, a definition, a type A is a 'set' if the identity type x = y has at
most one path for each x, y : A. These are essentially the same as
"ordinary sets" since the uniqueness of paths mimics the fact that elements
of a set are either equal or not, with no additional qualification. Given
any type A, one can form its 'set-truncation' |A|_0 which collapses the
identity types between elements of A in order to form a set while leaving
the elements as undisturbed as possible. To explain this differently and
more accurately, let's say that an 'invariant' is a map f:A -> B where B is
a set. (Traditional invariants like rank, genus, spectrum fit this
definition.) Since f must preserve identity types, it must map identified
elements of A to identified elements of B. Invariants are useful to show
that two elements of A are different since equality in the set B is
potentially much simpler than equality in the general type A. The
set-truncation is the universal invariant in the sense that any invariant
f:A -> B must factor through the set-truncation A -> |A|_0.

Given a universe type U, one can form Set(U) the type of all sets in U.
Set(U) is not a set. For example, as discussed above, the type 2 is a set
but 2 = 2 has two elements rather than just one. This may be surprising but
it has some positive consequences: Set(U) is naturally the category of all
sets in U and the path structure between sets is the groupoid structure on
Set(U). Thus Set(U) comes automatically equipped with its natural
structure. What is the set-truncation of Set(U)? It is the type Card(U) of
all cardinal numbers! This works just as well for Group(U), Ring(U), etc.
where the set-truncation are isomorphism types whereas Group(U), Ring(U),
etc. has the natural category structure.

In general, there is no natural lift |A|_0 -> A from the set-truncation to
the original type. Even if there is one, through some invocation of the
axiom of choice for example, the lift is not sufficient to recover the
additional structure of the original type. Assuming the axiom of choice,
there is a lift from Card(U) to Set(U), but this lift does little to
nothing when it comes to recovering the category structure of Set(U).
Similarly for Group(U), Ring(U),etc. This illustrates the subtlety of the
motto "equivalent objects are identified". This motto makes no sense if
"identified" is construed in the traditional binary equal/not-equal meaning
and even homotopy type theory knows that!


> b) What about “Reverse HoTT”, where one classifies theorems according to
> how much univalence / “identifying isomorphic objects” is needed?
>

Some key consequences of univalence have been identified. For example,
function extensionality and the existence of quotient types that I
mentioned earlier. Some people happily point out that one just needs one or
the other rather than full univalence, so this is something that some
naturally pay attention to. Proof assistants are very popular among
homotopy type theory enthusiasts and they can be used to measure proof
dependencies. I've seen a few results of the form "this and that together
are equivalent to univalence" (e.g. I think if one replaces "equivalent" by
"isomorphic" in the definition of univalence then one must separately
assume function extensionality). So there is budding interest in doing this
but no concerted effort in this direction as far as I can tell.

Perhaps there is also a belief that this work can be done automatically by
proof assistants, but reality is a little more subtle. Homotopy type theory
is 'proof-relevant' which has the effect of blurring the distinction
between theorems and proofs. This is problematic for the reversal process,
which is evidently trivial if theorems and proofs are completely fused. In
homotopy type theory there is a systematic process by which one can
separate theorems and proofs. Propositional truncation allows one to assert
that a type is inhabited without requiring an actual inhabitant. The
theorem statement (that a type is inhabited) is then separated from its
proof (the habitant). This makes reversal interesting and, as a side
effect, more opaque to automated analysis by proof assistants (which can
nevertheless be of great assistance in the process).

Best,
François
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160416/f891a858/attachment-0001.html>