Posted in

Speaker:

Egbert Rijke
Date:

Sat, 2016-02-13 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 |