Pith. sign in

REVIEW 4 major objections 5 minor 29 references

Directories: A Convenient and Well-Behaved Formalism for Hierarchical Organization in Categorical Systems Theory

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

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

Pith's one-line read Directories produce 2-monads whose strict algebras match finite products, coproducts, and symmetric monoidal categories.

desk verdict The directory monad is a promising idea and the code is real, but the lift to a 2-monad is unproven because Dtry is never shown to be a cartesian monad — the exact hypothesis Appendix B needs. read the letter →

arxiv 2504.19389 v2 pith:HRNBZTFP submitted 2025-04-27 math.CT

Owen Lynch , Markus Lohmayer This is my paper · ORCID
classification math.CT MSC 18C1518C2018D10
keywords directories2-monadspolynomialfunctorsstrictalgebrassymmetricmonoidalcategoriesfamconstructionnamedtuplescoherence
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 tries to establish that the familiar binary way of combining objects in categories with products, coproducts, or symmetric monoidal products can be replaced by a stricter, name-based formalism inspired by file-system directories. It constructs a monad $\mathrm{Dtry}$ on sets whose elements are period-separated path names such as $\mathtt{cart.motor.momentum}$, and then lifts it to a 2-monad on the 2-category $\mathbf{Cat}$. It claims that the strict algebras of this 2-monad and of two variants are 2-equivalent to categories with finite coproducts, finite products, and symmetric monoidal categories, respectively. The payoff would be an inherently strict presentation of such structures, in which flattening a nested directory is strictly associative and carries human-readable names, so no associator bookkeeping is needed; the paper also supplies a working Haskell implementation.

What carries the argument

The central object is the polynomial monad $\mathrm{Dtry} := \mathrm{Maybe} \circ \mathfrak{m}_{\mathrm{Record}_{\neq \emptyset}}$, built from the polynomial functor $\mathrm{Record}_{\neq \emptyset}$ of non-empty finite sets of symbols and the free monad construction $\mathfrak{m}_{(-)}$. As a data structure this is a trie: complete paths point to values, and empty subdirectories are disallowed except at the top level, which ensures that the path map is an injection. The 2-monad on $\mathbf{Cat}$ is assembled in two steps: first the cartesian (pullback-preserving) monad on sets is lifted to a 2-monad $\mathrm{Dtry}_0$ on internal categories, and then the morphisms of the classical $\mathrm{Fam}$ construction are grafted on via the bijective-on-objects / fully-faithful (bo-ff) factorization of the natural transformation $\mathrm{Dtry}_0 \to \mathrm{FinFam}^=$. Strict algebras of the resulting 2-monads act as unbiased products, combining all objects in a directory into a single object.

What would settle it

Find prefix-free sets of paths $U$ and $\{V_n\}_{n \in U}$ for which the lexicographic order on the concatenated set $U * \{V_n\}$ disagrees with the order on the disjoint sum $\sum_{n \in U} V_n$; because the proof of Theorem C.9 rests on exactly this order-preservation to conclude that $\mathrm{Dtry}_0 \to \mathrm{FinFam}^=$ is monadic, such a case would break the construction of $\mathrm{Dtry}$ as a 2-monad.

Watch

Extended reading notes

Core claim

The central claim is that the assignment sending a category $\mathcal{C}$ to the category $\mathrm{Dtry}(\mathcal{C})$, whose objects are directories of objects of $\mathcal{C}$ (finite prefix-free sets of dot-separated paths labeling objects) and whose morphisms are morphisms of such directories, is the object part of a 2-monad on $\mathbf{Cat}$. Theorem C.9 states this directly. From it, Section 3.4 derives the paper's main structural result: strict algebras of $\mathrm{Dtry}$ are 2-equivalent to categories with finite coproducts, strict algebras of the op-dual $\mathrm{Dtry}((-)^{\mathrm{op}})^{\mathrm{op}}$ to categories with finite products, and strict algebras of the bijective-morphism variant $\mathrm{Dtry}^{\mathfrak{f}}$ to symmetric monoidal categories. The discovery is that a directory such as $(a \mapsto x,\; b.c \mapsto y)$ is an unbiased named tuple, so composing directories -- concatenating path prefixes -- is strictly associative and unital in a way that nested binary tuples are not, while retaining intelligible names throughout.

