Presheaves and cocompletions in formal category theory

Dylan McDermott; Nathanael Arkor

Presheaves and cocompletions in formal category theory

T0 review · 0 major / 3 minor · reviewed 2026-08-02 · deepseek-v4-flash

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

Pith's one-line read Presheaf objects exhibit free cocompletions in any strict virtual equipment when a single lifting condition holds, with new consequences for large categories enriched in monoidal categories and bicategories.

desk verdict Genuinely useful formal theory: presheaf objects give cocompletions in virtual equipments, with a real enriched payoff; just fix the 'largest'/'smallest' slip. read the letter →

arxiv 2604.22370 v2 pith:2XF56672 submitted 2026-04-24 math.CT

Nathanael Arkor , Dylan McDermott This is my paper · ORCID

classification math.CT MSC 18D7018D6518D6018A3018A3518F2018D2018N10

keywords formalcategorytheoryvirtualequipmentspresheafobjectsfreecocompletionsweightedcolimitsenrichedcategoriesbicategoricalenrichmentcolimit-smallweights

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

The paper proves that presheaf constructions and free cocompletions coincide for formal reasons, not just in familiar enriched settings. In a strict virtual equipment—an abstract framework with functors as tight cells and distributors as loose cells—it gives a three-condition theorem under which the presheaf object on an object A is the free cocompletion of A under a class of colimits. The central result is applied to categories enriched in monoidal categories and bicategories that need not be symmetric: every such enriched category, even a large one, has a free cocompletion under any class of colimit-small weights, described as the largest subcategory of small presheaves closed under those colimits and representables. A sympathetic reader should care because this fills a gap that had persisted for non-symmetric and bicategorical enrichment, and because it turns a useful classical coincidence into a theorem one can verify condition by condition.

What carries the argument

The central object is the P-presheaf object in a strict virtual equipment: an object pP[A] together with a dense loose-cell π_A: pP[A] → A that classifies exactly the loose-cells in a chosen class P. The argument is carried by three pieces: the colimit saturation operator Φ ↦ Φ*, which records all weights that generate the same colimit notion as Φ; the left-composite operation q ⊙_L p, which makes presheaf objects admit precisely the weighted colimits whose weights stay in P; and the lifting condition on π_A (all right lifts through π_A exist), which upgrades the universal property from the 2-categorical level to the loose-cell level. These assemble into a recognition theorem: a dense, fully

What would settle it

Work in a virtual equipment where A is P-admissible but π_A is not lifting: choose a loose-cell q: X → A for which no right lift q◀π_A exists. If the first two hypotheses of Theorem 7.1 can be satisfied (left-composites q ⊙_L p stay in P~= and π_A lies in the colimit saturation of Φ), then the theorem predicts that no Φ-exact extension of q to pP[A] can exist. Checking whether such a q nevertheless extends—or, dually, whether a non-lifting π_A still yields a Φ-cocompletion—would settle whether the lifting hypothesis is necessary or merely sufficient.

Watch

Extended reading notes

Core claim

At the center of the paper is a precise formal statement of when presheaf objects are free cocompletions. Working in a strict virtual equipment, the authors define a P-presheaf object for a class P of loose cells as an object pP[A] equipped with a dense projection π_A that classifies exactly the loose cells in P. Theorem 7.1 says that if left-composites of P-cells with Φ-weights stay in P up to isomorphism, π_A lies in the colimit saturation of Φ, and π_A is lifting (all right lifts through it exist), then the P-presheaf embedding A → pP[A] is the Φ-cocompletion of A. The paper then instantiates this in the virtual equipment of categories enriched in a normal virtual bicategory, proving that

Load-bearing premise

The load-bearing premise is that the projection π_A from the presheaf object back to A is lifting—every right lift through π_A exists—a condition that upgrades the cocompletion to the paper's stronger loose-cell universal property and that, in the enriched application, is only guaranteed under local completeness and right-lift assumptions on the enriching bicategory.

Editorial extensions

If this is right

The classical theorem that presheaf categories are free cocompletions now holds in any strict virtual equipment meeting the three stated conditions, so any future setting formalisable as such inherits the construction.
For a locally complete and locally cocomplete bicategory with right lifts, free Φ-cocompletions exist for all V-categories, small or large, for any class of colimit-small weights.
These cocompletions are explicitly the largest subcategory of small presheaves closed under the relevant colimits and representables, giving a concrete description of an a priori abstract universal object.
The stronger loose-cell universal property proves that the cocompletion embedding is fully faithful, ruling out pathological cocompletions that satisfy only the classical 2-categorical property.
The recognition theorems let one detect when a given dense, fully faithful Φ-atom is already a cocompletion, extending the standard enriched recognition results to the formal setting.

