appendix sectionsignatures
Fields recorded
Every representative calculus has one block containing:
its inherited signature and exact additions, removals, or replacements;
its equality and conversion judgments;
indexed-family, recursion, coinduction, and universe support;
canonicity, normalization, consistency, and checking-decidability status;
the precise source or local proof for every imported metatheorem;
an artifact version where implementation behavior is used as evidence;
explicit “open,” “conditional,” or “not in signature” entries wherever no theorem is available.
No blank means “standard,” and no theorem transfers from one row calculus, equality architecture, cubical category, or implementation fragment to another without a stated translation theorem.