  This is the fourth in a series of papers extending Martin-L\"of's meaning
explanation of dependent type theory to higher-dimensional types. In this
installment, we show how to define cubical type systems supporting a general
schema of indexed cubical inductive types whose constructors may take dimension
parameters and have a specified boundary. Using this schema, we are able to
specify and implement many of the higher inductive types which have been
postulated in homotopy type theory, including homotopy pushouts, the torus,
$W$-quotients, truncations, arbitrary localizations. By including indexed
inductive types, we enable the definition of identity types.
  The addition of higher inductive types makes computational higher type theory
a model of homotopy type theory, capable of interpreting almost all of the
constructions in the HoTT Book (with the exception of inductive-inductive
types). This is the first such model with an explicit canonicity theorem, which
specifies the canonical values of higher inductive types and confirms that
every term in an inductive type evaluates to such a value.
