Skip to main content

Aspects of the graph model of homotopy type theory

Posted in
Egbert Rijke
Sam, 2016-02-13 14:30 - 16:00
MPIM Lecture Hall

The ω-compact types are the types for which exponentiation by that type
commutes with sequential colimits. Of course the finite types are
ω-compact, but we also want to show that the graph quotients of ω-small
graphs are ω-compact (including the type theoretic analogues of finite
CW-complexes). The proof relies on general constructions in the graph
model. Among them are the descent property, a modality which turns an
arbitrary graph family into an equifibered one, a generalized flattening
lemma which works for arbitrary graph families, and the fact that
colimits commute with identity types. This is a report on work in

© MPI f. Mathematik, Bonn Impressum & Datenschutz
-A A +A