Pith. sign in

REVIEW 4 major objections 5 minor 18 references

Formal P-Category Theory and Normalization by Evaluation in Rocq

T0 review · 4 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper establishes a machine-checked categorical proof that a computable normalizer produces a unique alpha-equivalent normal form for every beta-eta conversion class of simply typed lambda terms.

desk verdict A serious formalization of p-category theory with a new categorical proof of strong completeness for NbE; the machine-checked claim is plausible but unverifiable without the artifact. read the letter →

arxiv 2505.07780 v1 pith:GETDO3AC submitted 2025-05-12 cs.LO math.CT

David G. Berry , Marcelo P. Fiore This is my paper · ORCID
classification cs.LOmath.CT MSC 03B4018D15
keywords p-categorytheorypartialequivalencerelationsnormalizationbyevaluationsimplytypedlambdacalculusCartesian-closedcategoriesArtin-WraithgluingstrongcompletenessRocqformalization
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper claims that a purely categorical normalization-by-evaluation algorithm for the simply typed $\lambda$ calculus can be proved sound and strongly complete, and that the entire proof can be carried out in a proof assistant. It works in p-category theory, where morphisms are equipped with partial equivalence relations, allowing quotiented and unquotiented syntax to be compared without extinguishing computational content. The main result, Theorem 6.3.6, states that the algorithm $\mathit{nfD}_4$ sends every context substitution to a canonical representative of its $\beta\eta$-conversion class, together with a derivation of that conversion. If correct, this gives a machine-checked bridge from abstract categorical semantics to a concrete extracted program that computes long $\beta\eta$-normal forms.

What carries the argument

The central mechanism is p-category theory: categories whose homs are PTypes, meaning underlying types carrying a partial equivalence relation, so that a morphism may be self-related or not. The paper introduces Cartesian-pre-closed p-categories, a weakening of Cartesian closure in which the two maps relating $\mathrm{Hom}_{\mathcal{C}}(x,b^a)$ and $\mathrm{Hom}_{\mathcal{C}}(x\times a,b)$ are present but are not required to be inverses; this matches the structure of unquotiented syntax, which has abstraction and application but no $\beta\eta$ equations. This structure feeds a new universal property (Theorem 5.2.3) of the unquotiented substitution p-category $\mathsf{Subst}_\alpha$ relative to the quotiented p-category $\mathsf{Subst}_{\beta\eta}$. The final algorithm $\mathit{nfD}_4$ is assembled in a gluing p-category, and the use of strict propositions in the formalization makes the property parts of the PERs proof-irrelevant. The whole development is formalized, and extraction yields programs that compute long $\beta\eta$-normal forms together with conversion derivations.

What would settle it

The decisive test is to compile the accompanying Rocq development and run Print Assumptions on the theorem corresponding to Theorem 6.3.6: if any axiom, admitted lemma, or unproved hetero-composition associativity property appears in its dependency cone, the machine-checked correctness claim is false.

Watch

Extended reading notes

Core claim

