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
progress.
Links:
[1] https://www.mpim-bonn.mpg.de/taxonomy/term/39
[2] https://www.mpim-bonn.mpg.de/node/3444
[3] https://www.mpim-bonn.mpg.de/node/6459