Load-bearing premise

The load-bearing premise is a single technical assertion in Theorem C.9: the natural transformation from ordered directory families to the standard finite-family construction is monadic because directory multiplication preserves the lexicographic path order; if that assertion fails, $\mathrm{Dtry}$ is not guaranteed to be a 2-monad.

Editorial extensions

If this is right

  • Strict $\mathrm{Dtry}$-algebras provide an unbiased, strictly associative definition of finite coproducts, so computer implementations of categorical structures can skip the coherence conditions.
  • The equivalence $\mathrm{Dtry}(\mathcal{C}) \simeq \mathrm{FinFam}(\mathcal{C})$ gives a user-friendly coproduct completion: every finite family is representable by a directory whose path names survive nested flattening instead of being reindexed.
  • The $\mathrm{Dtry}^{\mathfrak{f}}$ variant offers an inherently strict presentation of symmetric monoidal categories, with named tuples replacing nested binary products that are only associative up to an associator.
  • In hierarchical systems modeling, variables named like `motor.stator.coil.flux` can be composed and flattened without name collisions, matching the motivating applications from port-Hamiltonian systems.

Reading between the lines

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

  • Editorial inference: the same two-step construction - lift a cartesian monad, then graft morphisms through a factorization - should apply to other polynomial monads, giving a general template for strict unbiased presentations of algebraic doctrines beyond products and coproducts.
  • Editorial inference: if the strict-algebra equivalence is correct, coherence theorems for symmetric monoidal categories could be recast as strictification statements about $\mathrm{Dtry}^{\mathfrak{f}}$, potentially simplifying proofs that currently manage associators and symmetries.
  • A testable extension: the paper's Haskell definitions could be turned into property-based tests that verify the monad laws and the path-map bijection on finite random directories, giving empirical confidence in the construction.
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 a monad Dtry on Set whose elements are hierarchical directories of named paths, and then proposes to lift it to a 2-monad on Cat. The central claims are that variants of this 2-monad have strict 2-algebras equivalent to categories with finite coproducts, finite products, and symmetric monoidal structures, respectively, providing an inherently strict named-tuple analogue of the Fam construction. The paper also exposes connections with polynomial monads and distributive laws, and includes literate Haskell code implementing the Set-level constructions.

Significance. If the 2-monad construction is made fully rigorous, the paper offers a practically motivated and genuinely strict alternative to the classical Fam completion, with potential value for applied category theory and computer implementation. The accompanying Haskell code and the expository treatment of polynomial monads, free monads, and distributive laws are useful contributions. However, the current manuscript leaves several load-bearing verification steps either unproved or proved only by appeal to hypotheses that are not checked; these gaps substantially weaken the confidence one can place in the advertised 2-algebra equivalences.

