Abstract
Although a mapping cylinder is a certain kind of (op)lax colimit, in some 2-categories like CAT and BTOP/S, mapping cylinders also enjoy a right-handed universal property that generalises the classification of (co)partial maps. If formulated naïvely as a principle of synthetic domain theory in Martin-Löf type theory extended by a dominance, this two-handed universal property is unexpectedly strong and renders the dominance discrete. We describe a more refined perspective in the setting of univalent foundations based on a strengthening of the Segal completeness law; from this we obtain a number of accessible reflective subuniverses of untruncated synthetic spaces within which mapping cylinders may be computed in terms of partial map classifiers, where lax and oplax orientation correspond to the choice of dominance.
Talk Details
Speaker: Jon Sterling (University of Cambridge, UK)
Event: Types and Topology Workshop in Honour of Martin Escardo’s 60th Birthday
Date: Wednesday 17 December 2025
Time: 13:45
Slides: Available
Key Topics
- Mapping cylinders
- (Op)lax colimits
- 2-categories
- Synthetic domain theory
- Martin-Löf type theory
- Dominances
- Univalent foundations
- Segal completeness law
- Partial map classifiers
- Reflective subuniverses