pith. sign in

arxiv: 2606.26717 · v1 · pith:K3DUXJNNnew · submitted 2026-06-25 · 🧮 math.CT

Isoregular theories, accessible 2-categories, and free constructions

Nicola Gambino , Giacomo Tendas This is my paper

Pith reviewed 2026-06-26 02:01 UTC · model grok-4.3

classification 🧮 math.CT
keywords isoregular theoriesaccessible 2-categoriesflexible limitsfunctorial semanticsfree constructionscategory theorycategorical logic
0
0 comments X

The pith

Isoregular theories capture existential quantification up to unique isomorphism and their model 2-categories are accessible with flexible limits.

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

The paper introduces isoregular theories as a framework for expressing existential quantification up to unique isomorphism, which is common in category-theoretic constructions like limits. It develops functorial semantics for these theories and proves that the associated 2-categories of models are accessible and possess flexible limits. This approach is then applied to demonstrate that various 2-categories arising in general category theory, categorical algebra, and categorical logic can be presented as models of isoregular theories. As a result, these 2-categories are shown to be accessible with flexible limits, leading to the derivation of several new free constructions within them.

Core claim

Isoregular theories are introduced to express existential quantification up to unique isomorphism, as used to characterise universal constructions such as limits. The functorial semantics developed shows that the 2-categories of models of isoregular theories are accessible with flexible limits. Numerous 2-categories of interest are shown to be models of such theories, establishing their accessibility and flexible limits while yielding new free constructions.

What carries the argument

Isoregular theories, which allow axiomatizing properties with existential quantifiers interpreted up to unique isomorphism rather than strictly.

If this is right

  • The 2-categories of models of isoregular theories are accessible with flexible limits.
  • A number of 2-categories in general category theory are accessible with flexible limits.
  • A number of 2-categories in categorical algebra are accessible with flexible limits.
  • A number of 2-categories in categorical logic are accessible with flexible limits.
  • New free constructions exist in these 2-categories.

Where Pith is reading between the lines

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

  • The results provide a uniform method for establishing accessibility and flexible limits across different 2-categories.
  • The new free constructions may simplify computations in specific examples from categorical logic.
  • Similar presentations could be sought for 2-categories arising in related areas such as homotopy theory.

Load-bearing premise

That the proposed functorial semantics for isoregular theories accurately represents existential quantification up to isomorphism without losing the accessibility or flexible limit properties.

What would settle it

An explicit isoregular theory whose 2-category of models fails to be accessible or to have flexible limits would contradict the main result.

read the original abstract

We introduce isoregular theories, in which it is possible to express existential quantification up to unique isomorphism, as typically used to characterise category-theoretic universal constructions, such as limits. We then develop a functorial semantics for isoregular theories and prove that their 2-categories of models are accessible with flexible limits. We apply these results by showing that a number of 2-categories of interest in general category theory, categorical algebra, and categorical logic are models of isoregular theories, thereby establishing that they are accessible 2-categories with flexible limits and obtaining a number of new free constructions.

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 / 2 minor

Summary. The paper introduces isoregular theories, which permit expressing existential quantification up to unique isomorphism (as used for universal constructions like limits). It develops functorial semantics for these theories and proves that the resulting 2-categories of models are accessible and admit flexible limits. The authors then exhibit a range of 2-categories arising in general category theory, categorical algebra, and categorical logic as models of isoregular theories, thereby establishing their accessibility with flexible limits and deriving new free constructions.

Significance. If the central claims hold, the work supplies a uniform syntactic framework for establishing accessibility and the existence of free constructions across many 2-categories of interest; the concrete applications constitute a genuine strength by linking the abstract theory to established examples in the literature.

minor comments (2)
  1. The abstract asserts the existence of proofs for accessibility and flexible-limit preservation but supplies no derivation outline or key lemma references; a one-sentence pointer to the relevant theorem number in the introduction would improve readability.
  2. Notation for the 2-categorical enrichment and the precise meaning of 'flexible limits' should be recalled or cross-referenced at the first use in the semantics section to aid readers unfamiliar with the 2-categorical setting.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of the paper, recognition of its significance, and recommendation of minor revision. No major comments were provided in the report.

Circularity Check

0 steps flagged

No significant circularity; derivation self-contained

full rationale

