pith. sign in

arxiv: 2510.08861 · v3 · submitted 2025-10-09 · 🧮 math.CT

Presheaves on lax double functors; or, Instances of models of double theories

Kevin Carlson , Evan Patterson This is my paper

Pith reviewed 2026-05-18 08:47 UTC · model grok-4.3

classification 🧮 math.CT MSC 18D0518C10
keywords presheaveslax double functorsdouble theoriesinstancesdiscrete opfibrationselements correspondenceLawvere theoriescollage construction
0
0 comments X

The pith

Instances of models of double theories are equivalent to discrete opfibrations over the model via an elements correspondence.

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

The paper defines a notion of instance for a lax double functor valued in sets, which serves as a model of a double theory. This uniform definition covers examples including categories, profunctors, monads, monoidal categories, and multicategories, recovering multifunctors into sets in the last case. Instances are shown to be equivalent to modules from the terminal model with trivial left action, or to loose natural transformations from the terminal model. A new notion of discrete opfibration between models is introduced along with a comprehensive factorization system, yielding an equivalence between the category of instances and the category of discrete opfibrations over any given model X. Properties of these instance categories are then derived using a collage construction characterized as a lax colimit.

Core claim

We introduce a notion of (co)presheaf on a lax double functor X, called an instance. Instances of X are equivalent to modules from the terminal model I to X with trivial left action, or to loose natural transformations from I to X. Discrete opfibrations between models of a double theory admit a comprehensive factorization system, and an elements correspondence establishes an equivalence between the category of instances of X and the category of discrete opfibrations over X. The resulting categories of instances are described via the collage construction, which is a lax colimit of a model.

What carries the argument

Instance, defined as a (co)presheaf on a lax double functor modeling a double theory; equivalently realized via modules with trivial left action or loose natural transformations from the terminal model I.

If this is right

  • A single definition applies to instances of categories, profunctors, monads, monoidal categories, and multicategories.
  • Multifunctors into the category of sets arise as the instances of the double theory for multicategories.
  • Categories of instances inherit properties from the collage construction viewed as a lax colimit.
  • Discrete opfibrations between models form a category with a comprehensive factorization system.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The equivalence may simplify explicit computations of instances in concrete double theories by reducing them to opfibration data.
  • The approach could extend the treatment of presheaves to other variants of double-categorical or higher-categorical logic.
  • Loose natural transformations and modules provide alternative computational routes when direct presheaf descriptions are cumbersome.

Load-bearing premise

The existing theory of double categories and lax double functors is developed enough to support the definitions of instances, discrete opfibrations, the factorization system, and the elements correspondence without further foundational work.

What would settle it

A concrete model X of a double theory together with an instance that fails to correspond to any discrete opfibration over X under the elements correspondence.

read the original abstract

We introduce a notion of (co)presheaf on a lax double functor $X$, which we generally call an instance. In the terminology of double-categorical logic, a lax double functor valued in sets, possibly preserving finite products, is called a model of a double (Lawvere) theory. By varying the double theory, we uniformly define a well-behaved notion of instances of categories, profunctors, monads, monoidal categories, multicategories, and more, and we recover for instance the multifunctors into the category of sets in the last example. We show that instances of $X$ can be described either in terms of modules from the terminal model $I$ to $X,$ satisfying an additional condition on triviality of the left action, or as loose natural transformations from $I$ to $X.$ We propose a notion of discrete opfibration between models of a double theory, establish a comprehensive factorization system, and prove an elements correspondence giving an equivalence between the category of instances of and the category of discrete opfibrations over a model $X.$ We describe properties of the resulting categories of instances, relying on a "collage" construction which we characterize as a lax colimit of a model of a double theory. An appendix gives a detailed treatment of certain morphisms of lax functors relevant also for bicategory theory: (loose) transformations versus modules and modifications versus modulations.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 4 minor