major comments (4)
  1. [Proposition 3.8 / Appendix B] The proof of Proposition 3.8 is the sentence 'See Appendix B.' The theorem invoked there, Theorem B.1 and Corollary B.2, requires a cartesian monad in the sense of Definitions B.6 and B.8. The only hypothesis proved for Dtry is Proposition 2.11, which says Dtry is a polynomial monad. This is not sufficient: for example, the reader monad T(X)=X^A with |A|≥2 is polynomial, but its unit is not a cartesian natural transformation, since the naturality square for a non-injective f is not a pullback. The manuscript nowhere verifies that the unit and multiplication of Dtry, or the naturality squares involved in the distributive law, are cartesian. Consequently Proposition 3.8 is currently unproved, and since Dtry0 is the input to the bo-ff factorization in Theorem C.9, this gap is load-bearing for the whole 2-monad claim. The authors should either prove the required cartesianness of Dtry or give a direct construction of Dtry0 as a 2-monad.
  2. [Theorem C.9 / Definition 3.10] The category Dtry(𝒞) in the body is defined as the bo-ff factorization of PathFamily: Dtry0(𝒞)→FinFam(𝒞). Theorem C.9 instead applies Lemma C.8 to the composite Dtry0→FinFam=, obtained by fixing a lexicographic order on paths. The proof never shows that the monad obtained from the second factorization is the same as, or isomorphic to, the monad defined in Definition 3.10, nor that their 2-monad structures agree. This is not a purely cosmetic issue: FinFam= is indexed by initial segments {1,...,n}, whereas the body's hom-sets are indexed by arbitrary prefix-free path sets. Since the statements in Section 3.4 concern the 2-monad of Definition 3.10, this identification must be stated and proved explicitly, or Dtry must be redefined from the start using ordered paths.
  3. [Theorem C.9, monad morphism verification] The proof asserts that the natural transformation Dtry0→FinFam= is monadic because the monad multiplication Dtry∘Dtry→Dtry is order-preserving for the lexicographic order. Lemma C.8 requires the full unit and multiplication diagrams displayed in its statement, and in the 2-categorical setting one must also check 2-naturality with respect to functors and natural transformations. Order preservation of μ is at most one ingredient; the unit square, the multiplication square, and the 2-naturality are not shown. This step should be expanded into an explicit, diagram-level proof.
  4. [Section 3.4] The advertised equivalences between strict 2-algebras of Dtry, Dtry((−)op)op, and Dtry𝔣 and categories with finite coproducts, finite products, and symmetric monoidal structures are asserted without theorem statements or proofs. These equivalences are not immediate consequences of the category-level equivalence Dtry(𝒞)≃FinFam(𝒞) in Proposition 3.11, because strict algebra structure depends on the 2-monad multiplication and the classical Fam results concern pseudoalgebras with a choice of strictification. The section should state precisely which morphisms (strict, pseudo, or lax) are used in the claimed 2-equivalences and provide proofs or exact references with the translation spelled out.
minor comments (5)
  1. [Lemma C.8 / Theorem C.9] The phrase 'monadic natural transformation' is used for what is usually called a monad morphism; this conflicts with the established meaning of monadicity. Please rename it, e.g., 'monad morphism' or 'morphism of monads.'
  2. [Example 2.6 / Theorem C.9] Example 2.6 only assumes |Sym|≥2, but Theorem C.9 uses a lexicographic order on paths; the paper should state once that Sym is equipped with a fixed linear order throughout.
  3. [Proposition 2.14] The proof of Proposition 2.14 is explicitly left as a sketch ('We will not do the proof ... in all of its fine detail'). Since the prefix-free presentation is used later to compare Dtry with FinFam, please provide a complete proof in an appendix.
  4. [Theorem A.9] The proof of Theorem A.9 is presented as a short two-case diagram chase. For a formal paper, the 'otherwise' case should be made precise, for example by describing the surviving record after dropping Nothings, rather than leaving the case distinction informal.
  5. [Definition 3.7] The phrase 'modulo size issues' should be made precise, for example by fixing a universe, if the paper intends Dtry0 to apply to the full 2-category Cat rather than only to small categories.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the derivation is self-contained and relies on external, established 2-monad and factorization machinery; the two proof gaps are correctness risks, not circular reductions.

full rationale

