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

["Martín Hötzel Escardó" <"m.es..."@cs.bham.ac.uk>]

Many thanks, Mike, for your reply. I am prepared to agree with all your 
points, in particular:

(1) You use geometric logic to explain the gap between topology and 
intuitionistic logic in a very nice and precise way. In particular, you 
said "the rules of intuitionistic logic do not encompass a definition of 
topological space (though one might argue that the rules of *geometric* 
logic do)". Nice way to put it.

(2) You make the point that, since the presence of identity types makes 
types into infty-groupoids, we get (an incarnation of) homotopy theory. 
So, in this sense, yes, we have a much more precise match.

(But, to play devil's advocate, we do have a precise definition of 
geometry logic to match up with intuitionistic logic, but are you 
offering precise definitions of the things to be matched up in (2)? 
(Existing or to be developed.))

You also make a point that HoTT is not tied to a particular type theory, 
like Vladimir says UF is not tied to a particular type theory. I agree 
with this, and I am sorry if in previous messages I may have conveyed 
the opposite view.

Now, for the sake of discussion, suppose a particular incarnation of 
HoTT like in the book, based on MLTT. I wonder what you think about the 
question of when MLTT ends and HoTT begins. For instance, much of 
HoTT/UF works without anything added to MLTT, not even function 
extensionality, like seeing that types are infty-groupoids, the 
definition of n-type, the definition of equivalence and more. Is HoTT a 
way to understand (the identity types of) MLTT? (Which, in this case, 
is, as Vladimir said, not the originally intended one.)

Best,
Martin

On 08/06/16 09:18, Michael Shulman wrote:
> 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
>

-- 
http://www.cs.bham.ac.uk/~mhe