* new slides
@ 2016-09-22 19:46 Vladimir Voevodsky
2016-09-22 20:18 ` [HoTT] " Martin Escardo
2016-09-22 23:12 ` Dimitris Tsementzis
0 siblings, 2 replies; 4+ messages in thread
From: Vladimir Voevodsky @ 2016-09-22 19:46 UTC (permalink / raw)
To: Univalent Mathematics, Homotopy Type Theory; +Cc: Prof. Vladimir Voevodsky
[-- Attachment #1: Type: text/plain, Size: 238 bytes --]
Hello,
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 .
Vladimir.
[-- Attachment #2: Message signed with OpenPGP using GPGMail --]
[-- Type: application/pgp-signature, Size: 507 bytes --]
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: [HoTT] new slides
2016-09-22 19:46 new slides Vladimir Voevodsky
@ 2016-09-22 20:18 ` Martin Escardo
2016-09-22 23:12 ` Dimitris Tsementzis
1 sibling, 0 replies; 4+ messages in thread
From: Martin Escardo @ 2016-09-22 20:18 UTC (permalink / raw)
To: Vladimir Voevodsky, Univalent Mathematics, Homotopy Type Theory
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
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: [HoTT] new slides
2016-09-22 19:46 new slides Vladimir Voevodsky
2016-09-22 20:18 ` [HoTT] " Martin Escardo
@ 2016-09-22 23:12 ` Dimitris Tsementzis
2016-09-23 19:05 ` Vladimir Voevodsky
1 sibling, 1 reply; 4+ messages in thread
From: Dimitris Tsementzis @ 2016-09-22 23:12 UTC (permalink / raw)
To: Vladimir Voevodsky; +Cc: Univalent Mathematics, Homotopy Type Theory
On the fourth bullet point of slide 12 it is claimed that it might be easier to solve the problem of infinite objects in CTT. Why is that the case?
Is this related to the third bullet point, namely because it might be easier to implement a strict equality in CTT? (I still don’t understand why implementing a strict equality in CTT is easier than in MLTT+UA, but at least this way I see the connection with the problem of infinite objects.)
Dimitris
> On Sep 22, 2016, at 15:46, Vladimir Voevodsky <vlad...@ias.edu> wrote:
>
> Hello,
>
> 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 .
>
> 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.
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: [HoTT] new slides
2016-09-22 23:12 ` Dimitris Tsementzis
@ 2016-09-23 19:05 ` Vladimir Voevodsky
0 siblings, 0 replies; 4+ messages in thread
From: Vladimir Voevodsky @ 2016-09-23 19:05 UTC (permalink / raw)
To: Dimitris Tsementzis
Cc: Prof. Vladimir Voevodsky, Univalent Mathematics, Homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 1308 bytes --]
No, it is more related to another idea that I am not quite ready to explain yet.
Vladimir.
> On Sep 23, 2016, at 1:12 AM, Dimitris Tsementzis <dtse...@princeton.edu> wrote:
>
> On the fourth bullet point of slide 12 it is claimed that it might be easier to solve the problem of infinite objects in CTT. Why is that the case?
>
> Is this related to the third bullet point, namely because it might be easier to implement a strict equality in CTT? (I still don’t understand why implementing a strict equality in CTT is easier than in MLTT+UA, but at least this way I see the connection with the problem of infinite objects.)
>
> Dimitris
>
>> On Sep 22, 2016, at 15:46, Vladimir Voevodsky <vlad...@ias.edu> wrote:
>>
>> Hello,
>>
>> 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 .
>>
>> 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.
>
[-- Attachment #2: Message signed with OpenPGP using GPGMail --]
[-- Type: application/pgp-signature, Size: 507 bytes --]
^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2016-09-23 19:05 UTC | newest]
Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2016-09-22 19:46 new slides Vladimir Voevodsky
2016-09-22 20:18 ` [HoTT] " Martin Escardo
2016-09-22 23:12 ` Dimitris Tsementzis
2016-09-23 19:05 ` Vladimir Voevodsky
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).