Walking the claimed derivation chain: Dtry is first built as a monad on Set (Proposition 2.11, Appendix A), then lifted to a 2-monad on Cat through the internal-category span construction (Proposition 3.8, Appendix B), then modified by an bo-ff factorization against FinFam (Definition 3.10, Appendix C), and finally compared to FinFam (Proposition 3.11). Every load-bearing step is supported either by proofs in the paper or by external references (Kelly, Lack, Power, Leinster, Fiore-Gambino-Kock, etc.). The authors' self-citations [1], [9], and [14] appear only as motivation and application context, not as the source of any theorem. There are no fitted parameters, no data-derived predictions, and no uniqueness theorem imported from the authors' prior work. The headline result that strict algebras of Dtry are 2-equivalent to categories with finite coproducts, products, or symmetric monoidal structures is a corollary of the claimed equivalence Dtry(𝒞) ≃ FinFam(𝒞) together with the classical Fam completion property; it is not an input to the construction. Two proof obligations are indeed under-supported: Proposition 3.8 refers to Appendix B, whose Theorem B.1 requires a cartesian monad, while the paper only proves that Dtry is a polynomial monad in the weak sense of Definition 2.7; and Theorem C.9 asserts without a detailed verification that Dtry0 → FinFam= is monadic. These are genuine correctness risks, but they are not circular: neither amounts to defining Dtry in terms of the target 2-algebra equivalence, nor do they reduce a claimed output to an input by construction. Accordingly, the paper shows no significant circularity.

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

The central claim depends on standard results in polynomial functors, free monads, distributive laws, internal categories, and factorisation systems, plus one asserted technical fact about the monadicity of the comparison natural transformation. There are no fitted numerical parameters or newly postulated physical entities.

assumptions (5)
  • standard math The free monad on a polynomial functor exists and is computed as a colimit (Proposition 2.9).
    Used to define Dtry1 and Dtry as polynomial monads; the proof is cited to [4,5,6] rather than given in the paper.
  • standard math Distributive laws are in bijection with liftings of a monad to the Eilenberg-Moore category (Lemma A.7).
    Stated as exercise 9.2 in [16]; applied in Appendix A to construct the distributive law between the free monad on Record≠∅ and Maybe.
  • standard math There is a 2-functor from locally cartesian categories to 2-Cat sending internal categories to their span/monad presentation (Appendix B).
    Composed from Span, Mon, and Arrow2-Cat; cited to [17], [18], [20], [22], with the Span step left as an exercise. Load-bearing for lifting Dtry from Set to Cat.
  • domain assumption The natural transformation Dtry0 to FinFam= is monadic because the monad multiplication is order-preserving for the lexicographic order induced by a linear order on Sym (Theorem C.9).
    Stated in one sentence in the proof of Theorem C.9 without full derivation; this monadicity is essential for the bo-ff factorization to carry the monad structure.
  • standard math A factorization system on Cat induces a factorization system on functor categories, and monad structures can be transferred through it (Lemma C.8).
    Proved in Appendix C using orthogonality and unique fillers; standard result in factorization system theory.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Directories: A Convenient and Well-Behaved Formalism for Hierarchical Organization in Categorical Systems Theory." pith.science (2026). https://pith.science/paper/HRNBZTFP

@misc{pith2026250419389,
  author       = {Pith},
  title        = {Pith review of: Directories: A Convenient and Well-Behaved Formalism for Hierarchical Organization in Categorical Systems Theory},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HRNBZTFP}},
  note         = {Machine review of arXiv:2504.19389}
}
abstract

This paper introduces an inherently strict presentation of categories with products, coproducts, or symmetric monoidal products that is inspired by file systems and directories. Rather than using nested binary tuples to combine objects or morphisms, the presentation uses named tuples. Specifically, we develop 2-monads whose strict 2-algebras are product categories, coproduct categories, or symmetric monoidal categories, in a similar vein to the classical Fam construction, but where the elements of the indexing set are period-separated identifiers like $\mathtt{cart.motor.momentum}$. Our development of directories is also intended to serve the secondary purpose of expositing certain aspects of polynomial monads, and is accompanied by Haskell code that shows how the mathematical ideas can be implemented.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

