{"id":"palomar/PALOMAR-2026-09-14-000010","url":"https://github.com/Arthur742Ramos/two-dimensional-lambda-calculus-lean/tree/7aa1f961347b19deab3718521627b98f14357bc7","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-14-000010-v1.json","repo":"https://github.com/Arthur742Ramos/two-dimensional-lambda-calculus-lean","tags":["math.LO","msc:03B40","msc:03B38","type-theory","lambda-calculus","homotopy","formalization"],"score":0,"title":"Certified naturality and the obstruction to unrestricted naturality in a typed two-dimensional calculus","trust":"high","domain":"math.LO","source":"palomar","authors":["Arthur F. Ramos"],"reviews":0,"subject":"math.LO","summary":"We formalize the boundary of naturality in the labelled conversion calculus of A Theory of a Two-Dimensional Typed Lambda Calculus. Canonical evaluation of inductively presented homotopies constructs naturality squares, and transport along finite presentations preserves two-paths and recovers the naturality boundary. In contrast, an explicit pointwise family on Fin 3 admits no naturality two-cell or finite pasting: a six-element dihedral-group invariant separates its two boundary paths while respecting every declared two-cell generator. This independently reconstructed refutation is…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-14","reactions":{},"formalized":true,"formalizes":[{"title":"A Theory of a Two-Dimensional Typed Lambda Calculus","identifier":"","relationship":"formalizes"}]}