{"id":"91478d62-f3ef-4b8c-93b5-d71523e27dad","arxiv_id":"2512.03371","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Restriction categories, local categories, bounded partial categories, and bounded inclusion categories form one 2-equivalent theory of partiality.","lead":"This paper introduces local, partial, and inclusion categories as three new ways to describe partial maps, and proves they are 2-equivalent to the established framework of restriction categories. The upshot is a dictionary that lets researchers choose the presentation of partiality that best fits their objects, morphisms, operations, or inclusions.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 12.9's chain of 2-equivalences rests on two 2-equivalence proofs (Thms 12.3/11.14 and 12.6) that are only sketched at the object level; the 2-cell correspondences are left to the reader.","rationale":"We read the paper as an attempt to prove Theorem 12.9: a chain of 2-equivalences among four frameworks for partiality. The object-level constructions (L[X], R[C], partial/inclusion correspondences) are carefully developed and appear correct; in particular, Theorem 4.19 is proved in detail and its unit/counit are isomorphism-level, which gives high confidence. However, the final chain relies on Theorem 12.6 and Theorem 12.3 (via Theorem 11.14), both of which explicitly defer the 2-cell-level verification. The sentence in Theorem 12.6's proof, 'We leave it to the reader to prove that this correspondence lifts to a 2-equivalence,' is a direct admission that the main result is not fully proved. Without bijectivity on 2-cells and 2-naturality, the concatenated equivalence in Theorem 12.9 is unsupported. We do not see a specific false statement, so we do not recommend REJECT; the appropriate status is CONDITIONAL, pending completion of the deferred proofs. This partially agrees with the reader's identification of [L.3] as the key axiom: [L.3] is what makes the object-level pullback constructions work, but the missing 2-cell checks are the immediate obstacle.","tokens_in":39468,"tokens_out":18341,"duration_ms":143680,"concrete_test":"Complete the proof of Theorem 12.6 by explicitly constructing the 2-functors Φ: LCAT→BNCAT and Ψ: BNCAT→LCAT and their unit/counit transformations; verify the triangle identities up to isomorphism. In particular, check that for every pair of local categories C,D, the map Nat(F,G)→Nat(ΦF,ΦG) is a bijection, and that the total sub-2-categories correspond (i.e., the pullback condition on η_M is equivalent to the pullback condition on all inclusions). If the 2-cell map is not bijective, Theorem 12.6 is not a 2-equivalence and the chain in Theorem 12.9 fails.","verdict_should_be":"UNCHANGED","load_bearing_attack":"In the proof of Theorem 12.6 (LCATlax ≃ BNCATlax), after showing an object-level bijection via Propositions 12.4 and 12.5, the paper states: 'We leave it to the reader to prove that this correspondence lifts to a 2-equivalence.' Similarly, the proof of Theorem 12.3 (BPCATlax ≃ BNCATlax) defers the key functorial correspondence: 'We leave it to the reader to show that boundedness-preserving partial functors correspond to boundedness-preserving inclusion functors.' A 2-equivalence requires much more than an object bijection: the 2-functors must be 2-natural, the unit and counit must be 2-natural equivalences, and the maps on 2-cells must be bijective (full and faithful). None of this is supplied. Since Theorem 12.9 simply concatenates these results, the central claim that all four frameworks are 2-equivalent is not established by the written proof. While the reader's weakest assumption [L.3] is indeed the structural axiom that makes the correspondences possible, the immediate load-bearing gap is the missing 2-cell-level verification. The concern is not that the result is false, but that the paper's main theorem relies on unproved assertions at precisely the level (2-equivalence) that the theorem concerns.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces three new frameworks for partiality — local categories (partiality on objects), partial categories (operational control via restriction and contraction), and inclusion categories (partiality via a distinguished system of monics) — and claims a chain of 2-equivalences RCATlax ≃ LCATlax ≃ BPCATlax ≃ BNCATlax, with a total/restriction variant. Sections 2–4 develop local categories and prove that restriction categories are 2-equivalent to local categories. Sections 5–9 translate restriction-category concepts (compatibility, order, monics, Cartesian, split, inverse, join) into local terms. Sections 10–11 introduce partial and inclusion categories and claim PCATlax ≃ NCATlax. Section 12 adds boundedness and claims the four-way equivalence, ending with an inverse-category version and a connection to the Ehresmann–Schein–Nambooripad theorem. The constructions are mostly explicit, and the object-level correspondences are spelled out, but several 2-categorical lifting steps are explicitly left to the reader.","tokens_in":39930,"tokens_out":5556,"duration_ms":52755,"significance":"If the main theorem is established, the paper offers a genuinely useful unification: the same kind of partiality can be expressed on morphisms, objects, operationally, or via inclusions, and the dictionary in Sections 5–9 gives a practical translation kit. The inverse-category application is attractive and connects to a substantial literature. The paper is also careful about its axioms: there are no fitted parameters or hidden definitions, and the paper explicitly flags the non-invariance of boundedness under equivalence of categories (Remark 12.7), the split/non-split distinction (Remark 7.2), and the relationship to M-categories (Remark 12.8). These are strengths. The central weakness is that several load-bearing 2-equivalence claims are not proved: the text repeatedly states that the 2-cell-level lifting is left to the reader. Since the headline result is precisely a 2-equivalence, those missing proofs are not cosmetic.","major_comments":[{"comment":"The proof of PCATlax ≃ NCATlax shows the underlying object correspondence but ends with 'We leave it to the reader to prove that this correspondence defines a full 2-equivalence.' A 2-equivalence requires the two 2-functors to be compatible with 2-cell composition and identities, the unit and counit to be 2-natural equivalences, and the maps on Hom-categories to be equivalences. None of this is supplied. Because Theorem 12.3 and therefore Theorem 12.9 build on this theorem, this is a load-bearing gap, not a stylistic abbreviation.","section":"§11, Theorem 11.14"},{"comment":"The proof of BPCATlax ≃ BNCATlax verifies only the object-level boundedness transfer and then states 'We leave it to the reader to show that boundedness-preserving partial functors correspond to boundedness-preserving inclusion functors.' The 2-functorial correspondence, the 2-naturality of the unit/counit, and the bijectivity/full-faithfulness on 2-cells are not established. Since the chain in Theorem 12.9 relies on this equivalence, the central claim is not proved as written.","section":"§12, Theorem 12.3"},{"comment":"After Propositions 12.4 and 12.5 establish a bijection of objects between local categories and bounded inclusion categories, the proof states: 'We leave it to the reader to prove that this correspondence lifts to a 2-equivalence.' The asserted equivalence LCATlax ≃ BNCATlax is exactly a 2-categorical statement, and the proof stops precisely where the 2-cell and 2-naturality data need to be checked. This is the third link in the chain of Theorem 12.9, so the main theorem is incomplete without this verification.","section":"§12, Theorem 12.6"},{"comment":"Theorem 4.19 is the foundation of the chain, and its proof is more detailed than the later 2-equivalence proofs: Propositions 4.17 and 4.18 give natural isomorphisms R[L[X]] ≅ X and L[R[C]] ≅ C, and the triangle identities are checked. However, the proof does not explicitly verify that these isomorphisms are 2-natural transformations between the 2-functors Llax and Rlax, nor does it show directly that the induced Hom-category functors are equivalences. If the authors are relying on a standard 2-categorical recognition principle, it should be stated precisely; otherwise the verification should be written out, since the final theorem is about 2-equivalence.","section":"§4, Theorem 4.19"}],"minor_comments":[{"comment":"Axiom [P.4] reads 'A f B=A f B=f', which appears to be a typo for the equality A f B = A together with f B = f. Please correct.","section":"§10, Definition 10.1"},{"comment":"The proof of Lemma 4.2 uses several bracketless expressions such as 'f af' and 'gf ag'. Given the paper's diagrammatic composition convention, these are understandable but strain readability; inserting parentheses would help.","section":"§4, Lemma 4.2 and surrounding text"},{"comment":"The proof says 'Theorem 12.3 proves that BPCATlax (PCATlax) is 2-equivalent to BNCATlax (BNCAT)'; the parenthetical 'PCATlax' is confusing and seems to omit the symbol ≃. Please rephrase.","section":"§12, proof of Theorem 12.9"},{"comment":"The statement says 'then both f and g are isomorphisms'; the proof immediately uses that g is monic and derives f first, then g. This is fine, but the statement would be clearer if it said 'then f is an isomorphism and, since g is monic, g is also an isomorphism.'","section":"§7, Lemma 7.4"},{"comment":"The definition of 'restriction monic' is introduced after Lemma 5.12 and phrased in terms of equations involving 'g f' and 'h f'; the notation 'f' for the restriction idempotent of f is standard but could be glossed again here for readers coming from the local-side sections.","section":"§5, Definition 5.13"}],"recommendation":"major_revision","confidential_remarks":"The paper is in scope for the journal and the main idea is promising. My recommendation is driven not by suspicion that the results are false, but by the fact that the headline chain of 2-equivalences rests on three or four places where the most important 2-categorical verification is explicitly omitted. These are likely fixable by adding an appendix with the missing proofs. I do not see citation or novelty concerns; the authors are transparent about the non-invariance of boundedness and about the relationship to prior work."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The core of this paper is solid and worth engaging with. Section 4 is the real work: the construction of L[X] and R[C] is explicit, the unit and counit are spelled out, and Theorem 4.19 is a genuine 2-equivalence between restriction categories and local categories. That result alone justifies the paper. The authors are also honest about what L is not (it is not a functor, η is not natural), and the examples are well chosen. The translation of inverse categories to inverse local categories, and the connection to ESN, is interesting and plausible, though the ESN comparison is more of a discussion than a theorem.\n\nThe soft spot is exactly where the stress-test lands: Theorems 12.3 and 12.6, which carry the final chain, are only proven at the object level. The paper explicitly says “we leave it to the reader” for the 2-cell correspondence in both proofs. That is not a small gap. A 2-equivalence requires the maps on 2-cells to be bijective and the unit/counit to be 2-natural, and none of that is supplied. The object-level constructions are convincing, and I suspect the 2-cell lift works, but as written the main theorem of the paper—the four-way 2-equivalence—rests on assertions rather than proofs. The boundendness non-invariance under equivalence (Remark 12.7) is a real modeling caveat, and the authors deserve credit for flagging it.\n\nOne thing the reader's report did not emphasize enough: the paper is dense and the writing is compressed. That is not a flaw in itself, but it makes the deferred proofs harder to fill in. This is a paper for people already comfortable with restriction categories and 2-category theory, not a survey.\n\nRecommendation: send it to peer review, but require the authors to supply the missing 2-cell-level proofs for Theorems 12.3 and 12.6, or to explicitly downgrade the claim from a 2-equivalence to an equivalence of categories with a conjecture. The main Section 4 result deserves to be published even if the final chain needs tightening.","headline":"A careful, genuinely useful paper that proves a real 2-equivalence between restriction and local categories and sets up a plausible four-way framework, but the final chain of 2-equivalences is not fully proved as written—the 2-cell level is deferred in the last two steps.","tokens_in":721,"tokens_out":882,"would_cite":true,"duration_ms":15000,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["18B10","18D05"],"pacs":[],"model":"deepseek-v4-flash","headline":"Partiality can be encoded equally on morphisms, objects, operationally, or via inclusions, and the four descriptions are 2-equivalent.","keywords":["restriction categories","local categories","partial categories","inclusion categories","partiality","2-equivalence","inverse categories","Ehresmann-Schein-Nambooripad theorem"],"falsifier":"Look for a category with an enlargement assignment satisfying [L.1]–[L.2] but where some pullback of η_M along f:N→L(M) is missing or has L(P)≠L(N). For instance, consider a category of structured sets with inclusions where the preimage of a subobject along a morphism is not itself a structured object of the same kind; then R[C] cannot be formed, so the claimed equivalence cannot apply. As the paper itself notes, the category of sets with subset inclusions fails boundedness, illustrating that the assumption is not vacuous.","tokens_in":39385,"feed_emoji":"🔀","tokens_out":6859,"duration_ms":60101,"temperature":0.7,"pith_summary":"This paper introduces local categories, partial categories, and inclusion categories as three new ways to formalise partiality, alongside the established restriction categories. Its central claim is that these four descriptions—partiality recorded on morphisms, on objects, operationally by restriction/contraction operators, or by a family of inclusions—are not merely analogous but 2-equivalent. Concretely, Theorem 12.9 builds a chain RCATlax ≃ LCATlax ≃ BPCATlax ≃ BNCATlax, with a companion chain for the stricter 'total' 2-cells. A sympathetic reader should care because the equivalences let results proved in one language migrate to the others, and they give a resource-oriented reading: objects of a local category are partially accessible resources whose total space is an enlargement L(M).","feed_headline":"Four categorical descriptions of partiality are 2-equivalent","feed_subtitle":"Restriction, local, bounded partial, and bounded inclusion categories are shown to be one and the same theory.","key_machinery":"The load-bearing object is the local structure: an object-wise assignment M ↦ L(M) (the enlargement) with a monic maximal inclusion η_M: M → L(M) satisfying [L.1] L(L(M))=L(M) and η_{L(M)}=id; [L.2] η_M monic; and [L.3] every pullback of η_M along a morphism f:N→L(M) exists, with L(P)=L(N) and the induced comparison P→N an inclusion satisfying m η_N = η_P. This axiom is what permits defining R[C]'s composition by spans and their pullbacks. The companion machinery is the bounded inclusion system: a class of monics closed under identities, composition, and pullbacks, with at most one inclusion between any two objects and a unique maximal inclusion for each object. The two constructions L[X] an","core_discovery":"The paper's core discovery is that partiality is not a feature of one categorical doctrine but a single structure visible from four sides. It proves the first 2-equivalence by sending a restriction category X to L[X]=Tot[Split_R[X]], whose objects are restriction idempotents and whose morphisms are total maps between them, and a local category C to R[C], whose morphisms are isomorphism classes of spans U ⇉ M,N with L(U)=M. The axioms [L.1]–[L.3] make η_M:M→L(M) a monic 'maximal inclusion' whose pullbacks along arbitrary morphisms exist and remain inclusions, and these pullbacks are exactly what make span composition well-defined. The remaining equivalences pass through bounded partial and in","pith_inferences":["The non-invariance of boundedness under equivalence of categories (Remark 12.7) means the choice of which objects count as total is a genuine modeling choice, not a purely structural one; users of the framework should state that choice explicitly.","The local-category reading suggests a resource-theoretic dictionary (enlargement = total resource, pullback = access restriction) that could be pushed further into concrete models of reversible or resource-aware computation.","The paper leaves a full theory of local limits as future work; if such limits exist and are preserved by the 2-equivalences, all four frameworks would inherit a common theory of partial limits."],"forward_implications":["Any concept or theorem stated for restriction categories—total morphisms, compatibility, partial order, restriction monics—now has a corresponding statement for local categories, and the paper spells the dictionary out.","The 2-equivalences restrict to Cartesian, split, inverse, and join variants, so special classes of restriction categories can be studied through objects (local categories) instead of morphisms.","Inverse (restriction) categories are 2-equivalent to inverse local categories and to bounded inverse inclusion categories, giving a new categorical generalisation of the Ehresmann-Schein-Nambooripad theorem.","Because the four frameworks are 2-equivalent, a construction or classification obtained in one framework (e.g., resource interpretations from local categories) transfers to the others."],"fun_headline_variants":["Partiality: four categorical lenses, one equivalent theory","Local categories unify partiality across four frameworks","Restriction, local, partial, inclusion: all 2-equivalent","Inverse local categories generalize the ESN theorem","One theory of partiality, four categorical viewpoints"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"Axiom [L.3]—that every pullback of a maximal inclusion along any morphism exists and preserves both the enlargement and the inclusion commutation—is the load-bearing premise; if it fails, the span composition in R[C] is undefined and the 2-equivalence between restriction and local categories collapses.","fun_headline_variants_meta":{"raw":{"variants":["Partiality: four categorical lenses, one equivalent theory","Local categories unify partiality across four frameworks","Restriction, local, partial, inclusion: all 2-equivalent","Inverse local categories generalize the ESN theorem","One theory of partiality, four categorical viewpoints"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000486,"raw_usage":{"total_tokens":2259,"prompt_tokens":796,"completion_tokens":1463,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":540,"completion_tokens_details":{"reasoning_tokens":1400}},"tokens_in":540,"tokens_out":1463,"duration_ms":11015,"temperature":1.0,"reasoning_tokens":1400,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-03T18:47:34.560424+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Look for a category with an enlargement assignment satisfying [L.1]–[L.2] but where some pullback of η_M along f:N→L(M) is missing or has L(P)≠L(N). For instance, consider a category of structured sets with inclusions where the preimage of a subobject along a morphism is not itself a structured object of the same kind; then R[C] cannot be formed, so the claimed equivalence cannot apply. As the paper itself notes, the category of sets with subset inclusions fails boundedness, illustrating that the assumption is not vacuous.","supporting_citations":[],"review_version":1}