Sequential Colimits in Homotopy Type Theory

Sequential colimits are an important class of higher inductive types. We present a self-contained and fully formalized proof of the conjecture that in homotopy type theory sequential colimits appropriately commute with Σ-types. This result allows us to give short proofs of a number of useful corollaries, some of which were conjectured in other works: the commutativity of sequential colimits with identity types, with homotopy fibers, loop spaces, and truncations, and the preservation of the properties of truncatedness and connectedness under sequential colimits. Our entire development carries over to (∞, 1)-toposes using Shulman's recent interpretation of homotopy type theory into these structures.