pierrecagne
commented
2 years ago Asserting that there is a given homotopy initial structure is more or less asserting the corresponding higher inductive type. As far as I can tell, the book favors introducing the higher inductive type first with the dependent inductive elimination rule, and then establishing the initiality. The usual next step, when possible, is to prove that the higher inductive type is equivalent to a constructed type (which usually need to jump universes).
This is the roadmap for the circle at least: introduced as a higher inductive type with the dependent elimination rule, then showing it is the initial lasso, and finally showing we can reconstruct the circle as the connected component of (Z,s) (Z being the set of integers, and s the successor function) in the type of types together with a symmetry.
In type theory, there are generally two different ways to construct various algebraic structures such as tensor products of abelian groups, free vector spaces, and polynomial rings: one could either define it type theoretically as a higher inductive type $A$ with point constructors and path constructors representing the structure and properties of the algebraic structure, or categorically as the homotopy initial algebraic structure $A:\mathrm{Str}$, such that for any other such algebraic structure $B:\mathrm{Str}$, the type of structure preserving homomorphisms $A \to_\mathrm{Str} B$ from $A$ to $B$ is contractible. Which approach should be used in this book? I recently realised that while free groups were defined as a higher inductive type in chapter 6, I had defined free vector spaces as a particular homotopy initial vector space in chapter 8.