Reading between the lines

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

The authors list internal categories, restriction categories, and indexed enriched categories as intended future instances; a reader can test each by exhibiting a strict virtual equipment and checking the same three conditions, especially the lifting condition.
The lifting condition may be more than a technical convenience: in settings where presheaf objects exist but right lifts do not, the paper's stronger notion of cocompletion may be unattainable even though a classical 2-categorical cocompletion exists, as the paper's own example suggests.
Because the Φ*-closure construction builds cocompletions without first forming a full presheaf category, it may serve as a template for enrichment bases where the full presheaf V-category is too large to exist, even though individual presheaves and their closures are manageable.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note

read the letter

Arkor and McDermott prove a genuinely formal theorem—Theorem 7.1—that turns presheaf objects in a strict virtual equipment into free cocompletions under classes of weights, provided the presheaf projection is lifting and lies in the colimit saturation. The concrete payoff is Theorem 9.45: for a locally complete/cocomplete bicategory with right lifts, every (possibly large) enriched category has a free cocompletion under any class of colimit-small weights, given by the closure of the representables in the small presheaf category. That closes a real gap in the literature on non-symmetric monoidal and bicategorical enrichment. The paper also develops atomicity and rank in this setting and gives recognition theorems. The universal property they use is stronger than Koudenburg's 2-categorical one, and Remark 7.4 is honest about the relationship.

The proofs are long but the main line checks out. Condition (3) of Theorem 7.1—the lifting of π_A—is genuinely load-bearing, and the paper does not hide it: Section 9 discharges it under local completeness/right-lift assumptions. I read carefully for circularity and found none; the heavy self-citation is for framework lemmas, not for the target theorems. The one concrete defect is a wording slip in Theorem 9.45 (and the abstract): 'largest sub-V-category closed under Φ-colimits and representables' should be 'smallest'. Read literally, 'largest' is false—for Φ empty it would give the whole small presheaf category instead of A. The proof uses Proposition 9.28, which correctly says 'smallest', so the error is terminological, but it should be fixed.

The paper is dense and assumes a lot of formal category theory; it is not a light read. But for anyone working on enriched category theory, bicategorical enrichment, or formal category theory, this is a serious contribution. It deserves a careful referee, with the main risk being that the technical overhead hides a small error rather than a big one. I would send it to review.

Referee Report

0 major / 3 minor

Summary. The paper works in a strict virtual equipment and develops a formal theory of presheaf objects and free cocompletions. It introduces P-presheaf objects (Definition 3.2), Φ-cocompletions with a strong loose-cell universal property (Definition 6.8), and proves a central theorem: under suitable hypotheses — closure of P under left-composites with weights in Φ, membership of the presheaf projection π_A in the colimit saturation of Φ, and lifting of π_A — the P-presheaf embedding exhibits the Φ-cocompletion (Theorem 7.1). The framework is applied in Section 9 to enriched categories in normal virtual bicategories: Theorem 9.25 and Corollary 9.26 construct Φ-cocompletions via the colimit closure Φ^*-cl, and Theorem 9.45 states that, for a locally complete and locally cocomplete bicategory with right lifts, every (possibly large) V-category has a free cocompletion under any class of colimit-small weights. The paper also develops atomicity, rank, recognition theorems, adjointness results, relative pseudomonads, and the dual theory of copresheaf objects and completions.

Significance. If the results hold, they provide a substantial unification: the classical correspondence between presheaf constructions and free cocompletions is shown to be purely formal, and the enriched applications resolve a genuine gap in the literature for non-symmetric monoidal and bicategorical enrichment. The paper is also honest about the strength of its main definition: the loose-cell universal property in Definition 6.8(3) is what separates it from earlier 2-categorical treatments such as Koudenburg's, and the authors use this stronger property to prove desirable consequences such as full faithfulness of cocompletion embeddings (Lemma 6.11) and recognition theorems (Proposition 6.32). The proof of Theorem 7.1 is long but proceeds from explicit hypotheses, and Section 9 verifies those hypotheses under concrete local completeness and lifting assumptions. The most delicate premise, condition (3) of Theorem 7.1, is discharged in the enriched setting by the inductive argument in Theorem 9.25 together with Lemmas 9.15 and 9.38. I found no circularity: the target cocompletion theorems are not assumed in the development. The main defect is terminological and local.

