Type-Theoretic Replacement and Univalent Completion

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Opening obstruction

A small family can land in a merely locally small type without its image being available as a small type, obstructing replacement and completion constructions.

Development contract

Import finite join powers and connectivity from Chapter 200; construct the sequential-colimit image and prove its universal property; then derive type-theoretic replacement and univalent completion of small families. The completion acts on families, not on a precategory.