ch:dependent-records: ch:dependent-records

Problem and result. Check the dependency order of the chapter’s $\mathsf{PointedLoop}$ record. The carrier classifies the point, and the point fixes both loop endpoints. The accepted natural-number record has point zero; a mismatched endpoint and a Boolean point under the natural carrier are rejected. A fifth oracle rejects duplicate labels in the executable fresh-label fragment.

Representation. Represent the small universe by NatCarrier and BoolCarrier, and represent field values by tagged natural or Boolean values. A record stores the carrier, point, and endpoints in telescope order. CheckResult separately records acceptance, point-type mismatch, and an endpoint mismatch carrying expected and actual EndpointTypes. A nested Sigma encoding is closer to the metatheory and makes the prefix structure canonical, but the dependent classifiers would have to be simulated by the same tags in this finite Kappa universe. Represent the three declaration labels by a separate finite Label type. freshLabels rejects a repeated label before any value fields are checked. This is the executable fragment used by the Pollack-to-CPT correspondence; Pollack’s larger calculus permits shadowing and is not implemented here.

First complete version. Implement valueMatches, then accept a point only when its tag agrees with the carrier. Projection is already total: matching MkPointedLoop returns its second field, and the displayed good record projects to zero.

Remaining cases. Add equality on tagged values and check endpoints only after the point. On the bad loop, render both classifiers: expected Id Nat 0 0; actual Id Nat 1 1. This is the executable left-to-right telescope invariant, not a generic rejection string.

A failing version. If endpointsGood omits sameValue, the named bad record with point zero and endpoints one is accepted. The line mismatched loop endpoint rejected changes to FAIL.

Acceptance test. Require the five named PASS lines, the final recorded summary, and an empty audit under the four commands recorded in appendix E.

Mathematical boundary. The corpus illustrates left-to-right telescope checking, fresh labels, and projection beta on one finite record universe. It does not prove substitution, normalization, canonicity, the Pollack-to-CPT correspondence, or the translation to nested Sigma types; judgmental record eta is not a rule of the chapter.