minor comments (3)

[Abstract and Theorem 9.45] The phrase 'largest sub-V-category ... closed under Φ-weighted colimits and representable presheaves' should read 'smallest'. The proof invokes Proposition 9.28, which establishes the smallest full subcategory with this closure property; read literally, 'largest' is false. For example, when Φ is empty, the free cocompletion of A is A itself, whereas the largest subcategory of small presheaves containing the representables and closed under empty colimits would be much larger. The same correction is needed in Theorem 9.45co.
[Definition 9.21co] In the definition of the limit closure, the displayed copresheaf is written 'qn(c,1) ⊙L ··· ⊙L q1 ⊙R p' in a definition that says 'right-composites exist'. This appears to be a dualisation typo: the chain should presumably use ⊙R throughout, or the mixed convention should be explained.
[General] Several small typos remain, e.g. 'necesssary' in Remark 3.1 and 'incuding' at the start of Section 6.7. These do not affect the mathematics but should be cleaned up in the same revision.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity; central theorems are derived from definitions; only a non-circular 'largest'/'smallest' wording slip.

full rationale

The derivation chain is definitional but not circular. Theorem 7.1 is not assumed: it starts with Definition 3.2 (P-presheaf object) and Definition 6.8 (Φ-cocompletion) and proves the latter from the former by verifying the four conditions of Theorem 6.19; the proof uses Propositions 3.16, 4.8, Lemma 2.32 and Lemma 6.7, all established in the paper. In the enriched instantiation, Theorem 9.25 constructs Φ*-cl, proves Φ ≈ Φ*-cl in Lemma 9.24 via Corollary 9.14, proves lifting of each member by induction, and then applies Theorem 7.1; Proposition 9.28 then identifies the resulting subcategory. No step quotes Theorem 7.1 or Theorem 9.45 as an input. The self-citations to [AM24], [AM25b], [ASS25] are for definitions and framework lemmas (e.g. Lemma 2.21 states 'proofs ... are exactly as their correspondents in [AM24, §3] and are omitted'); these lemmas are parameter-free general statements whose assumptions do not include the target cocompletion theorems, so they are independent support rather than a circular chain. I also flag a non-circular defect: Theorem 9.45 states 'largest sub-V-category' while Proposition 9.28, the invoked result, proves the 'smallest' such subcategory; for Φ = ∅ the largest would be the whole small-presheaf category instead of A itself. This is a wording slip that should be corrected, but it does not create circularity.

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

The paper's central claims are conditional theorems; the ledger records the framework axioms (virtual equipment, lifting, local completeness) and the definitional choice of the strong cocompletion universal property. No free parameters are fitted to data and no empirical entities are postulated.

assumptions (5)

domain assumption The ambient structure is a strict virtual equipment with restrictions and loose-identities.
Throughout, the paper works in a strict virtual equipment (Definition 2.11). This is mild because every virtual equipment is equivalent to a strict one, but it is a nontrivial structural axiom.
domain assumption For the central theorem, the presheaf projection π_A is lifting (all right lifts through it exist).
Condition (3) of Theorem 7.1. This is the key technical premise enabling the loose-cell universal property; in Section 9 it is derived from local completeness/right-lift assumptions on the enrichment base.
domain assumption The enrichment base V is a locally complete and (left-)locally cocomplete bicategory with right lifts.
These hypotheses in Corollary 9.26 and Theorem 9.45 ensure the required right lifts and left-composites exist; without them the cocompletion construction may fail.
standard math Weighted colimits and cocompletions are expressed via right lifts and right extensions in virtual equipments, following Wood, Koudenburg, and the authors' prior work.
The paper builds on established formal category theory; this framework is standard in the field and is used throughout Sections 2–8.
ad hoc to paper The strict universal property in Definition 6.8(3) is adopted as the definition of Φ-cocompletion.
This is a deliberate strengthening of the classical 2-categorical universal property, justified in Section 6. It is load-bearing for the full faithfulness of the embedding and for the strong loose-cell exactness property.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Presheaves and cocompletions in formal category theory." pith.science (2026). https://pith.science/paper/2XF56672

@misc{pith2026260422370,
  author       = {Pith},
  title        = {Pith review of: Presheaves and cocompletions in formal category theory},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2XF56672}},
  note         = {Machine review of arXiv:2604.22370}
}

