ch:cic: ch:cic
Problem and result. Implement the printed finite declaration-summary checks in Kappa. The result accepts vectors and equality, rejects the negative Bad occurrence at constructor-arg/domain, and rejects informative elimination of the existential with the verdict Prop-witness-blocks-Type-elimination. It also rejects informative elimination from the two-constructor proposition Or.
Representation. Represent a declaration by its family name, sort and level, parameter-token list, constructor-field types and conclusions, field-sort classifications, and requested elimination family. Constructor fields retain nested arrows, so a recursive family occurrence in an arrow domain remains visible. A full raw PCUIC abstract syntax would make the small checker less transparent and might suggest that it implements the historical checker; finite summaries preserve the exact boundary.
First complete version. Check that every constructor conclusion names the declared family and repeats its universe level and all parameters exactly. Traverse every constructor field and reject a recursive family occurrence in a nested arrow domain.
Remaining cases. Add the elimination-family check for propositions. It permits a Type target only for at most one constructor whose fields are all of sort Prop. Equality passes; the existential carries Or has two constructors. Print one verdict per declaration.
A failing version. Treat every occurrence in a constructor argument as positive. The mutated checker then accepts Bad; its output disagrees with the required path-sensitive third line and the inline test fails.
Acceptance test. Run the four commands in appendix E. Require exactly ACCEPT Vector, ACCEPT Equality, the three named REJECT lines, and an empty audit.
Mathematical boundary. The companion checks only the printed summary fragment. It neither implements historical PCUIC nor proves positivity-oracle correctness, normalization, consistency, canonicity, or safe-checker soundness.