Posted in
Speaker:
Egbert Rijke
Datum:
Sam, 13/02/2016 - 14:30 - 16:00
Location:
MPIM Lecture Hall
Parent event:
Workshop on Homotopy Type Theory 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.
© MPI f. Mathematik, Bonn | Impressum & Datenschutz |