Re: [HoTT] new slides

[Martin Escardo <escardo...@googlemail.com>]

On 22/09/16 20:46, Vladimir Voevodsky wrote:
> I have uploaded to me homepage the slides of my lecture at HLF 2016 with a discussion of the Univalent Foundations and some discussion of the UniMath library. See https://www.math.ias.edu/vladimir/Lectures .

I like the recognition of the usefulness, and, more importantly, the 
intrinsic interest in the constructive aspect, given in your presentation.

Like you, I am impressed by the work in Cubical Type Theory to make this 
to successfully work in univalent extensions of constructive type theories.

In my view, an important part of the intimate connection of intuition 
with rigorous mathematics (your slide 3) is precisely constructivity. 
Perhaps not everybody wants to be constructive all the time, but we do 
need a good, precise mathematical language that supports constructivity 
directly, without ruling out non-constructive arguments (by seeing them 
as arguments that just give much less information one would like to, 
which potentially one would like to uncover with further refinement).

The Cubical-Type-Theory rendering of UF is such a language.

Best,
Martin