Pith. sign in

REVIEW 4 major objections 5 minor 21 references

Local categories: a new framework for partiality

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

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

Pith's one-line read Partiality can be encoded equally on morphisms, objects, operationally, or via inclusions, and the four descriptions are 2-equivalent.

desk verdict 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. read the letter →

arxiv 2512.03371 v2 pith:FW55EKOV submitted 2025-12-03 math.CT

Marcello Lanfranchi , Jean-Simon Pacaud Lemay This is my paper · ORCID
classification math.CT MSC 18B1018D05
keywords restrictioncategorieslocalpartialinclusionpartiality2-equivalenceinverseEhresmann-Schein-Nambooripadtheorem
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 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).

What carries the argument

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

What would settle it

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.

Watch

Extended reading notes

Core claim

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

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

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

  • 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.
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 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.

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 (4)
  1. [§11, Theorem 11.14] 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.
  2. [§12, Theorem 12.3] 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.
  3. [§12, Theorem 12.6] 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.
  4. [§4, Theorem 4.19] 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.
minor comments (5)
  1. [§10, Definition 10.1] 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.
  2. [§4, Lemma 4.2 and surrounding text] 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.
  3. [§12, proof of Theorem 12.9] 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.
  4. [§7, Lemma 7.4] 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.'
  5. [§5, Definition 5.13] 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.

Circularity Check

0 steps flagged · score 2.0 of 10

No circular derivation; central equivalences are constructed explicitly, with minor non-load-bearing self-citation and two deferred 2-cell verifications.

full rationale

The derivation chain is not circular. Section 4 defines L[X]=Tot[Split_R[X]] and R[C] via spans and proves R[L[X]]≅X and L[R[C]]≅C (Props 4.17-4.18), with Theorem 4.19 checking the triangle identities; no parameter is fitted and neither construction assumes the other. The bounded partial/inclusion stage is also additive: Definitions 12.1-12.2 impose boundedness, Propositions 12.4-12.5 give mutually inverse object-level constructions, and Theorem 11.14 already gave partial≃inclusion. The only self-citation involving an author of this paper is [6] (Cockett–Lemay), used in Definition 5.1 for the standard notion of compatible morphisms; it is not load-bearing for Theorem 12.9. The genuine weaknesses are rigor gaps, not circularity: Theorem 12.6 says 'We leave it to the reader to prove that this correspondence lifts to a 2-equivalence' and Theorem 12.3 says 'We leave it to the reader to show that boundeness-preserving partial functors correspond to boundedness-preserving inclusion functors.' These defer the 2-cell-level verification that a 2-equivalence requires; if the gaps were filled the result would stand, and if not the theorem is underproved, but no step reduces to its own input. Remark 12.7's admission that boundedness is not invariant under equivalence is a limitation on the choice of total objects, not a circular step.

Assumptions & free parameters 0 free parameters · 6 assumptions · 1 invented entities

No free parameters or fitted data appear in this purely categorical paper. The central claim rests on the new axioms for local, partial, and inclusion structures, together with standard 2-category and pullback facts. These new axioms are the paper's contribution rather than empirical inputs.

assumptions (6)
  • standard math Restriction category axioms ([R.1]–[R.4]) and split-completion construction Split_R from Cockett–Lack
    Background framework the paper extends; used in Section 2 and throughout.
  • ad hoc to paper Local category axioms [L.1]–[L.3], including existence/stability of pullbacks of maximal inclusions with LP=LN
    New definitional premise (Section 3). The 2-equivalence with restriction categories depends on these exact axioms; the paper shows they are satisfied by L[X] but does not prove they are the only possible choice.
  • ad hoc to paper Partial category axioms [P.1]–[P.8] and boundedness (unique maximal object)
    New axiomatization in Sections 10 and 12; used to prove equivalence to inclusion and, when bounded, to local/restriction categories.
  • ad hoc to paper Inclusion system axioms [I.1]–[I.5] and boundedness (unique maximal inclusion)
    New axiomatization in Sections 11 and 12; necessary for Theorems 12.3–12.9.
  • standard math Standard 2-categorical machinery: 2-equivalences preserve adjunctions and Cartesian objects ([16, Prop. 6.1.7])
    Used in Theorem 6.9 to lift the equivalence to Cartesian objects; accepted background.
  • standard math Pullback pasting and stability of monics/isomorphisms under pullback
    Used throughout proofs, e.g. Lemmas 7.4, 8.6, and 10.10.
invented entities (1)
  • Enlargement operation L and maximal inclusions η_M on a local category
    purpose: Encoding partiality on objects: every object M is embedded into a larger total object LM.
    A new primitive structure. Its legitimacy rests entirely on the proved internal equivalences and on concrete examples (PARSET, PARTOP, IDEMRING^op); there is no external mathematical datum predicting it.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Local categories: a new framework for partiality." pith.science (2026). https://pith.science/paper/FW55EKOV

@misc{pith2026251203371,
  author       = {Pith},
  title        = {Pith review of: Local categories: a new framework for partiality},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FW55EKOV}},
  note         = {Machine review of arXiv:2512.03371}
}
abstract

