QIIT and QWI Schemas, Elimination, and Initiality

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

Opening obstruction

Individual higher inductive examples do not supply a schema guaranteeing that mutually generated operations and equations have an initial algebra.

Development contract

Build the selected QIIT/QWI signatures, algebras, displayed algebras and eliminators; prove initiality/existence at the exact WISC or size assumptions; and distinguish finitary from infinitary constructions.