Fwd: [HoTT] What is UF, what is HoTT and what is a univalent type theory?

[Michael Shulman <virit...@gmail.com>]

Here is a message that didn't make it through to the list.


---------- Forwarded message ----------
From: Michael Shulman <shu...@sandiego.edu>
Date: Wed, Jun 8, 2016 at 1:18 AM
Subject: Re: [HoTT] What is UF, what is HoTT and what is a univalent
type theory?
To: Martin Escardo <m.es...@cs.bham.ac.uk>
Cc: "HomotopyT...@googlegroups.com" <HomotopyT...@googlegroups.com>


On Sun, Jun 5, 2016 at 1:40 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> Perhaps you should say what you think HoTT is, for instance to prevent me
> from mis-representing it.

Personally (all caveats repeated), I prefer to use it for the
mathematical subject involving the interaction of homotopy-theoretic
and type-theoretic ideas, including models of type theory in classical
homotopy theories but also application of homotopy-theoretic ideas to
type theory.  I don't mean to specify any particular philosophy or
motivation for doing such mathematics.

> But also to prevent people from reading the book in an unintended way.

Yes, it would be nice for the book to make clearer that the particular
type theory used therein is only one possible choice, and other
possibilities are a field of active research.

> To make a parallel (again), I very much like intuitionistic mathematics as
> Brouwer initiated it. What we nowadays distil from it is called
> intuitionistic logic.
>
> But with Brouwer it had a heavy amount of topology, which we now consider to
> be still very interesting (and in particular I do myself), but we don't any
> more consider to be the essence of intuitionistic mathematics.
>
> ...
>
> But to say homotopy is the ultimate understanding of identity would be like
> saying that topology is the ultimate understanding of intuitionistic logic.

This is a very interesting point; I am glad that you brought it up.
When you first mentioned it a while ago, my reaction was that
"logically it makes sense, but intuitively it feels wrong".  But I
didn't say that out loud because it didn't seem like a very good
argument!  (-:

After mulling it over for a while, however, I have a couple of real
points to make, to explain my intuitive reaction.

Firstly, I agree that topology is not the ultimate understanding of
intuitionistic logic.  But I think one might more plausibly argue that
topology is the ultimate understanding of *geometric* logic.  That is,
the relationship between topology and intuitionistic logic is the same
as the relationship between frames and Heyting algebras.  Every frame
is a Heyting algebra, so topology furnishes models of intuitionistic
logic.  But frame homomorphisms are different from Heyting algebra
homomorphisms, and moreover not every Heyting algebra is complete; so
there is more to intuitionistic logic than topology.

So this is one concrete way in which I think the connection between
homotopy and identity is closer than the connection between topology
and intuitionistic logic.

Secondly, I *DO* actually believe that homotopy is the ultimate
understanding of identity.  Why?  That is essentially the definition
of "homotopy"!  Homotopy theory is the study of infty-groupoids, and
an infty-groupoid is exactly what you get when you take a vague
intuitive notion of "collection" and allow "different witnesses of
identity" in a coherent way.  The historical origins (and current
concrete incarnations) of homotopy theory in topological spaces and
simplicial sets are, philosophically, irrelevant; what the homotopy
theorist is actually interested in are infty-groupoids, as witnessed
by the tide sweeping homotopy theory into (infty,1)-categorical
language that talks more directly about its objects of interest.

A mathematical expression of this is Brunerie's observation that
Martin-Lof's rule for identity types is essentially a definition of
infty-groupoid, and that the definition one gets is essentially the
very first such definition given by Grothendieck.  There is nothing
analogous on the other side of your analogy: the rules of
intuitionistic logic do not encompass a definition of topological
space (though one might argue that the rules of *geometric* logic do).

Best,
Mike