Extensional, homotopical, and computed equality deltas

$T_{\mathrm{H}}$ is the universe-free $\mathrm{\Pi }/\mathrm{\Sigma }/\mathbf{1}/\mathbb{N}/\mathsf{Id}$ Hofmann core. $T_E$ adds reflection and identity uniqueness; $T_I$ instead adds UIP and function-extensionality constants. Theorem 35.39 compares inhabitation only at this signature. It is not a conservativity theorem for $T_0$. Separately, theorem 90.48 imports the Kapulkin–Li Morita equivalence between contextual-category models with $\mathsf{Id}$, ${\mathrm{\Pi }}_{\mathsf{Ext}}$, $\mathrm{\Sigma }$, and UIP, and the matching extensional models. Morita equivalence here means the displayed free–forgetful Quillen adjunction has weak-equivalence unit at cofibrant models. It covers cofibrant extensions at that signature; it is neither blanket syntactic conservativity nor support for $T_{\mathsf{fam}}$ or $T_{\mathsf{co}}$.

Add universe-indexed univalence, its derived function extensionality, truncations, and only the displayed HIT signatures. Univalence is axiomatic and does not compute. The simplicial-model consistency import is exact; no normalization theorem is claimed.

Replace ordinary equality use by the displayed observational equality and cast rules. Normalization/canonicity claims are exactly those imported from the Pujet–Tabareau signature; the chapter’s finite Kappa companion is implemented only.

Add De Morgan dimensions, face formulas, systems, composition, and Glue. Univalence computes through Glue. The cited canonicity/normalization results apply only at their stated cubical signatures.

Replace De Morgan dimension operations by Cartesian substitution and diagonal cofibrations; use arbitrary-source coercion, homogeneous composition, and V/Kan universes. Computational soundness and canonicity are exact imports from Angiuli’s operational semantics; normalization is exactly imported from Sterling–Angiuli only for their universe-free $\mathrm{\Pi }$/$\mathrm{\Sigma }$/path/Glue/circle calculus ${\mathcal{C}}_{\mathrm{SA}}$. The source explicitly omits universes and does not prove its stated De Morgan adaptation. These imports do not make either extension, or any omitted rule, derivable.