On its own terms, the paper's discovery is that strong completeness of normalization by evaluation can be derived from categorical universal properties alone, rather than from syntactic arguments about neutral and normal forms. The key new ingredient is a universal property of the p-category of unquotiented simply typed substitutions, $\mathsf{Subst}_\alpha$, relative to the quotiented p-category $\mathsf{Subst}_{\beta\eta}$. Instantiating this property in a gluing p-category yields the normalization function $\mathit{nfD}_4$ and proves Theorem 6.3.6: for every $\sigma$, $\sigma \sim_{\beta\eta} j(\mathit{nfD}_4(\sigma))$, and $\sigma \sim_{\beta\eta} \sigma'$ implies $\mathit{nfD}_4(\sigma) \equiv_\alpha \mathit{nfD}_4(\sigma')$.

Load-bearing premise

The load-bearing premise is that the Rocq formalization genuinely covers every step of Theorem 6.3.6, even though the paper admits that only some mixed renaming-substitution associativity laws were formalized and that stronger p-naturality properties for $\tilde{q}$ and $\tilde{u}$ could not be proved.

Editorial extensions

If this is right

  • $\beta\eta$-conversion in the simply typed lambda calculus is decidable by computation: convertibility coincides with $\alpha$-equality of the outputs of $\mathit{nfD}_4$.
  • The extracted normalizer returns, along with each normal form, a derivation of $\beta\eta$-conversion, so each normalization result is self-certifying.
  • The formalized full universal property of the free Cartesian-closed p-category gives a reusable categorical interface for interpreting simply typed syntax into arbitrary Cartesian-closed p-categories.
  • The construction separates computational data from logical properties, so restricting to sub-p-sets does not change the underlying computational data type and does not pollute extracted code with proof content.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Inference: the same gluing methodology may extend to type theories with additional type formers, such as products, by defining the corresponding pre-closed structure and checking whether the universal property of unquotiented syntax still forces strong completeness.
  • Inference: the admitted lack of stronger p-naturality for $\tilde{q}$ and $\tilde{u}$ suggests that the universal property of unquotiented syntax may hold in a laxer 2-categorical form; proving that would explain why strong completeness is derivable categorically even where the earlier soundness argument did not transfer.
  • Inference: since the correctness proof is not tied to one concrete syntax presentation, the extracted normalizer could serve as a decision procedure for $\beta\eta$-convertibility in other constructive settings where the same p-categorical structure can be instantiated.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The manuscript develops a formalization of P-category theory (where hom sets are partial equivalence relations, implemented as subsetoids) in the Rocq proof assistant, and applies it to simply typed lambda-calculus. It defines p-categories, p-functors, p-natural transformations, ends and coends, Cartesian-closed and Cartesian-pre-closed structure, and then uses a new universal property of the unquotiented substitution category Substα relative to Substβη (Theorem 5.2.3) to construct normalization functions. The main claimed result is Theorem 6.3.6: the normalization function nfD4 defined in Definition 6.3.2 is sound (σ∼βη j(nfD4(σ))) and strongly complete (σ∼βη σ′ ⇒ nfD4(σ) ≡α nfD4(σ′)). The paper aims to extend Cubrić–Dybjer–Scott by giving a categorical proof of strong completeness and to provide a machine-checked formalization with extracted normalization programs.

Significance. If the formalization is complete, the paper makes a genuinely useful contribution: it gives the first formalized account, to the authors' knowledge, of the full two-dimensional universal property of the free Cartesian-closed category, introduces the notion of p-Cartesian-pre-closed structure, and obtains a sound and strongly complete normalization-by-evaluation algorithm that avoids separate treatment of neutral and normal terms. The design choices of proof-irrelevant strict propositions and explicit-list substitutions are sensible for the p-category setting. The paper also reports extracted programs computing long βη-normal forms, which is a falsifiable, practical claim. However, because the central correctness claim is explicitly described as machine-checked, the missing artifact and the admitted gaps in §4.3 and §7.2 are the main obstacles to accepting this claim at face value.

major comments (4)
  1. [General; Theorem 6.3.6] The claim that Theorem 6.3.6 is machine-checked in Rocq is not verifiable from the manuscript, since no Rocq source, repository, or build instructions are supplied. The paper's own remarks in §4.3 and §7.2 state that only "some, but not all" hetero-composition associativity conditions were formalized and that stronger p-naturality for q̃ and ũ could not be proved; as nfD4 in Definition 6.3.2 is built from q̃, ũ, and the universal property of Theorem 5.2.3, the text does not establish that these admitted gaps are disjoint from the proof of Theorem 6.3.6. Please provide the artifact and a per-lemma status table for the statements used in the main theorem.
  2. [§6.3, Construction 6.3.1 and Lemma 6.3.5] Construction 6.3.1 asserts that the gluing p-category [Substα↓[Substα is Cartesian-closed and that there is an induced Cartesian-pre-closed p-functor ⟨y↓⟨j⟩j⟩; the text does not provide a proof of these facts. Similarly, Lemma 6.3.5, the extensional agreement of nfD4 and nfC4, is stated without proof. Since these results are load-bearing for both halves of Theorem 6.3.6, the paper should include proof outlines or explicit references to the corresponding Rocq lemmas.
  3. [§4.3 Remark] The remark in §4.3 that "some, but not all" hetero-composition associativity conditions were formalized is too coarse for a formalization paper whose main theorem depends on composition of substitutions and renamings. Please indicate exactly which hetero-composition laws are required by the development leading to Theorem 6.3.6 and which of them are checked in Rocq, or explicitly restrict the machine-checked claim accordingly.
  4. [§5.2, Theorem 5.2.3] Theorem 5.2.3 is the novel universal property of Substα relative to Substβη on which the normalization construction is based, but the statement is highly intricate and no proof or proof sketch is given in the text. For a journal submission, either a pen-and-paper proof outline or a precise pointer to the corresponding Rocq development is needed, especially because the theorem's uniqueness condition involves implications that are easy to misstate.
minor comments (5)
  1. [§2.2, Definition 2.2.5] The symbol ∼= for p-isomorphism is used in later sections (e.g., Definition 2.2.7 and Definition 5.2.1) but is not introduced in Definition 2.2.5; please define it explicitly at the point of first use.
  2. [§6.1, Theorem 6.1.3 proof] The proof of Theorem 6.1.3 uses steps marked "nat" and "yon/nerve" without referencing the specific lemmas that justify them; please add pointers to the relevant p-naturality and Yoneda/nerve lemmas in the formalization.
  3. [§3.3, Lemma 3.3.6 and Figure 3.3.1] Lemma 3.3.6 refers to Figure 3.3.1, but the diagram is not explained in the text, leaving the maps e~H and e~K and the compatibility condition "α lifts the Cartesian-pre-closure" implicit; consider adding a paragraph that names these maps and states the condition precisely.
  4. [Abstract; §4.3; §7.2] The abstract claims a "complete formalization", but §4.3 and §7.2 describe limitations; please harmonize the claims in the abstract and introduction with the actual formalization status.
  5. [§4.4, Definition 4.4.1] The phrase "least symmetric, transitive, and congruent relation over β-reduction and η-expansion" is informal; the Rocq listing A.8 makes it precise, but the text should state explicitly that this is the inductive closure.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the normalization theorem is derived from stated universal properties and gluing constructions, not from fitted inputs or a self-citation chain.

full rationale

The derivation is self-contained. The normalization function nfD4 (Definition 6.3.2) is a defined algorithm built from the universal property of Substα relative to Substβη (Theorem 5.2.3), the gluing p-category construction (Construction 6.3.1), and the interpretation functor J−K; none of these is a fitted parameter. Theorem 5.2.3 is stated as a theorem of the Rocq development, not imported from the authors' prior work: the Fiore (2002, 2022) citations are contextual and are not used to discharge any proof obligation. The strong-completeness property follows because J−K is a p-functor on Substβη and hence respects βη-conversion, while the q̃/ũ components come from the stated universal property; this is a proved semantic fact rather than an assumption of the conclusion. Soundness is justified by explicit equational reasoning in §6.1, and Lemma 6.3.5 is supplied by the comma/gluing construction rather than being a restatement of Theorem 6.3.6. The paper's own limitations—§4.3 Remark (only some hetero-composition associativity conditions formalized) and §7.2 (stronger p-naturality for q̃ and ũ unproved)—concern the completeness of the machine-checked claim, and the absence of an accompanying Rocq artifact makes Theorem 6.3.6 unverifiable from the preprint alone. Those are verification gaps, not circular steps. No equation was found that reduces a predicted quantity to its defining input, and no load-bearing justification is supplied by self-citation.

Assumptions & free parameters 0 free parameters · 2 assumptions · 0 invented entities

This is a proof-heavy paper with no fitted parameters or hand-chosen numbers. The implicit assumptions are the soundness of the Rocq logical framework features used (SProp, universe polymorphism) and the correctness of the extensive formalization, which is not shipped as an artifact. The paper's own stated limitations are acknowledged.

assumptions (2)
  • domain assumption The Rocq logical framework with strict propositions (SProp) is sound and the formalization compiles.
    All proofs are machine-checked against this framework; any inconsistency would invalidate the results. The paper relies on SProp for PER relations and on universe polymorphism, which are features of Rocq.
  • standard math The p-category definitions (Sections 2-3) faithfully generalize classical category theory to the PER setting.
    The paper adapts standard notions from Cubrić et al. (1998) and Fiore (2002, 2022); if these definitions are inadequate, the universal properties and gluing constructions do not apply.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Formal P-Category Theory and Normalization by Evaluation in Rocq." pith.science (2026). https://pith.science/paper/GETDO3AC

@misc{pith2026250507780,
  author       = {Pith},
  title        = {Pith review of: Formal P-Category Theory and Normalization by Evaluation in Rocq},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/GETDO3AC}},
  note         = {Machine review of arXiv:2505.07780}
}
read the original abstract

Traditional category theory is typically based on set-theoretic principles and ideas, which are often non-constructive. An alternative approach to formalizing category theory is to use E-category theory, where hom sets become setoids. Our work reconsiders a third approach - P-category theory - from \v{C}ubri\'c et al. (1998) emphasizing a computational standpoint. We formalize in Rocq a modest library of P-category theory - where homs become subsetoids - and apply it to formalizing algorithms for normalization by evaluation which are purely categorical but, surprisingly, do not use neutral and normal terms. \v{C}ubri\'c et al. (1998) establish only a soundness correctness property by categorical means; here, we extend their work by providing a categorical proof also for a strong completeness property. For this we formalize the full universal property of the free Cartesian-closed category, which is not known to have been performed before. We further formalize a novel universal property of unquotiented simply typed lambda-calculus syntax and apply this to a proof of correctness of a categorical normalization by evaluation algorithm. We pair the overall mathematical development with a formalization in the Rocq proof assistant, following the principle that the formalization exists for practical computation. Indeed, it permits extraction of synthesized normalization programs that compute (long) beta-eta-normal forms of simply typed lambda-terms together with a derivation of beta-eta-conversion.

Figures

Figures reproduced from arXiv: 2505.07780 by the authors.

Figure 3.3
Figure 3.3. 1: Lifting of Cartesian-Pre-Closure to Induced [PITH_FULL_IMAGE:figures/full_fig_p012_3_3.png] view at source ↗
Figure 5.2
Figure 5.2. 1: Freeness Property for a Free Cartesian-Closed [PITH_FULL_IMAGE:figures/full_fig_p017_5_2.png] view at source ↗
Figure 6.1
Figure 6.1. 1: Interpretation of Substβη into its p-Category of Presheaves Substβη Subst [α J−K ⟨j⟩ q u [PITH_FULL_IMAGE:figures/full_fig_p018_6_1.png] view at source ↗
Figures from the paper (2 more)
Figure 6.2
Figure 6.2. Figure 6.2: 1: Interpretation of Substβη into the p-Category of Presheaves over Substα Proof. The result follows by equational reasoning: abstracting nf i as nf, and y and ⟨j⟩ as I, we have: nf(σ) ≡ q∆,Γ(JσKΓ(uΓ,Γ(idΓ))) def ∼βη q∆,Γ(u∆,Γ(I(σ)Γ(idΓ))) nat ∼βη q∆,Γ(u∆,Γ(σ)) yon/n…
Figure 6.3
Figure 6.3. Figure 6.3: 1: Interpretation of Substβη into the Gluing p-Category Subst [α ↓ Subst [α 6.3 Sound and Strongly Complete Normalization We glue together a sound normalization algorithm and a strongly complete normalization algorithm to establish full correctness for the strongly c…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

18 extracted references · 18 canonical work pages

  1. [1]

    , Dybjer, P

    Altenkirch, T. , Dybjer, P. , Hofmann, M. , and Scott, P. 2001. Normalization by evaluation for typed lambda calculus with coproducts . In Proceedings 16th Annual IEEE Symposium on Logic in Computer Science , pp. 303--310

    work page 2001

  2. [2]

    , Hofmann, M

    Altenkirch, T. , Hofmann, M. , and Streicher, T. 1995. Categorical Reconstruction of a Reduction Free Normalization Proof . In Pitt, D. , Rydeheard, D. E. , and Johnstone, P. , editors, Proceedings of the 6th International Conference on Category Theory and Computer Science , CTCS '95, pp. 182--199, Berlin, Heidelberg. Springer-Verlag

    work page 1995

  3. [3]

    , Di Cosmo, R

    Balat, V. , Di Cosmo, R. , and Fiore, M. 2004. Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums . In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , POPL '04, 64–76, New York, NY, USA. Association for Computing Machinery

    work page 2004

  4. [4]

    , Gross, J

    Bauer, A. , Gross, J. , Lumsdaine, P. L. , Shulman, M. , Sozeau, M. , and Spitters, B. 2017. The HoTT library: a formalization of homotopy type theory in Coq . In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs , CPP 2017, 164–172, New York, NY, USA. Association for Computing Machinery

    work page 2017

  5. [5]

    , Hur, C.-K

    Benton, N. , Hur, C.-K. , Kennedy, A. , and McBride, C. 2012. Strongly Typed Term Representations in Coq . Journal of Automated Reasoning , 49:141--159

    work page 2012

  6. [6]

    and Schwichtenberg, H

    Berger, U. and Schwichtenberg, H. 1991. An inverse of the evaluation functional for typed -calculus . In Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS 1991) , pp. 203--211, Washington, DC, USA. IEEE Computer Society Press

    work page 1991

  7. [7]

    , Dybjer, P

    C ubri \' c , D. , Dybjer, P. , and Scott, P. 1998. Normalization and the Y oneda Embedding . Mathematical Structures in Computer Science , 8(2):153--192

    work page 1998

  8. [8]

    Fiore, M. 2002. Semantic Analysis of Normalisation by Evaluation for Typed Lambda Calculus . In Proceedings of the 4th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming , PPDP '02, 26–37, New York, NY, USA. Association for Computing Machinery

    work page 2002

Show all 18 references
  1. [9]

    Fiore, M. 2022. Semantic analysis of normalisation by evaluation for typed lambda calculus . Mathematical Structures in Computer Science , 32(8):1028--1065

    2022

  2. [10]

    Gandy, R. O. 1956. On the axiom of extensionality -- Part I . The Journal of Symbolic Logic , 21(1):36–48

    1956

  3. [11]

    , Cockx, J

    Gilbert, G. , Cockx, J. , Sozeau, M. , and Tabareau, N. 2019. Definitional proof-irrelevance without K . Proc. ACM Program. Lang. , 3(POPL)

    2019

  4. [12]

    , Chlipala, A

    Gross, J. , Chlipala, A. , and Spivak, D. I. 2014. Experience Implementing a Performant Category-Theory Library in Coq . In Klein, G. and Gamboa, R. , editors, Interactive Theorem Proving , pp. 275--291, Cham, Switzerland. Springer International Publishing

    2014

  5. [13]

    Hu, J. Z. S. and Carette, J. 2021. Formalizing Category Theory in Agda . In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs , CPP 2021, pp. 327--342, New York, NY, USA. Association for Computing Machinery

    2021

  6. [14]

    Huet, G. P. and Sa \" i bi, A. 2000. Constructive Category Theory . In Plotkin, G. , Stirling, C. P. , and Tofte, M. , editors, Proof, Language, and Interaction: Essays in Honour of Robin Milner , pp. 239--275, Cambridge, MA, USA. The MIT Press

    2000

  7. [15]

    Hyland, J. M. E. 2016. The Forgotten T uring . In Cooper, S. B. and Hodges, A. , editors, The Once and Future Turing: Computing the World , pp. 20--33. Cambridge University Press

    2016

  8. [16]

    Kov \' a cs, A. 2017. A Machine-Checked Correctness Proof of Normalization by Evaluation for Simply Typed Lambda Calculus . Master's thesis, E\"otv\"os Lor\'and University, Budapest, Hungary

    2017

  9. [17]

    and Smith, J

    Salvesen, A. and Smith, J. M. 1988. The strength of the subset type in M artin- L \" o f's type theory . In Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science (LICS 1988) , pp. 384--391, Washington, DC, USA. IEEE Computer Society Press

    1988

  10. [18]

    The Lean Mathematical Library

    The mathlib community 2020. The Lean Mathematical Library . In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs , CPP 2020, 367–381, New York, NY, USA. Association for Computing Machinery

    2020

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.