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 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 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. >