Christian Sattler: Filtered colimits and HoTT
Time: Wed 2020-05-20 10.00 - 12.00
Location: Zoom, meeting ID: 657 3571 6862
Participating: Christian Sattler, Gothenburg
I plan to discuss two aspects of filtered colimits of higher categories. The focus will be according to audience interent.
The first aspect is an application in HoTT to open questions concerning truncation levels of certain objects, for example the free higher group FX on a set X. Using filtered colimit technology, FX is 1-truncated under n-truncation for any external n. Externally, this gives a constructive proof of the (classically known) fact that the free higher group on a set is 1-truncated.
The second aspect concerns the development of filtered colimits in the higher setting (modelled for example by complete Segal types in HoTT). Adamek et al. define a *sound doctrine* to be a class S of limit shapes such that for any category D, the following are equivalent:
- D-shaped colimits commute with S-limits of sets,
- for any C in S, the constant functor D → [C^op, D] is final.
This notion underlies the theory of S-accessible and locally S-presentable categories. They observe that pullbacks fail to be a sound doctrine. This is rectified in higher categories: pullbacks are a sound doctine. This yields a modular treatment of the theory of filtered colimits.
Meeting ID: 657 3571 6862