Summary. The manuscript introduces the notion of an instance as a (co)presheaf on a lax double functor X, where lax double functors valued in sets (possibly preserving finite products) are models of double (Lawvere) theories. By varying the underlying double theory, it uniformly defines instances for categories, profunctors, monads, monoidal categories, multicategories and related structures, recovering multifunctors into Set in the last case. Central results establish that instances of X are equivalently described either as modules from the terminal model I to X with trivial left action or as loose natural transformations from I to X; a notion of discrete opfibration between models is proposed, a comprehensive factorization system is established, and an elements correspondence is proved that equates the category of instances of X with the category of discrete opfibrations over X. Properties of the resulting categories are derived using a collage construction characterized as a lax colimit, and an appendix compares (loose) transformations versus modules and modifications versus modulations for lax functors.

Significance. If the stated equivalences and factorization system hold, the paper supplies a uniform, well-behaved framework for instances/presheaves across a range of categorical structures by varying the double theory, thereby unifying examples such as multifunctors into Set. The elements correspondence and comprehensive factorization system, together with the lax-colimit characterization of the collage, constitute concrete technical advances that build directly on existing lax double functor theory without new foundational axioms. The detailed appendix treatment of transformations versus modules is a further strength that is relevant beyond the present setting to bicategory theory. These contributions have the potential to support further work in double-categorical logic and semantics.

minor comments (4)
  1. The statement of the elements correspondence (around the main theorem equating instances and discrete opfibrations) would benefit from an explicit diagram or short example showing how the correspondence acts on morphisms, to make the equivalence more immediately verifiable.
  2. Notation for the terminal model I and the triviality condition on the left action is introduced early but used throughout; a consolidated summary table or paragraph collecting all such standing assumptions would improve readability for readers not already immersed in double category theory.
  3. The appendix treatment of transformations versus modules is valuable, but a brief forward reference in the main text (e.g., near the definition of loose natural transformations) would help readers locate the more detailed comparison when needed.
  4. A small number of typographical inconsistencies appear in the use of 'lax' versus 'loose' qualifiers on natural transformations; a uniform convention should be adopted and checked throughout.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive and encouraging report on our manuscript. The recommendation for minor revision is noted, and we are prepared to make any necessary adjustments. Since the report does not raise any specific major comments, we have no individual points to respond to at this time.

Circularity Check

0 steps flagged

No significant circularity; derivations self-contained in standard theory

full rationale

The paper defines instances of models of double theories as (co)presheaves on lax double functors, equivalently via modules from the terminal model I (with trivial left action) or loose natural transformations from I. It introduces discrete opfibrations, a factorization system, and an elements correspondence establishing equivalence to the category of instances. These rest on standard lax double functor and double category theory without reducing any central claim to a self-definition, fitted input renamed as prediction, or load-bearing self-citation. The collage construction is characterized as a lax colimit using existing notions. No equations or equivalences are tautological by construction; all build outward from the new definitions applied to prior independent theory. This is the normal case of a foundational category-theory paper with independent content.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

The central claims rest on standard background axioms of double categories together with the newly introduced definitions of instances, discrete opfibrations, and the collage construction.

axioms (1)
  • standard math Standard axioms and properties of double categories, lax double functors, and double (Lawvere) theories as developed in prior category theory literature.
    The paper invokes these to define models and instances.
invented entities (2)
  • Instance (presheaf on a lax double functor) no independent evidence
    purpose: To provide a uniform notion of presheaf-like objects for models of different double theories.
    This is a newly defined concept in the paper.
  • Discrete opfibration between models of a double theory no independent evidence
    purpose: To establish a factorization system and elements correspondence with instances.
    Newly proposed notion in the paper.

pith-pipeline@v0.9.0 · 5787 in / 1503 out tokens · 67880 ms · 2026-05-18T08:47:17.784433+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

