ch:dependent-records: ch:dependent-records

For $p:{\mathsf{PointedLoop}}_i$, The point search passes the visible loop field and then stops: $$p.\mathsf{point}\equiv (p|\mathsf{loop}).\mathsf{point}\equiv \mathsf{0}.$$ The carrier search passes loop and point before projection beta: $$p.\mathsf{Carrier}\equiv (p|\mathsf{loop}).\mathsf{Carrier}\equiv ((p|\mathsf{loop})|\mathsf{point}).\mathsf{Carrier}\equiv \mathbb{N}.$$ Each restriction names the actual rightmost field stripped by that passing step: first loop, then point. Every step shortens the searched signature.

For neutral $q$, lookup typing gives $q.\mathsf{point}:q.\mathsf{Carrier}$ and $q.\mathsf{loop}:{\mathsf{Id}}_{q.\mathsf{Carrier}}(q.\mathsf{point},q.\mathsf{point})$. Neither term is headed by a record constructor, so neither contracts. Construction gives $$⟨q|\mathsf{loop},\mathsf{loop}=q.\mathsf{loop}⟩:{\mathsf{PointedLoop}}_i.$$ The displayed computation rules reduce only constructor-headed restriction or projection. They contain no eta rule, so the new constructor is not judgmentally equal to $q$.

For a last field $r$, the candidate source equation translates to $$q^S\stackrel{?}{=}({\mathsf{pr}}_1(q^S),{\mathsf{pr}}_2(q^S)).$$ Sigma eta validates this target equality. The comparison theorem preserves source equality but does not reflect every equality of arbitrary target terms. In particular, no source rule maps back from this Sigma-eta step, so the source record-eta equation remains underivable from the displayed rules.

Define $f(q):=q|r:L$. This is an explicit term former, not a subsumption rule. If width subsumption were added, the raw term $q:L^{\prime }$ would itself also have type $L$. Those types are not judgmentally equal, so ordinary uniqueness of types would fail. Under the Sigma translation, $f^S$ is the first projection $$f^S:\sum _{\rho :L^S}{A}^S(\rho )\to L^S,f^S(q):={\mathsf{pr}}_1(q).$$ The selected calculus contains $f$ but no width judgment.

The Pollack signature appends fields in the order Carrier, point, loop, name. The CPT translation reverses the association: $$⟨\mathsf{Carrier}:{\mathcal{U}}_i,x.⟨\mathsf{point}:x,y.⟨\mathsf{loop}:{\mathsf{Id}}_x(y,y),z.⟨\mathsf{name}:\mathbf{2},w.1⟩⟩⟩⟩.$$ Selecting point in the source passes name and loop, then projects point. In the target, $(\mathsf{Carrier}=\mathbb{N},(\mathsf{point}=\mathsf{0},(\mathsf{loop}=\mathsf{refl},(\mathsf{name}=\mathsf{tt},())))).\mathsf{point}$ passes Carrier once and then uses dot beta at point. Selecting Carrier is immediate in the target but passes name, loop, and point in that order in the left-associated source. These are the two association conventions described by the correspondence proof.