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

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

No, I am not offering precise definitions of the things to be matched
up in (2).  I don't think this detracts much from the point, given the
youth of the subject.  (-:

As for when MLTT ends and when HoTT begins, if "MLTT" and "HoTT" refer
to specific formal systems, then the answer is that HoTT begins
whenever we use something present in HoTT that is not present in MLTT,
like univalence or HITs.  But if "MLTT" and "HoTT" refer to
philosophies, attitudes, or techniques, then there's no reason that
one of them has to end at the same time as the other begins.  I would
say that HoTT begins whenever we start using ideas from homotopy
theory, including things like the definition of n-type and the
definition of equivalence that don't use anything added to the formal
system of MLTT.  Whether MLTT has ended before that depends on what
exactly the philosophy/attitude/techniques of MLTT mean, which I'm
probably not qualified to comment on.

Mike

On Wed, Jun 8, 2016 at 3:14 AM, Martín Hötzel Escardó
<m.es...@cs.bham.ac.uk> wrote:
> 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
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.