Peter LeFanu Lumsdaine: Equivalences of (models of) type theories (cont.)
Time: Wed 2015-10-14 10.00 - 11.45
Location: Room 16, building 5, Kräftriket, Department of mathematics, Stockholm University
Participating: Peter LeFanu Lumsdaine, Department of mathematics, Stockholm University
Abstract: Continuing from last week’s seminar, I will go into the details of the logical structure in the models in spans and span-equivalences. I will also lay out some more abstract nonsense about categories of contextual categories, and use this to give applications of the span-equivalences model to the “homotopy theory of homotopy type theory”.