ch:pi-sigma-unit: ch:pi-sigma-unit
Problem and invariant. Construct the finite premise checker required by the seminar. Maintain the invariant that a proposed application, pair, or second projection is accepted only when its family indices agree with the component on which they depend.
Two representations. One can use intrinsically indexed terms, or annotated nominal terms with an external family-index check. The companion uses the second representation, collapsing families to numeric tags so that a mismatched second projection remains a visible negative case.
First complete version. Check application first, pairing second, and the dependent second projection last. After each stage, add one positive case and one nearby malformed case before extending the syntax.
Observable result. The accepted corpus checks dependent application, the dependent curry and uncurry maps of example 27.25, and a mismatched second projection. It prints four named PASS lines and then All 4 Chapter 72 corpus cases passed. A rejected input is represented by a false decision or None; the main oracle negates that result when rejection is expected.
A failing version. Accept every second projection without comparing its family index. The input with first-component tag
Acceptance test. Run the four commands in appendix E. Require a silent check, one passing inline test, the exact five-line run transcript, and an empty audit. Restore the accepted source after replaying the mutation and repeat all four commands.
Mathematical boundary. The program decides the finite representation and cases just described. It does not prove the Sigma-induction construction of proposition 27.12 or the judgmental round trips in example 27.25; those results remain the displayed derivations.