Till innehåll på sidan

Peter LeFanu Lumsdaine: Inverse diagram models of type theory, part 3

Tid: On 2018-02-21 kl 10.00 - 11.45

Plats: Room 16, building 5 kräftriket, Department of Mathematics, Stockholm University 

Medverkande: Peter LeFanu Lumsdaine, SU

Exportera till kalender

Abstract: I will revisit inverse diagram models of type theory, which I previously spoke about in the seminar last November. In particular, I will talk about how functors between inverse categories induce maps between their diagram CwA’s, and give the (rather fun) proof that a homotopy equivalence of inverse categories induces a local equivalence of diagram CwA’s.

As background, it will be helpful if you either have some recollection (possibly hazy) of my seminars last November, or else have viewed my online seminar from last Thursday in the HoTTEST series — slides and video to be posted shortly at uwo.ca/math/faculty/kapulkin/seminars/hottest.html