read the original abstract

We study the relationship between presheaf constructions and free cocompletions in the context of formal category theory, elucidating the coincidence between the two concepts in familiar settings. We show that, in a virtual equipment satisfying mild assumptions, free cocompletions under classes of weights are exhibited by presheaf constructions. We furthermore extend the theory of weighted colimits from enriched category theory to this setting, developing the concepts of atomicity and rank, and providing recognition theorems for presheaf objects, free cocompletions, and cocomplete objects. As an application of our methods, we construct free cocompletions, under arbitrary classes of colimit-small weights, of (possibly large) categories enriched in (not necessarily symmetric) monoidal categories and bicategories; this resolves a longstanding omission in the literature on enriched category theory.

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

10 extracted references · 2 linked inside Pith

[1]

‘Monads need not be endofunctors’

[ACU10] Thorsten Altenkirch, James Chapman and Tarmo Uustalu. ‘Monads need not be endofunctors’. In:International Conference on Foundations of Software Science and Computational Structures. Springer. 2010, pages 297–311 (cited on page 34). [ACU15] Thorsten Altenkirch, James Chapman and Tarmo Uustalu. ‘Monads need not be endofunctors’. In:Logical Methods i...

2010
[64]

[KK81] G

Cambridge University Press, 1982 (cited on pages 2–4, 9, 19, 24, 26, 28, 31, 34, 35, 41, 47, 49–51, 53). [KK81] G. M. Kelly and V. Koubek. ‘The large limits that all good categories admit’. In: Journal of Pure and Applied Algebra22.3 (1981), pages 253–263 (cited on pages 9, 48). [Koc67] Anders Jungersen Kock. ‘Limit monads in categories’. PhD thesis. The ...

1982
[184]

[ASS25] Nathanael Arkor, Philip Saville and Andrew Slattery.Bicategories of algebras for relative pseudomonads

Cambridge University Press, 2010 (cited on page 24). [ASS25] Nathanael Arkor, Philip Saville and Andrew Slattery.Bicategories of algebras for relative pseudomonads

2010
[194]

[Shu13] Michael A

