Peter LeFanu Lumsdaine: Equivalences of (models of) type theories (cont.)

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