26 extracted references · 26 canonical work pages · 2 internal anchors

  1. [1]

    Cahiers de Topologie et Géométrie Différentielle Catégoriques40(3), 162–220 (1999) 1

    Grandis, M., Pare, R.: Limits in double categories. Cahiers de Topologie et Géométrie Différentielle Catégoriques40(3), 162–220 (1999) 1

    work page 1999

  2. [2]

    Reprints in Theory and Applications of Categories (20), 1–266 (2011)

    Verity, D.: Enriched categories, internal categories and change of base. Reprints in Theory and Applications of Categories (20), 1–266 (2011). Originally published as Ph.D. thesis, Cambridge University, 1992 1 49

    work page 2011

  3. [3]

    Theory and Applications of Categories25(17), 436–489 (2011) 2, 7

    Paré, R.: Yoneda theory for double categories. Theory and Applications of Categories25(17), 436–489 (2011) 2, 7

    work page 2011

  4. [4]

    Theory and Applications of Categories27(16), 393–444 (2013) 2

    Paré, R.: Composition of modules for lax functors. Theory and Applications of Categories27(16), 393–444 (2013) 2

    work page 2013

  5. [5]

    Advances in Mathematics444, 109630 (2024) https://doi.org/10.1016/j.aim.2024.109630 2310.05384 2, 3, 4, 7, 15, 37, 39, 41, 45, 49

    Lambert, M., Patterson, E.: Cartesian double theories: A double-categorical framework for categorical doctrines. Advances in Mathematics444, 109630 (2024) https://doi.org/10.1016/j.aim.2024.109630 2310.05384 2, 3, 4, 7, 15, 37, 39, 41, 45, 49

    work page doi:10.1016/j.aim.2024.109630 2024

  6. [6]

    Compositionality6(2) (2024) https://doi.org/10.32408/ compositionality-6-2 2301.01445 2

    Aduddell, R., Fairbanks, J., Kumar, A., Ocal, P.S., Patterson, E., Shapiro, B.T.: A compositional account of motifs, mechanisms, and dynamics in biochemical regulatory networks. Compositionality6(2) (2024) https://doi.org/10.32408/ compositionality-6-2 2301.01445 2

    work page arXiv 2024

  7. [7]

    Baez, J.C., Chaudhuri, A.: Graphs with polarities (2025) 2506.23375 2

    work page arXiv 2025

  8. [8]

    Ologs: a categorical framework for knowledge representation

    Spivak, D.I., Kent, R.E.: Ologs: A categorical framework for knowledge representa- tion. PloS One7(1), 24274 (2012) https://doi.org/10.1371/journal.pone.0024274 1102.1889 2

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.1371/journal.pone.0024274 2012

  9. [9]

    Theory and Applications of Categories32(16), 547–619 (2017) 1602.03501 3, 44, 45, 46

    Schultz, P., Spivak, D.I., Vasilakopoulou, C., Wisnesky, R.: Algebraic databases. Theory and Applications of Categories32(16), 547–619 (2017) 1602.03501 3, 44, 45, 46

    work page arXiv 2017

  10. [10]

    Compositionality4(5) (2022) https://doi.org/10.32408/ compositionality-4-5 2106.04703 3, 15

    Patterson, E., Lynch, O., Fairbanks, J.: Categorical data structures for technical computing. Compositionality4(5) (2022) https://doi.org/10.32408/ compositionality-4-5 2106.04703 3, 15

    work page arXiv 2022

  11. [11]

    A unified framework for generalized multicategories

    Cruttwell, G.S.H., Shulman, M.A.: A unified framework for generalized multicate- gories. Theory and Applications of Categories24(21), 580–655 (2010) 0907.2460 3, 8

    work page internal anchor Pith review Pith/arXiv arXiv 2010

  12. [12]

    Bulletin of the American Mathematical Society79(5), 936–941 (1973) https://doi.org/10

    Street, R., Walters, R.F.C.: The comprehensive factorization of a functor. Bulletin of the American Mathematical Society79(5), 936–941 (1973) https://doi.org/10. 1090/S0002-9904-1973-13268-9 4

    work page 1973

  13. [13]

    Arlin, K., Fairbanks, J., Hosgood, T., Patterson, E.: The diagrammatic presenta- tion of equations in categories (2024) 2401.09751 4

    work page arXiv 2024

  14. [14]

    Riehl and D

    Riehl, E., Verity, D.: Elements of∞-Category Theory. Cambridge University Press, ??? (2022). https://doi.org/10.1017/9781108936880 4

    work page doi:10.1017/9781108936880 2022

  15. [15]

    Theory and Applications of Categories35(31), 1159–1207 (2020) 5

    Moeller, J., Vasilakopoulou, C.: Monoidal grothendieck construction. Theory and Applications of Categories35(31), 1159–1207 (2020) 5

    work page 2020

  16. [16]

    Applied Categorical Structures29, 249–265 (2021) https://doi.org/10

    Cigoli, A.S., Mantovani, S., Metere, G.: Discrete and conservative factorizations 50 in Fib(b). Applied Categorical Structures29, 249–265 (2021) https://doi.org/10. 1007/s10485-020-09615-9 1909.10822 5

    work page arXiv 2021

  17. [17]

    Journal of Algebra663, 399–434 (2025) https://doi.org/10.1016/j.jalgebra.2024.08.040 8

    Arkor, N., McDermott, D.: Relative monadicity. Journal of Algebra663, 399–434 (2025) https://doi.org/10.1016/j.jalgebra.2024.08.040 8

    work page doi:10.1016/j.jalgebra.2024.08.040 2025

  18. [18]

    Bulletin of the Australian Math- ematical Society22(1), 1–83 (1980) https://doi.org/10.1017/S0004972700006353 22

    Kelly, G.M.: A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on. Bulletin of the Australian Math- ematical Society22(1), 1–83 (1980) https://doi.org/10.1017/S0004972700006353 22

    work page doi:10.1017/s0004972700006353 1980

  19. [19]

    PhD thesis, Dalhousie University (2018) 36

    Aleiferi, E.: Cartesian double categories with an emphasis on characterizing spans. PhD thesis, Dalhousie University (2018) 36

    work page 2018

  20. [20]

    Patterson, E.: Products in double categories, revisited (2024) 2401.08990 36, 44

    work page arXiv 2024

  21. [21]

    Cambridge University Press, ??? (2010)

    Adámek, J., Rosický, J., Vitale, E.M.: Algebraic Theories: A Categorical Intro- duction to General Algebra. Cambridge University Press, ??? (2010). https: //doi.org/10.1017/CBO9780511760754 39

    work page doi:10.1017/cbo9780511760754 2010

  22. [22]

    Theory and Applications of Categories 44(28), 826–868 (2025) 2409.10150 41, 42

    Pisani, C.: Unbiased multicategory theory. Theory and Applications of Categories 44(28), 826–868 (2025) 2409.10150 41, 42

    work page arXiv 2025

  23. [23]

    Draft for AARMS Summer School 2016 (2016)

    Shulman, M.: Categorical logic from a categorical point of view. Draft for AARMS Summer School 2016 (2016). https://mikeshulman.github.io/catlog/catlog.pdf 41

    work page 2016

  24. [24]

    Cambridge University Press, ??? (2004)

    Leinster, T.: Higher Operads, Higher Categories. Cambridge University Press, ??? (2004). https://doi.org/10.1017/CBO9780511525896 42, 43

    work page doi:10.1017/cbo9780511525896 2004

  25. [25]

    Theory and Applications of Categories40(5), 130–179 (2024) 2306.06436 44

    Paré, R.: Retrocells. Theory and Applications of Categories40(5), 130–179 (2024) 2306.06436 44

    work page arXiv 2024

  26. [26]

    Cambridge University Press, ??? (1994)

    Adamek, J., Rosicky, J.: Locally Presentable and Accessible Categories. Cambridge University Press, ??? (1994). https://doi.org/10.1017/CBO9780511600579 49 51

    work page doi:10.1017/cbo9780511600579 1994