Cam- bridge University Press, 2022 (cited on page 9). [Shu13] Michael A. Shulman. ‘Enriched indexed categories’. In:Theory and Applications of Categories28.21 (2013), pages 616–695 (cited on pages 3, 22, 23, 38, 49, 50). [Str74] Ross Street. ‘Fibrations and Yoneda’s lemma in a 2-category’. In:Category seminar. Springer. 1974, pages 104–133 (cited on page ...

2022
[391]

Springer, 1974 (cited on page 2)

Lecture Notes in Mathematics. Springer, 1974 (cited on page 2). [GS16] Richard Garner and Michael A. Shulman. ‘Enriched categories as a free cocompletion’. In:Advances in Mathematics289 (2016), pages 1–94 (cited on pages 53, 61, 62). [GU71] Peter Gabriel and Friedrich Ulmer.Lokal präsentierbare kategorien. Springer-Verlag, 1971 (cited on pages 24, 25, 53)...

1974
[1964]

[Fre68] Peter Freyd

Harper & Row New York, 1964 (cited on page 31). [Fre68] Peter Freyd. ‘Several new concepts: lucid and concordant functors, pre-limits, pre- completeness, the continuous and concordant completions of categories’. In:Category Theory, Homology Theory and Their Applications III: Proceedings of the Conference held at the Seattle Research Center of the Battelle...

1964
[1981]

Federigo Enriques

1981, pages 8–12 (cited on page 55). [BW85] Renato Betti and Robert F.C. Walters.Closed bicategories and variable category theory. Universita degli Studi di Milano, Dipartimento di Matematica “Federigo Enriques”, 1985 (cited on page 54). [BW87] R. Betti and R. F. C. Walters. ‘On completeness of locally-internal categories’. In: Journal of Pure and Applied...

1981
[2003]

[Mar97] Francisco Marmolejo

arXiv: math/0306109 (cited on page 24). [Mar97] Francisco Marmolejo. ‘Doctrines whose structure forms a fully faithful adjoint string’. In:Theory and applications of categories3.2 (1997), pages 24–44 (cited on page 37). [Par13] Robert Paré. ‘Composition of modules for lax functors’. In:Theory and Applications of Categories27.16 (2013), pages 393–444 (cite...

arXiv 1997

Show all 10 references

[2019]

[Wal81] Robert F

(cited on pages 3, 31). [Wal81] Robert F. C. Walters. ‘Sheaves and Cauchy-complete categories’. In:Cahiers de topologie et géométrie différentielle catégoriques22.3 (1981), pages 283–286 (cited on pages 2, 3). [Wal82] Robert F. C. Walters. ‘Sheaves on sites as Cauchy-complete ...

1981
[2025]

[BC82] Renato Betti and Aurelio Carboni

arXiv: 2501.12510 (cited on pages 36–38). [BC82] Renato Betti and Aurelio Carboni. ‘Cauchy-completion and the associated sheaf’. In: Cahiers de topologie et géométrie différentielle23.3 (1982), pages 243–256 (cited on page 54). [BC83] Renato Betti and Aurelio Carboni. ‘Notion ...

1982 arXiv

Pith tools

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

[1] [1]

‘Monads need not be endofunctors’

[ACU10] Thorsten Altenkirch, James Chapman and Tarmo Uustalu. ‘Monads need not be endofunctors’. In:International Conference on Foundations of Software Science and Computational Structures. Springer. 2010, pages 297–311 (cited on page 34). [ACU15] Thorsten Altenkirch, James Chapman and Tarmo Uustalu. ‘Monads need not be endofunctors’. In:Logical Methods i...

2010

[2] [64]

[KK81] G

Cambridge University Press, 1982 (cited on pages 2–4, 9, 19, 24, 26, 28, 31, 34, 35, 41, 47, 49–51, 53). [KK81] G. M. Kelly and V. Koubek. ‘The large limits that all good categories admit’. In: Journal of Pure and Applied Algebra22.3 (1981), pages 253–263 (cited on pages 9, 48). [Koc67] Anders Jungersen Kock. ‘Limit monads in categories’. PhD thesis. The ...

1982

[3] [184]

[ASS25] Nathanael Arkor, Philip Saville and Andrew Slattery.Bicategories of algebras for relative pseudomonads

Cambridge University Press, 2010 (cited on page 24). [ASS25] Nathanael Arkor, Philip Saville and Andrew Slattery.Bicategories of algebras for relative pseudomonads

2010

[4] [194]

[Shu13] Michael A

Cam- bridge University Press, 2022 (cited on page 9). [Shu13] Michael A. Shulman. ‘Enriched indexed categories’. In:Theory and Applications of Categories28.21 (2013), pages 616–695 (cited on pages 3, 22, 23, 38, 49, 50). [Str74] Ross Street. ‘Fibrations and Yoneda’s lemma in a 2-category’. In:Category seminar. Springer. 1974, pages 104–133 (cited on page ...

2022

[5] [391]

Springer, 1974 (cited on page 2)

Lecture Notes in Mathematics. Springer, 1974 (cited on page 2). [GS16] Richard Garner and Michael A. Shulman. ‘Enriched categories as a free cocompletion’. In:Advances in Mathematics289 (2016), pages 1–94 (cited on pages 53, 61, 62). [GU71] Peter Gabriel and Friedrich Ulmer.Lokal präsentierbare kategorien. Springer-Verlag, 1971 (cited on pages 24, 25, 53)...

1974

[6] [1964]

[Fre68] Peter Freyd

Harper & Row New York, 1964 (cited on page 31). [Fre68] Peter Freyd. ‘Several new concepts: lucid and concordant functors, pre-limits, pre- completeness, the continuous and concordant completions of categories’. In:Category Theory, Homology Theory and Their Applications III: Proceedings of the Conference held at the Seattle Research Center of the Battelle...

1964

[7] [1981]

Federigo Enriques

1981, pages 8–12 (cited on page 55). [BW85] Renato Betti and Robert F.C. Walters.Closed bicategories and variable category theory. Universita degli Studi di Milano, Dipartimento di Matematica “Federigo Enriques”, 1985 (cited on page 54). [BW87] R. Betti and R. F. C. Walters. ‘On completeness of locally-internal categories’. In: Journal of Pure and Applied...

1981

[8] [2003]

[Mar97] Francisco Marmolejo

arXiv: math/0306109 (cited on page 24). [Mar97] Francisco Marmolejo. ‘Doctrines whose structure forms a fully faithful adjoint string’. In:Theory and applications of categories3.2 (1997), pages 24–44 (cited on page 37). [Par13] Robert Paré. ‘Composition of modules for lax functors’. In:Theory and Applications of Categories27.16 (2013), pages 393–444 (cite...

arXiv 1997