29 extracted references · 21 canonical work pages

  1. [1]

    Exergetic Port-Hamiltonian Systems Modeling Language

    M.Lohmayer,O.Lynch,S.Leyendecker,Exergeticport-hamiltoniansystems modeling language (2025).doi:10.48550/ARXIV.2402.17640. URL https://arxiv.org/abs/2402.17640

    work page Pith review arXiv doi:10.48550/arxiv.2402.17640 2025

  2. [2]

    C. B. Jay, J. R. B. Cockett, Shapely types and shape polymorphism, Springer Berlin Heidelberg, 1994, pp. 302–316.doi:10.1007/3-540-57880-3_20

    work page doi:10.1007/3-540-57880-3_20 1994

  3. [3]

    N. Niu, D. I. Spivak, Polynomial Functors: A Mathematical Theory of Interaction, 2023. URL https://topos.site/poly-book.pdf

    work page 2023

  4. [4]

    G.M.Kelly,Aunifiedtreatmentoftransfiniteconstructionsforfreealgebras, free monoids, colimits, associated sheaves, and so on, Bull. Austral. Math. Soc. 22 (1980) 1–83

    work page 1980

  5. [5]

    org/nlab/show/transfinite+construction+of+free+algebras, Revi- sion 13 (August 2024)

    nLab authors, transfinite construction of free algebras,https://ncatlab. org/nlab/show/transfinite+construction+of+free+algebras, Revi- sion 13 (August 2024)

    work page 2024

  6. [6]

    Libkind, D

    S. Libkind, D. I. Spivak, Pattern runs on matter: The free monad monad as a module over the cofree comonad comonad (apr 2024).arXiv:2404. 16321v1. URL http://arxiv.org/abs/2404.16321v1

    work page arXiv 2024

  7. [7]

    Beck, Distributive laws, Springer Berlin Heidelberg, 1969, pp

    J. Beck, Distributive laws, Springer Berlin Heidelberg, 1969, pp. 119–140. doi:10.1007/bfb0083084. 25

    doi:10.1007/bfb0083084 1969

  8. [8]

    D. E. Rydeheard, R. M. Burstall, Computational Category Theory, Prentice Hall, 1988

    work page 1988

