Re: [HoTT] Re: Vladimir Voevodsky

[Michael Shulman <shu...@sandiego.edu>]

Regarding (0), I'm fairly certain that h-levels were pretty solidly
established in the Coq code that he showed us at CMU in February 2010.
So if he did formulate them in "early 2010" it was very early in the
year.

On Thu, Oct 12, 2017 at 2:55 PM, Martín Hötzel Escardó
<escardo...@gmail.com> wrote:
> On Thursday, 12 October 2017 20:24:26 UTC+1, Daniel R. Grayson wrote:
>>
>> PS: it is the oldest email I have from him with the word "univalent" or
>> "univalence" in it.
>
>
>  In the vein of bringing to public record  things that Vladimir said, here
> is a short interview.
>
> -------- Forwarded Message --------
> Subject: Re: historical question
> Date: Thu, 22 Oct 2015 16:08:14 -0400
> From: Vladimir Voevodsky <vlad...@ias.edu>
> To: Martin Escardo <m.es...@cs.bham.ac.uk>
> CC: Prof. Vladimir Voevodsky <vlad...@ias.edu>
>
>
>> On Oct 22, 2015, at 3:32 PM, Martin Escardo <m.es...@cs.bham.ac.uk>
>> wrote:
>>
>> Hi Vladimir,
>>
>> (0) When did you formulate hlevels in type theory?
>
> Probably in early 2010
>
>> (1) When did you formulate the univalence axiom?
>
> Originally in 2005 as a property of morphisms (fibrations). In late 2009 as
> a formula in type theory.
>
>>
>>    (And when did you give your model for it?)
>
> In a sense in 2006, only I did not know how to model the Martin-Lof identity
> types and thought that different identity types will need to be introduced
> that will satisfy univalence but what other properties to require from them
> I did not know.
>
>>
>> (2) When did you prove that univalence implies function extensionality?
>
> July 2010.
>
>>
>> I am giving a talk next week trying to rigorously explain the univalence
>> axiom to classical mathematicians. This will involve, of course, trying
>> to first explain Martin-Loef type theory, particularly the identity type.
>>
>> One thing between you and Martin-Loef is Hofmann-Streicher's groupoid
>> model, in which they have a proto-form of univalence. Were you inspired
>> by that, or were your thoughts independent of that?
>
> I was not inspired by it. In fact I tried several times to understand what
> they are saying and never could.
>
>>
>> (Also: what was your first reaction when you saw the identity type for
>> the first time? Did you immediately connect it with path spaces?)
>
> Not at all. I did not make this connection until late 2009. All the time
> before it I was hypnotized by the mantra that the only inhabitant of the Id
> type is reflexivity which made then useless from my point of view.
>
> Vladimir.
>
>
> --
> 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.