Published on *Max Planck Institute for Mathematics* (https://www.mpim-bonn.mpg.de)

Posted in

- Talk [1]

Speaker:

Egbert Rijke
Date:

Sat, 2016-02-13 14:30 - 16:00 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