Show all 29 references
  1. [9]

    Lynch, K

    O. Lynch, K. Brown, E. Patterson, J. Fairbanks, Gatlab: a computer algebra system based on generalized algebraic theories (2024). URL https://github.com/AlgebraicJulia/Gatlab.jl

    2024

  2. [10]

    Varkor, Original reference for the fam construction (2021)

    N. Varkor, Original reference for the fam construction (2021). URL https://mathoverflow.net/questions/393917/ original-reference-for-the-fam-construction

    2021

  3. [11]

    URL http://dx.doi.org/10.1007/s10485-021-09671-9

    P.Perrone,W.Tholen,Kanextensionsarepartialcolimits,AppliedCategor- ical Structures 30 (4) (2022) 685–753.doi:10.1007/s10485-021-09671-9. URL http://dx.doi.org/10.1007/s10485-021-09671-9

    2022 doi

  4. [12]

    Lack, A 2-Categories Companion, Springer New York, 2009, pp

    S. Lack, A 2-Categories Companion, Springer New York, 2009, pp. 105–191. doi:10.1007/978-1-4419-1524-5_4. URL http://dx.doi.org/10.1007/978-1-4419-1524-5_4

    2009 doi

  5. [13]

    D. I. Spivak, The operad of wiring diagrams: formalizing a graphical language for databases, recursion, and plug-and-play circuits (2013).doi: 10.48550/ARXIV.1305.0297

    2013 doi arXiv

  6. [14]

    URL https://MarkusLohmayer.github.io/EPHS.jl

    M.Lohmayer,EPHS.jl–acompositional,energy-basedsoftwareframework for modeling mechanical, electromagnetic, and thermodynamic systems (2025). URL https://MarkusLohmayer.github.io/EPHS.jl

    2025

  7. [15]

    nLab authors, free monad, , Revision 19 (May 2024)

    2024

  8. [16]

    M. Barr, C. Wells, Toposes, Triples and Theories, Reprints in Theory and Applications of Categories, 2005, originally published by Springer-Verlag. URL http://www.tac.mta.ca/tac/reprints/articles/12/tr12abs. html

    2005

  9. [17]

    Leinster, Higher Operads, Higher Categories, Cambridge University Press, 2004

    T. Leinster, Higher Operads, Higher Categories, Cambridge University Press, 2004. doi:10.1017/cbo9780511525896. URL http://dx.doi.org/10.1017/CBO9780511525896

    2004 doi

  10. [18]

    T. M. Fiore, N. Gambino, J. Kock, Monads in double categories, Journal of Pure and Applied Algebra 215 (6) (2011) 1174–1197.doi:10.1016/j.jpaa. 2010.08.003. URL http://dx.doi.org/10.1016/j.jpaa.2010.08.003

    2011 doi

  11. [19]

    Street, The formal theory of monads, Journal of Pure and Applied Algebra 2 (2) (1972) 149–168.doi:10.1016/0022-4049(72)90019-9

    R. Street, The formal theory of monads, Journal of Pure and Applied Algebra 2 (2) (1972) 149–168.doi:10.1016/0022-4049(72)90019-9. URL http://dx.doi.org/10.1016/0022-4049(72)90019-9

    1972 doi

  12. [20]

    Grandis, Higher dimensional categories: From double to multiple categories, World Scientific Publishing, Singapore, Singapore, 2019

    M. Grandis, Higher dimensional categories: From double to multiple categories, World Scientific Publishing, Singapore, Singapore, 2019. 26

    2019

  13. [21]

    Shulman, Framed bicategories and monoidal fibrations, Theory and Applications of Categories 20 (18) (2008) 650–738

    M. Shulman, Framed bicategories and monoidal fibrations, Theory and Applications of Categories 20 (18) (2008) 650–738. URL http://www.tac.mta.ca/tac/volumes/20/18/20-18.pdf

    2008

  14. [22]

    Lambert, E

    M. Lambert, E. Patterson, Cartesian double theories: A double-categorical framework for categorical doctrines, Advances in Mathematics 444 (2024) 109630. doi:10.1016/j.aim.2024.109630

    2024

  15. [23]

    Power, Unicity of enrichment over cat or gpd, Applied Categorical Structures 19 (1) (2009) 293–299.doi:10.1007/s10485-009-9202-7

    J. Power, Unicity of enrichment over cat or gpd, Applied Categorical Structures 19 (1) (2009) 293–299.doi:10.1007/s10485-009-9202-7. URL http://dx.doi.org/10.1007/s10485-009-9202-7

    2009 doi

  16. [24]

    the free monad

    Joyal’s Catlab authors, Factorisation systems, https://ncatlab.org/joyalscatlab/published/Factorisation+systems (2020). A. Free Monads and Distributive Laws In this appendix, we complete the proof that there is a distributive law between 𝔪Record≠∅ and Maybe. One way to do this...

    2020

  17. [25]

    If we lift𝑇 to a monad onMAlg(𝔪𝑃), we get the distributive law we want (Lemma A.7)

  18. [26]

    Thecategory MAlg(𝔪𝑃)isisomorphictothecategory FAlg(𝑃)(Lemma A.4)

  19. [27]

    obvious” to a sufficiently experienced category theorist. Likely there is also an “elementary

    We can lift𝑇 to a monad onFAlg(𝑃) (Lemma A.8). We now prove that the conditions of Theorem A.5 hold for𝑃 = Record≠∅ and𝑇 = Maybe, with𝜎 = filterNothings. Theorem A.9. There is a distributive law between𝔪Record≠∅ and Maybe. △ Proof. Because we have Theorem A.5, this is just a d...

  20. [28]

    Every morphism𝑓 : 𝐴→ 𝐵 in𝒞 admits a factorization𝑓 = 𝑢 #𝑝 : 𝐴→ 𝐸→𝐵, with𝑢∈ℒ and𝑝∈ℛ

  21. [29]

    △ Factorization systems have some nice properties beyond what is obvious from their definition

    The classesℒ andℛ contain the isomorphisms and are closed under composition. △ Factorization systems have some nice properties beyond what is obvious from their definition. One of these properties isorthogonality. Definition C.3. Let𝒞 be a category, and let𝑓 : 𝑋→𝑌 and𝑔 : 𝑍→𝑊 b...

Pith tools

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