Restriction categories provide a categorical framework for partiality. In this paper, we introduce three new categorical theories for partiality: local categories, partial categories, and inclusion categories. The objects of a local category are partially accessible resources, and morphisms are processes between these resources. In a partial category, partiality is addressed via two operators, restriction and contraction, which control the domain of definition of a morphism. Finally, an inclusion category is a category equipped with a family of monics which axiomatize the inclusions between sets. The main result of this paper shows that restriction categories are $2$-equivalent to local categories, that partial categories are $2$-equivalent to inclusion categories, and that both restriction/local categories are $2$-equivalent to bounded partial/inclusion categories. Our result offers four equivalent ways to describe partiality: on morphisms, via restriction categories; on objects, with local categories; operationally, with partial categories; and via inclusions, with inclusion categories. We also translate several key concepts from restriction category theory to the local category context, which allows us to show that various special kinds of restriction categories, such as inverse categories, are $2$-equivalent to their analogous kind of local categories. In particular, the equivalence between inverse (restriction) categories and inverse local categories is a generalization of the celebrated Ehresmann-Schein-Nambooripad theorem for inverse semigroups.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

21 extracted references

  1. [1]

    AppliedCategoricalStructures.22.2(2014),pp.331-417

    Cockett,J.R.B.&Cruttwell,G.S.H.DifferentialStructure,TangentStructure,andSDG. AppliedCategoricalStructures.22.2(2014),pp.331-417

    2014

  2. [2]

    Carboni, A., Kelly, G. M. & Wood, R. J. A 2-categorical approach to change of base and geometricmorphisms.I.CahiersTopologieGéom.DifférentielleCatég..32.1(1991),pp.47- 95

    1991

  3. [3]

    Cockett,J.R.B.&Lack,S.RestrictioncategoriesI:categoriesofpartialmaps.Theoretical ComputerScience.270.1-2(2002),pp.223-259

    2002

  4. [4]

    Cockett,J.R.B.&Lack,S.RestrictioncategoriesII:partialmapclassification.Theoretical ComputerScience.294.1-2(2003),pp.61-102

    2003

  5. [5]

    MathematicalStructuresInComputerScience.17.4(2007),pp.775-817

    Cockett,J.R.B.&Lack,S.RestrictioncategoriesIII:colimits,partiallimitsandextensivity. MathematicalStructuresInComputerScience.17.4(2007),pp.775-817

    2007

  6. [6]

    Categ..42PaperNo.6(2024),pp.102-144

    Cockett,J.R.B.&Lemay,J.-S.P.Classicaldistributiverestrictioncategories.TheoryAppl. Categ..42PaperNo.6(2024),pp.102-144

    2024

  7. [7]

    Cockett,J.R.B.&Manes,E.Booleanandclassicalrestrictioncategories.Math.Structures Comput.Sci..19.2(2009),pp.357-416

    2009

  8. [8]

    Cockett, J. R. B. & Schwarz, F. Lie groups in tangent join restriction categories. eprint: arxiv:2509.18410(2025)

    arXiv 2025

Show all 21 references
  1. [9]

    DiPaola,R.&Heller,A.Dominicalcategories: recursiontheorywithoutelements.J.Sym- bolicLogic.52.3(1987),pp.594-635

    1987

  2. [10]

    DeWolf,D.&Pronk,D.TheEhresmann-Schein-Nambooripadtheoremforinversecat- egories.TheoryAppl.Categ..33PaperNo.27(2018),pp.813-831. 63

    2018

  3. [11]

    UniversityofCalgary(2014)

    Giles,B.Aninvestigationofsometheoreticalaspectsofreversiblecomputing.PhDthesis. UniversityofCalgary(2014)

    2014

  4. [12]

    Guo,X.Products,joins,meets,andrangesinrestrictioncategories.PhDthesis.University ofCalgary(2012)

    2012

  5. [13]

    Hollings,C.TheEhresmann-Schein-Nambooripadtheoremanditssuccessors.European JournalOfPureAndAppliedMathematics.5.4(2012),pp.414-450

    2012

  6. [14]

    Jacobs,B.Semanticsofweakeningandcontraction.Ann.PureAppl.Logic.69.1(1994),pp. 73-106

    1994

  7. [15]

    Jones,P.R.Almostperfectrestrictionsemigroups.J.Algebra.445(2016),pp.193-220

    2016

  8. [16]

    Johnson,N.&Yau,D.2-dimensionalcategories.OxfordUniversityPress(2021),pp.xix+615

    2021

  9. [17]

    Kastl,J.Inversecategories.AlgebraischeModelle,KategorienUndGruppoide(1979),pp. 51-60

    1979

  10. [18]

    Lawson, M. V. Inverse semigroups. The theory of partial symmetries. World Scientific PublishingCo.,Inc.,RiverEdge,NJ.(1998),pp.xiv+411

    1998

  11. [19]

    Vol.5.GraduatetextsinMathematics(1971),pp.ix+262

    MacLane,S.Categoriesfortheworkingmathematician.Springer-Verlag,NewYork-Berlin. Vol.5.GraduatetextsinMathematics(1971),pp.ix+262

    1971

  12. [20]

    Sci..136.1(1994),pp.109-123

    Mulry,P.S.PartialmapclassifiersandpartialCartesianclosedcategories.Theoret.Comput. Sci..136.1(1994),pp.109-123

    1994

  13. [21]

    Robinson,E.&Rosolini,G.Categoriesofpartialmaps.Inform.AndComput..79.2(1988), pp.95-130. 64

    1988

Pith tools

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