[Coq-Club] [Agda] A HoTT-Date with Thorsten Altenkirch at Strathclyde 04.03.15

[Andrea Vezzosi]

I would also be very interested in the content of these talks, was the
slide collection successful?

Cheers,
Andrea

On Sat, Feb 21, 2015 at 11:34 PM, Fredrik Nordvall Forsberg
<fredrik.nordvall-forsberg at strath.ac.uk> wrote:
> Dear Darius and Vladimir,
>
> On 21/02/15 15:33, Vladimir Voevodsky wrote:
>>
>> I join in this request - it does sound very interesting. Videos and
>> posted slides (or even notes) would be great to have.
>
>
> I'll see what we can do. At the very least, we'll try to collect slides.
>
> Cheers,
> Fred
>
>>> On Feb 20, 2015, at 4:37 PM, Darius Jahandarie <djahandarie at gmail.com>
>>> wrote:
>>>
>>> I'm unfortunately a few countries and oceans too far away, but these
>>> sound so interesting that I need to ask if you can somehow record the
>>> talks!
>>>
>>> On Fri, Feb 20, 2015 at 12:50 PM, Fredrik Nordvall Forsberg wrote:
>>>>
>>>> Dear All
>>>>
>>>> Dr Thorsten Altenkirch is visiting the MSP group during the week of
>>>> March 2,
>>>> and we thought we would have an afternoon of talks in his honour on
>>>> Wednesday 4 March. Please feel free to attend and forward this to anyone
>>>> else who might be interested. If you would like to give a talk, we could
>>>> create a few spots too. Please get in touch ASAP if you wish to i)
>>>> attend;
>>>> ii) give a talk; and/or iii) stay for dinner. This will help us to cater
>>>> appropriately.
>>>>
>>>> All the best
>>>> Neil and Fred
>>>>
>>>> ******************************
>>>> A HoTT-Date With Thorsten Altenkirch
>>>> (An Afternoon of Talks)
>>>>
>>>> Date: Wednesday 4 March, 2pm
>>>> Location: Room 1415, Livingstone Tower, 26 Richmond Street, Glasgow G1
>>>> 1XH.
>>>>
>>>> Speakers:
>>>>
>>>> Thorsten Altenkirch: Higher Inductive Types
>>>>
>>>> Fredrik Nordvall Forsberg: Presentations of mutually defined types
>>>> (including HITs)
>>>>
>>>> James McKinna: Using relations to streamline the encode-decode method?
>>>>
>>>> Neil Ghani: Higher Dimensional Parametricity via Cubical Categories
>>>>
>>>> Bob Atkey: A Cubical Set Model for Relationally Parametric Type Theory
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda