Connected Maps, Factorization, and Modalities

Opening obstruction

Truncation classifies how much path information a type retains, but later homotopy arguments need maps factored by the connectivity and truncation of their fibers.

Development contract

Develop connected and truncated maps, orthogonal factorization, reflective subuniverses, and modalities without using joins or suspensions before their construction; prove the composition, cancellation, and fiberwise results needed later.