ch:definitional-functoriality: positive actions

Problem and invariant. Interpret a finite positive description and map every recursive position exactly once while leaving constant positions unchanged.

Representation and construction. Use codes for unit, constant, parameter, product, sum, and dependent tagged sum, with a matching finite value datatype. Define the action by structural recursion, check identity and composition on named values, and reject the separate negative-occurrence code before interpretation.

Observable result and mutation. Require identity, composition, dependent-sigma, the negative-occurrence rejection, and the summary shown in Appendix E. Returning the old right product component still checks but changes the first line to identity-failed; always selecting the zero dependent-Sigma fiber changes the third line to dependent-sigma-failed.

Acceptance and boundary. Match the accepted source record in Appendix E. Restore and rerun the four commands after mutation. The finite interpreter proves none of the calculus’s normalization, canonicity, or checking results.