appendix sectionsignatures

Checked extension edges

$T_{Π 2} ↪ T_{0}$ .: Inclusion of a literal subsignature; no metatheorem is transported upward.
$T_{0} ⇝ T_{hott}$ .: Add axiomatic univalence, truncations, and selected HITs. This edge loses judgmental canonicity for closed stuck transports.
$T_{0} ⇝ T T^{obs}$ .: Replace the equality architecture; this is not established as a conservative extension.
De Morgan $↭$ Cartesian cubical.: A comparison of Kan presentations under additional connection/diagonal hypotheses, not an unconditional signature inclusion.