Lectures onType Theory
Fields recorded
appendix sectionsignatures

Fields recorded

Every representative calculus has one block containing:

  1. its inherited signature and exact additions, removals, or replacements;

  2. its equality and conversion judgments;

  3. indexed-family, recursion, coinduction, and universe support;

  4. canonicity, normalization, consistency, and checking-decidability status;

  5. the precise source or local proof for every imported metatheorem;

  6. an artifact version where implementation behavior is used as evidence;

  7. 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.

Search the book

Type to search the local edition.