The paper introduces isoregular theories via new syntax for existential quantification up to isomorphism, then proves that the associated 2-categories of models are accessible and admit flexible limits using standard 2-categorical arguments. Concrete applications consist of exhibiting explicit isoregular theories whose models recover known 2-categories; these are direct constructions rather than predictions or renamings that reduce to the input data. No self-definitional equations, fitted parameters presented as predictions, or load-bearing self-citations appear in the derivation chain. The central claims rest on the internal definitions and functorial semantics, which are independent of prior results by the same authors.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The paper introduces a new class of theories and associated semantics; background assumptions are standard 2-category theory.

axioms (1)
  • standard math Standard axioms and definitions of 2-category theory and accessible categories
    Invoked as background for the new definitions and theorems.
invented entities (1)
  • isoregular theory no independent evidence
    purpose: To express existential quantification up to unique isomorphism
    Newly defined concept whose properties are then proved.

pith-pipeline@v0.9.1-grok · 5616 in / 1037 out tokens · 29671 ms · 2026-06-26T02:01:13.143119+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

207 extracted references · 9 canonical work pages

  1. [1]

    Uemura , date-added =

    T. Uemura , date-added =. A general framework for the semantics of type theory , volume =. Mathematical Structures in Computer Science , pages =

  2. [2]

    Jacobs , date-added =

    B. Jacobs , date-added =. Categorical logic and type theory , year =

  3. [3]

    Taylor , date-added =

    P. Taylor , date-added =. Recursive domains, indexed category theory and polymorphism , year =

  4. [4]

    Joyal , date-added =

    A. Joyal , date-added =. Notes on clans and tribes , year =

  5. [5]

    Gran , booktitle =

    M. Gran , booktitle =. An introduction to regular categories , year =

  6. [6]

    , date-modified =

    Giusto, A. , date-modified =. Fibrations with comprehensions and their completions , year =. Master Thesis, Universit\`a degli

  7. [7]

    Aczel and N

    P. Aczel and N. Gambino , date-added =. The generalised type-theoretic intepretation of constructive set theory , volume =. Journal of Symbolic Logic , number =

  8. [8]

    Nordstr\"om and K

    B. Nordstr\"om and K. Petersson and J. Smith , booktitle =. Martin-

  9. [9]

    Makkai , date-added =

    M. Makkai , date-added =. Generalised sketches as a framework for completeness theorem. Part. Journal of Pure and Applied Algebra , number =

  10. [10]

    Street , date-added =

    R. Street , date-added =. Two-dimensional sheaf theory , volume =. Journal of Pure and Applied Algebra , pages =

  11. [11]

    Voevodsky , date-added =

    V. Voevodsky , date-added =. An experimental library of formalised. Mathematical Structures in Computer Science , number =

  12. [12]

    Homotopy Type Theory: Univalent Foundations of Mathematics , year =

    The. Homotopy Type Theory: Univalent Foundations of Mathematics , year =

  13. [13]

    Lack , date-added =

    S. Lack , date-added =. Homotopy-theoretic aspects of 2 -monads , volume =. Journal of Homotopy and Related Structures , number =

  14. [14]

    G. M. Kelly and I. Le Creurer , date-added =. On the monadicity over graphs of categories with limits , volume =. Cahiers de Topologie et G\'

  15. [15]

    G. M. Kelly and S. Lack , date-added =. On the monadicity of categories with chosen colimits , volume =. Theory and Applications of Categories , number =

  16. [16]

    Power and E

    J. Power and E. Robinson , date-added =. A characterization of pie limits , volume =. Mathematical Proceedings of the Cambridge Philosophical Society , pages =

  17. [17]

    Di Liberti and A

    I. Di Liberti and A. Osmond , date-added =. Bi-accessible and bipresentable 2-categories , volume =. Applied Categorical Structures , number =

  18. [18]

    Kock , date-added =

    A. Kock , date-added =. Monads whose structures are adjoint to units , volume =. Journal of Pure and Applied Algebra , pages =

  19. [19]

    Hyland and J

    M. Hyland and J. Power , date-added =. The category theoretic understanding of universal algebra:. Electronic Notes in Theoretical Computer Science , pages =

  20. [20]

    G. M. Kelly and S. Lack , date-added =. On property-like structures , volume =. Theory and Applications of Categories , number =

  21. [21]

    Blackwell and G

    R. Blackwell and G. M. Kelly and A. J. Power , date-added =. Two-dimensional monad theory , volume =. Journal of Pure and Applied Algebra , pages =

  22. [22]

    G. M. Kelly , date-added =. Elementary observations on 2-categorical limits , volume =. Bulletin of the Australian Mathematical Society , pages =

  23. [23]

    , publisher =

    Johnstone, P. , publisher =. Sketches of an Elephant: A Topos Theory Compendium , year =

  24. [24]

    Locally presentable and accessible categories , SERIES =

    Ad\'. Locally presentable and accessible categories , url =. 1994 , bdsk-url-1 =. doi:10.1017/CBO9780511600579 , isbn =

    work page doi:10.1017/cbo9780511600579 1994

  25. [25]

    and Par\'e, R

    Makkai, M. and Par\'e, R. , publisher =. Accessible Categories: The Foundations of Categorical Model Theory , volume =

  26. [26]

    and Reyes, G.E

    Makkai, M. and Reyes, G.E. , publisher =. First Order Categorical Logic , year =

  27. [27]

    Kelly, G. M. , publisher =. Basic Concepts of Enriched Category Theory , year =

  28. [28]

    , publisher =

    Prest, M. , publisher =. Definable Additive Categories: Purity and Model Theory , year =

  29. [29]

    and Grillet, P.A

    Barr, M. and Grillet, P.A. and van Osdol, D.H. , publisher =. Exact Categories and Categories of Sheaves , year =

  30. [30]

    , publisher =

    Borceux, F. , publisher =. Handbook of Categorical Algebra: Volume 2, Categories and Structures , year =

  31. [31]

    Lokal pr\"

    Gabriel, Peter and Ulmer, Friedrich , mrclass =. Lokal pr\"

  32. [32]

    and Zisman, M

    Gabriel, P. and Zisman, M. , publisher =. Calculus of fractions and homotopy theory , year =

  33. [33]

    and Schapira, P

    Kashiwara, M. and Schapira, P. , publisher =. Categories and Sheaves , year =

  34. [34]

    2009 , PAGES =

    Lurie, J. , date-modified =. Higher topos theory , url =. 2009 , bdsk-url-1 =. doi:10.1515/9781400830558 , isbn =

    work page doi:10.1515/9781400830558 2009

  35. [35]

    , booktitle =

    Lack, S. , booktitle =. A 2-categories companion , year =

  36. [36]

    Lawvere, F. W. , publisher =. Category theory over a base topos , year =

  37. [37]

    Lawvere, F. W. , publisher =. Functorial Semantics of Algebraic Theories , year =

  38. [38]

    , publisher =

    Hovey, M. , publisher =. Model Categories , year =

  39. [39]

    Bird, G. J. , publisher =

  40. [40]

    Toposes, Triples, and Theories , year =

    Barr, Michael and Wells, Charles , publisher =. Toposes, Triples, and Theories , year =

  41. [41]

    Quantum Groups: A Path to Current Algebra , year =

    Street, Ross , collection =. Quantum Groups: A Path to Current Algebra , year =. doi:10.1017/CBO9780511618505 , place =

    work page doi:10.1017/cbo9780511618505

  42. [42]

    Le lien entre la logique et la g

    Gerner, Matthias , publisher =. Le lien entre la logique et la g

  43. [43]

    Pedicchio, M. C. and Tholen, W. , collection =. Categorical Foundations: Special Topics in Order, Topology, Algebra, and Sheaf Theory , year =. doi:10.1017/CBO9781107340985 , place =

    work page doi:10.1017/cbo9781107340985

  44. [44]

    Elements of ∞-Category Theory , year =

    Riehl, Emily and Verity, Dominic , collection =. Elements of ∞-Category Theory , year =. doi:10.1017/9781108936880 , place =

    work page doi:10.1017/9781108936880

  45. [45]

    , publisher =

    Lamarche, F. , publisher =. Modelling polymorphism with categories , year =

  46. [46]

    , publisher =

    Bourke, J. , publisher =. Codescent objects in 2-dimensional universal algebra , year =

  47. [47]

    Representace konkr\'

    Rosick\'. Representace konkr\'

  48. [48]

    Triangulated categories , year =

    Neeman, Amnon , number =. Triangulated categories , year =

  49. [49]

    Abelian categories , volume =

    Freyd, Peter J , publisher =. Abelian categories , volume =

  50. [50]

    Handbook of categorical algebra: volume 1, Basic category theory , volume =

    Borceux, Francis , publisher =. Handbook of categorical algebra: volume 1, Basic category theory , volume =

  51. [51]

    Kelly, G. M. , booktitle =. Doctrinal adjunction , year =

  52. [52]

    Exact categories , year =

    Barr, Michael , publisher =. Exact categories , year =

  53. [53]

    Algebraic theories: a categorical introduction to general algebra , volume =

    Ad. Algebraic theories: a categorical introduction to general algebra , volume =

  54. [54]

    , journal =

    Makkai, M. , journal =. A Theorem on

  55. [55]

    and Rosick\'

    Kuber, A. and Rosick\'. Definable Categories , volume =. Journal of Pure and Applied Algebra , number =

  56. [56]

    , journal =

    Chikhladze, D. , journal =. Barr's Embedding Theorem for Enriched Categories , volume =

  57. [57]

    , journal =

    Dupont, P. , journal =. Projectivity of Sheaves on a Locale and of Free Modules , volume =

  58. [58]

    Transactions of the American Mathematical Society , title =

    Ad. Transactions of the American Mathematical Society , title =

  59. [59]

    More on Injectivity in Locally Presentable Categories , volume =

    Rosick\'. More on Injectivity in Locally Presentable Categories , volume =. Theory and Applications of Categories , number =

  60. [60]

    , journal =

    Fawcett, B. , journal =. A Canonical Factorization for Graph Homomorphisms , volume =

  61. [61]

    Kelly, G. M. , issn =. Structures defined by finite limits in the enriched context. Cahiers de Topologie et G\'

  62. [62]

    , journal =

    Barr, M. , journal =. Representation of Categories , volume =

  63. [63]

    https://www.tu-braunschweig.de/Medien-DB/iti/cor.pdf , title =

    Ad. https://www.tu-braunschweig.de/Medien-DB/iti/cor.pdf , title =

  64. [64]

    , date-modified =

    Lurie, J. , date-modified =. Ultracategories , year =

  65. [65]

    and Rosick\'

    Lack, S. and Rosick\'. Enriched weakness , volume =. Journal of Pure and Applied Algebra , pages =

  66. [66]

    and Lack, S

    Garner, R. and Lack, S. , doi =. Lex colimits , url =. Journal of Pure and Applied Algebra , mrclass =. 2012 , bdsk-url-1 =

    2012

  67. [67]

    Some remarks on 2-categorical algebra

    B\'. Some remarks on 2-categorical algebra. Bulletin de la Soci

  68. [68]

    and Rajani, R

    Prest, M. and Rajani, R. , journal =. Structure sheaves of definable additive categories , volume =

  69. [69]

    , journal =

    Carboni, A and Celia Magno, R. , journal =. The Free Exact Category on a Left Exact One , year =

  70. [70]

    and Vitale, E

    Carboni, A. and Vitale, E. M. , doi =. Regular and exact completions , url =. Journal of Pure and Applied Algebra , mrclass =. 1998 , bdsk-url-1 =

    1998

  71. [71]

    , journal =

    Hu, H. , journal =. Flat Functors and Free Exact Categories , year =

  72. [72]

    and Tholen, W

    Hu, H. and Tholen, W. , journal =. A Note on Free Regular and Exact Completions and Their Infinitary Generalizations , year =

  73. [73]

    , journal =

    Makkai, M. , journal =. Stone Duality for First Order Logic , volume =

  74. [74]

    , journal =

    Freyd, P. , journal =. Aspects of Topoi , volume =

  75. [75]

    , journal =

    Day, B. , journal =. On closed categories of functors , volume =

  76. [76]

    On Sifted Colimits and Generalized Varieties , volume =

    Ad. On Sifted Colimits and Generalized Varieties , volume =. Theory and Applications of Categories , number =

  77. [77]

    and Kelly, G.M

    Janelidze, G. and Kelly, G.M. , journal =. A Note on Actions of a Monoidal Category , volume =

  78. [78]

    and Street, R

    Day, B. and Street, R. , journal =. Localisation of locally presentable categories , volume =

  79. [79]

    Algebraic Theories of Quasivarieties , volume =

    Ad. Algebraic Theories of Quasivarieties , volume =. Journal of Algebra , pages =

  80. [80]

    , journal =

    Day, B. , journal =. A reflection theorem for closed categories , volume =

Showing first 80 references.