REVIEW 3 major objections 3 minor 20 references
Double-functorial representation of regular hyperdoctrines
T0 review · 3 major / 3 minor · reviewed 2026-08-05 · deepseek-v4-flash
Pith's one-line read The paper claims that regular hyperdoctrines—the categorical semantics of regular logic—correspond exactly to certain structure-preserving maps between double categories, with the Frobenius condition carried by their monoidal structure.
desk verdict The abstract describes a plausible and genuinely useful double-categorical characterization of Frobenius for regular hyperdoctrines, but with the full text corrupted to unreadable mojibake the claim is unverified and the manuscript as supplied cannot be refereed. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The load-bearing machinery consists of two double categories: $\mathbf{Span}$, whose objects are sets or objects of a base category and whose arrows are spans $A\leftarrow X\to B$, and $\mathbf{Quint}$, whose cells are quintets of morphisms forming a commuting square. The correspondence is carried by a pseudo double functor from spans to quintets together with a monoidal structure on each side. The central mechanism is the monoidal laxator—a comparison cell between the functor of a tensor and the tensor of the functor—and the requirement that these laxators be companion commuter cells, meaning they coherently relate vertical and horizontal structure through the functor. These laxators are ex
What would settle it
Take a known Beck–Chevalley bifibration that fails the Frobenius condition, form its pseudo double functor into quintets, and check whether it admits a lax symmetric monoidal structure whose laxators are companion commuter cells. A single example with such a structure would refute the correspondence; a single example without it is evidence for the claim that the monoidal laxators encode Frobenius.
Extended reading notes
Core claim
The central claim is a correspondence. On one side sits a (generalised) regular hyperdoctrine; on the other side sits a lax symmetric monoidal pseudo double functor $F:\mathbf{Span}\to\mathbf{Quint}$ in which the monoidal laxators are companion commuter cells. The paper argues that the Beck–Chevalley condition is exactly pseudofunctoriality of $F$, and the Frobenius condition is exactly the existence and coherence of the monoidal laxators. Thus the word "regular" in "regular hyperdoctrine" is not extra baggage tacked onto a fibration; it is the monoidal structure of a double functor. This reformulation is what lets the paper discuss compositionality of regular hyperdoctrines and propose a no
Load-bearing premise
The result depends on the class of "certain" lax symmetric monoidal pseudo double functors being defined independently of hyperdoctrines, so that the Frobenius condition is genuinely captured by the double-categorical data rather than built into the class by construction.
Editorial extensions
If this is right
- If the correspondence is correct, Frobenius is not a condition to check after constructing a Beck–Chevalley bifibration: it is the data of a monoidal structure on the associated double functor.
- Composition of regular hyperdoctrines can be studied as composition of these double functors, which gives a direct way to paste logical systems along interfaces.
- The double-categorical reformulation yields a candidate definition of regular double hyperdoctrines, opening a double-categorical version of regular logic.
- The associated graphical calculus gives a form of graphical regular logic in which system specifications can be represented as diagrams and composed operadically, as in port-plugging systems.
Reading between the lines
- Inference: if the correspondence is genuine, it supplies a recognition principle: to prove a fibration is a regular hyperdoctrine, it suffices to construct companion-commuter laxators, which is likely easier diagrammatically than checking the Frobenius identities by hand.
- Inference: the same double-functor encoding may adapt to other logical fragments—coherent logic, first-order logic with equality, or modal logics—by changing the target double category or the shape of the companion cells.
- Inference: the "certain" qualifier in the correspondence suggests a possible hierarchy: as additional logical properties are added, they should appear as additional coherence cells on the same double functor, making the hierarchy of logics a hierarchy of double-categorical structures.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper claims a double-categorical characterization of (generalised) regular hyperdoctrines: they are equivalent to certain lax symmetric monoidal pseudo double functors from spans to quintets, with the monoidal laxators supplying companion commuter cells in the sense of Paré. This is presented as extending the known correspondence between pseudofunctors from spans and Beck-Chevalley bifibrations to include the Frobenius property, and as a step toward a compositional, graphical regular logic. The abstract also announces an application to systems specifications that compose operadically. Unfortunately, the supplied full text is almost entirely corrupted and unreadable, so the actual definitions, theorems, and proofs cannot be inspected.
Significance. If the stated correspondence is correct and non-tautological, it would be a valuable contribution to categorical logic and double category theory: it would give a purely double-categorical description of regular hyperdoctrines, including the Frobenius condition, and would connect to compositionality via operadic structures. The claimed application to graphical regular logic is intriguing. However, because the full text is unreadable, the significance cannot currently be assessed beyond the abstract-level claim.
major comments (3)
- [Full text (all sections)] The provided manuscript is severely corrupted: most text is garbled mojibake, with only isolated fragments, diagrams, and the abstract readable. No definition, theorem, proof, or equation can be verified. This blocks any substantive review. The authors must provide a clean, complete version before the technical content can be evaluated.
- [Abstract] The abstract asserts an equivalence between (generalised) regular hyperdoctrines and 'certain lax symmetric monoidal pseudo double functors from spans to quintets whose monoidal laxators provide companion commuter cells.' As stated, this risks being definitionally circular: if the class of 'certain' functors and the property of 'companion commuter cells' are chosen to encode exactly the Frobenius condition, the correspondence may hold by construction rather than as a substantive theorem. The manuscript needs to define the target-side class explicitly, independently of hyperdoctrines, and show that the condition on laxators is not merely a restatement of the Frobenius property. This is load-bearing for the main claim.
- [Unspecified (to be identified in clean version)] The claimed equivalence must be a 2-categorical or double-categorical equivalence, and the coherence conditions are exactly where such equivalences typically hide gaps. The abstract does not indicate what the 1-cells and 2-cells on each side are, nor how the equivalence acts on them. The manuscript must spell out the full structure: the double categories involved, the notion of pseudo double functor, the coherence axioms, and the equivalence (or adjoint equivalence) at the level of objects, tight and loose cells. Without these, the central claim is not checkable.
minor comments (3)
- [Abstract] The phrase 'It is well-known' lacks a citation. Please cite the relevant work on pseudofunctors from spans and Beck-Chevalley bifibrations, as well as Dawson–Paré–Pronk.
- [Abstract] The abstract mentions a hinted 'new notion of regular double hyperdoctrine' but gives no definition. Even a brief indication of what this notion is would help the reader.
- [Abstract] The application to port-plugging systems is vague; a concrete example or a reference to the intended compositionality result would clarify the scope.
Circularity Check
No circularity demonstrated from the available text; the main equivalence is stated between established independent structures, and no reduction of a prediction to a fitted input or self-citation chain is visible.
full rationale
The central claim is that (generalised) regular hyperdoctrines correspond to certain lax symmetric monoidal pseudo double functors from spans to quintets whose monoidal laxators provide companion commuter cells. The correspondence is presented as a theorem about two existing double-categorical constructions (spans, quintets, companions in Pare's sense), not as a definitional restatement. The qualifier 'certain' does create a verification burden: one must check that the functor-side condition is statable independently of the hyperdoctrine-side Frobenius property. However, the supplied full text is heavily corrupted and unreadable, so no definition or proof step can be quoted to exhibit a specific circular reduction such as Eq. X = Eq. Y by construction. Without such evidence, per the stated rules, I cannot claim circularity. There is also no load-bearing self-citation in the readable portion: the cited background (Dawson, Pare, and Pronk) is prior external work. The honest finding is therefore no demonstrated circularity, with the caveat that the unreadable proof text cannot be independently certified from this copy.
Assumptions & free parameters
assumptions (3)
- domain assumption The cited 'well-known' equivalence between pseudofunctors from bicategories of spans and Beck-Chevalley bifibrations, together with Dawson-Paré-Pronk's double-categorical version, is correct.
- standard math Standard definition and axioms of (generalised) regular hyperdoctrines: finite products on the base, fibred logical structure, Beck-Chevalley and Frobenius conditions.
- ad hoc to paper The double-categorical data (lax symmetric monoidal structure whose laxators are companion commuter cells) exactly exhausts the coherence data of the Frobenius/regular structure, with no hidden extra axioms needed.
invented entities (1)
-
Regular double hyperdoctrine (hinted)
Cite this review
Pith. "Pith review of Double-functorial representation of regular hyperdoctrines." pith.science (2026). https://pith.science/paper/ODIGNZ3E
@misc{pith2026250806637,
author = {Pith},
title = {Pith review of: Double-functorial representation of regular hyperdoctrines},
year = {2026},
howpublished = {\url{https://pith.science/paper/ODIGNZ3E}},
note = {Machine review of arXiv:2508.06637}
}
read the original abstract
It is well-known that pseudofunctors from bicategories of spans are equivalent to Beck-Chevalley bifibrations, and therefore capture the relationships underlying the adjunctions suitable as semantics for existential quantification. This was further expanded upon by Dawson, Par\'e and Pronk in the context of double categories. By viewing hyperdoctrines from a double-categorical lens, this paper shows that we can also characterise the Frob\"enius property: (generalised) regular hyperdoctrines correspond to certain lax symmetric monoidal pseudo double functors from spans to quintets whose monoidal laxators provide companion commuter cells (in the sense of Par\'e). This facilitates the study of the compositionality of regular hyperdoctrines and hints at a new notion of regular double hyperdoctrine. As an application, we discuss how we can recover a form of graphical regular logic suitable for modelling specifications of systems (e.g., port-plugging systems) that compose operadically.
Reference graph
Works this paper leans on
-
[1]
Propositional logics for the L awvere quantale
Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Propositional logics for the L awvere quantale. Electronic Notes in Theoretical Informatics and Computer Science , Volume 3-Proceedings of MFPS 2023, November 2023
work page 2023
-
[2]
Spectral M ackey functors and equivariant algebraic K -theory ( I )
Clark Barwick. Spectral M ackey functors and equivariant algebraic K -theory ( I ). Advances in Mathematics , 304:646--727, 2017
work page 2017
-
[3]
Robert Dawson, Robert Pare, and Dorette Pronk. Adjoining adjoints. Advances in Mathematics , 178:99--140, 2003
work page 2003
-
[4]
Robert Dawson, Robert Pare, and Dorette Pronk. Universal properties of span. Theory and Applications of Categories , 13(4):61--85, 2004
work page 2004
-
[5]
Robert Dawson, Robert Pare, and Dorette Pronk. The span construction. Theory and Applications of Categories , 24(13):302--377, 2010
work page 2010
-
[6]
Brendan Fong and David I Spivak. Graphical regular logic. arXiv:1812.05765 , 2018
work page Pith review arXiv 2018
-
[7]
Brendan Fong and David I. Spivak. Hypergraph categories. Journal of Pure and Applied Algebra , 223(11):4746--4777, 2019
work page 2019
-
[8]
Marco Grandis. Limits in double categories. Cahiers de topologie et géométrie différentielle catégoriques , 40:162--220, 1999
work page 1999
Show all 20 references
-
[9]
Higher Dimensional Categories: From Double to Multiple Categories
Marco Grandis. Higher Dimensional Categories: From Double to Multiple Categories . World Scientific, ISBN 9789811205101, 2019
2019
-
[10]
Two-variable fibrations, factorisation systems and categories of spans
Rune Haugseng, Sil Linskens, Joost Nuiten, and Fabian Hebestreit. Two-variable fibrations, factorisation systems and categories of spans. Forum of Mathematics, Sigma , 11(2023):1--70, 2023
2023
-
[11]
Representable multicategories
Claudio Hermida. Representable multicategories. Advances in Mathematics , 151:164--225, 2000
2000
-
[12]
Cartesian double theories: A double-categorical framework for categorical doctrines
Michael Lambert and Evan Patterson. Cartesian double theories: A double-categorical framework for categorical doctrines. Advances in Mathematics , 444:109630, 2024
2024
-
[13]
William Lawvere
F. William Lawvere. Adjointness in foundations, with author commentary. Reprints in Theory and Applications of Categories , (16):1--16, 2006
2006
-
[14]
Towards a double operadic theory of systems
Sophie Libkind and David Jaz Myers. Towards a double operadic theory of systems. arXiv:2505.18329 , 2025
2025 arXiv
-
[15]
Monoidal G rothendieck C onstruction
Joe Moeller and Christina Vasilakopoulou. Monoidal G rothendieck C onstruction. Theory and Applications of Categories , 35(31):1159--1207, 2020
2020
-
[16]
Retrocells
Robert Paré. Retrocells. Theory and Applications of Categories , 40(5):130--179, 2024
2024
-
[17]
M. Shulman. Framed bicategories and monoidal fibrations. Theory and Applications of Categories , 20(18):650--738, 2008
2008
-
[18]
Comparing composites of left and right derived functors
Michael Shulman. Comparing composites of left and right derived functors. The New York Journal of Mathematics [electronic only] , 17:75--125, 2011
2011
-
[19]
David I. Spivak. The operad of wiring diagrams: formalizing a graphical language for databases, recursion, and plug-and-play circuits. arXiv:1305.0297 , 2013
2013 arXiv
-
[20]
David I. Spivak. Generalized lens categories via functors C ^ op Cat . arXiv:1908.02202 , 2019
1908 arXiv
Reviewed August 5, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.