{"id":"b2487797-1f9f-4b85-8f8d-97f42aee9542","arxiv_id":"2504.19389","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Directories give an inherently strict, name-indexed 2-monadic presentation of product, coproduct, and symmetric monoidal categories, equivalent to the classical FinFam constructions.","lead":"The paper formalizes directories: a way to combine objects and morphisms using named, period-separated paths like cart.motor.momentum instead of nested binary tuples. It builds monads whose strict algebras are product, coproduct, or symmetric monoidal categories, and implements the idea in Haskell.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The proof that Dtry is a 2-monad skips the cartesian-monad hypothesis: Proposition 3.8 cites Appendix B, which requires a cartesian monad, but the paper only proves Dtry is a polynomial monad.","rationale":"The reader identified the monadicity claim in Theorem C.9 as the weakest assumption, and that is a real one-sentence gap. However, before Theorem C.9 can even be stated, the paper must know that Dtry0 is a 2-monad. Proposition 3.8 delegates this to Appendix B, which requires a cartesian monad. The paper's Definition 2.7 of polynomial monad is weaker, and the paper itself gives FinFam as an example of a polynomial monad that is not a strict 2-monad. Therefore the unproven cartesianness of Dtry is a more fundamental, load-bearing omitted verification. I agree with the reader's overall CONDITIONAL posture: the results are plausible and likely correct, but the proof has a missing hypothesis check. The concrete test—checking cartesianness of the distributive law—would settle whether the gap is real. If the distributive law is cartesian, the paper's construction works but needs an explicit proof; if not, the central claim would need a different argument. Since the reader's verdict already requires additional proof before acceptance, I do not change the verdict, but I flag this earlier and distinct gap.","tokens_in":23222,"tokens_out":35495,"duration_ms":351331,"concrete_test":"Prove or disprove that the distributive law filterNothings of Theorem A.9 is a cartesian natural transformation: for every function f: X→Y, the naturality square for filterNothings: Record≠∅(Maybe X) → Maybe(Record≠∅ X) must be a pullback. Concretely, take X={a,b}, Y={y}, f(a)=f(b)=y, and check that for any b∈Record≠∅(Maybe Y) and c∈Record≠∅(Maybe X) with the appropriate compatibility, there is a unique lift in Record≠∅(Maybe X) making the square a pullback. If all such squares are pullbacks, then Dtry = Maybe∘𝔪Record≠∅ is a cartesian monad (free monads on polynomial functors and Maybe are cartesian, and cartesian distributive laws compose), so Appendix B applies and Proposition 3.8 is justified. If any square fails, the construction of Dtry0 as a 2-monad requires additional argument.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central construction requires Dtry0 to be a 2-monad on Cat. Proposition 3.8 says 'Proof: See Appendix B.' But Theorem B.1 is stated for a cartesian monad on a locally cartesian category, and Corollary B.2 lifts a cartesian monad on Set to a monad on Cat. The paper only proves in Proposition 2.11 that Dtry is a polynomial monad, defined in Definition 2.7 as a monad whose underlying functor is polynomial. This is strictly weaker: the FinFam monad is also polynomial (underlying functor X ↦ ∐_{I finite} X^I) yet is not a strict 2-monad, as Section 3.2 itself notes. To lift a Set-monad to a monad on Cat via the internal-category span construction, the unit η and multiplication μ must be cartesian natural transformations (all naturality squares pullbacks), so that the lifted unit and multiplication are functors of internal categories. The paper never verifies that the unit, multiplication, or the distributive law filterNothings of Theorem A.9 are cartesian. Without this, Proposition 3.8 has no proof, and the later factorization in Theorem C.9 starts from an unestablished 2-monad. This is a gap distinct from, and prior to, the monadicity of the natural transformation Dtry0→FinFam= that the reader flagged.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":23477,"tokens_out":39969,"duration_ms":422309,"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":[{"comment":"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.","section":"Proposition 3.8 / Appendix B"},{"comment":"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.","section":"Theorem C.9 / Definition 3.10"},{"comment":"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.","section":"Theorem C.9, monad morphism verification"},{"comment":"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.","section":"Section 3.4"}],"minor_comments":[{"comment":"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.'","section":"Lemma C.8 / Theorem C.9"},{"comment":"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.","section":"Example 2.6 / Theorem C.9"},{"comment":"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.","section":"Proposition 2.14"},{"comment":"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.","section":"Theorem A.9"},{"comment":"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.","section":"Definition 3.7"}],"recommendation":"major_revision","confidential_remarks":"The paper is likely salvageable: the missing cartesian-monad verification may be a genuine but local gap, since Dtry may well be cartesian and the 2-monad lifting can alternatively be checked directly by a pointwise construction. The FinFam=/FinFam identification in Theorem C.9 also appears fixable, but it must be stated. My main concern is that the central 2-algebra equivalences in Section 3.4, which are the paper's advertised payoff, are currently asserted rather than proved; this is the point that most needs a complete treatment before publication."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"I'll give you the short version first: if you work on applied category theory or compositional modeling, this paper is worth a look, but don't trust the main theorem yet. The directory monad Dtry on Set is a nice, practical construction, and the literate Haskell is honest and runnable. The mathematical gap, though, is not a minor omitted diagram. Proposition 3.8 sends the reader to Appendix B, but Appendix B lifts only cartesian monads on Set to monads on Cat. The paper proves Dtry is a polynomial monad — and that is not enough. FinFam is polynomial too, and it is not a strict 2-monad; the paper itself says so. To use the appendix you need the unit and multiplication to be cartesian natural transformations, and that includes the distributive law filterNothings. I could not find those verifications anywhere in the text. Without them, Dtry0 is not established, and Theorem C.9 starts from an unproven base. The one-sentence monadicity claim in C.9 about Dtry0 → FinFam= is a separate, secondary gap, and the pathMap inverse is sketched rather than proved. None of these are fatal to the idea; they are missing arguments.\n\nWhat is genuinely new: the presentation of finite products, coproducts, and symmetric monoidal structure via period-separated named tuples, and the concrete construction of Dtry as Maybe composed with the free monad on non-empty records. The exposition of polynomial monads and distributive laws is clear and would be useful to students. The connection to Fam and FinFam= is well drawn.\n\nMy recommendation: send it to a serious referee, but tell the referee to focus on the cartesian hypothesis. If the authors can give a real proof that Dtry is a cartesian monad, or find a different lifting route, the paper will be worth publishing. As it stands, it is a promising working draft, not a finished proof.","headline":"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.","tokens_in":24037,"tokens_out":3641,"would_cite":false,"duration_ms":34526,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["18C15","18C20","18D10"],"pacs":[],"model":"deepseek-v4-flash","headline":"Directories produce 2-monads whose strict algebras match finite products, coproducts, and symmetric monoidal categories.","keywords":["directories","2-monads","polynomial functors","strict algebras","symmetric monoidal categories","fam construction","named tuples","coherence"],"falsifier":"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.","tokens_in":22983,"feed_emoji":"📁","tokens_out":15470,"duration_ms":137398,"temperature":0.7,"pith_summary":"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.","feed_headline":"Named-tuple directories make products and coproducts strict","feed_subtitle":"A directory formalism removes associator bookkeeping and comes with working Haskell code.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the transfinite construction of free algebras used to form the free monad on non-empty finite sets of symbols.","marker":"[4]"},{"why":"Supplies the distributive-law criterion used to prove the monad structure on Dtry as the composite of Maybe with that free monad.","marker":"[7]"},{"why":"Documents the classical Fam construction whose morphism structure is grafted onto Dtry via the bo-ff factorization.","marker":"[10]"},{"why":"Provides the 2-category background for 2-algebras and lax or colax morphisms used in Section 3.4.","marker":"[12]"},{"why":"Gives the notion of algebraically-free monad used to identify functor algebras with monad algebras in Appendix A.","marker":"[15]"},{"why":"Supplies the exercise that distributive laws correspond to liftings of monads to Eilenberg-Moore categories, used in Lemma A.7.","marker":"[16]"},{"why":"Supplies the treatment of cartesian monads used in Appendix B to lift Dtry from sets to categories.","marker":"[17]"},{"why":"Gives the monad construction in double categories used in Appendix B's composite 2-functor for internal categories.","marker":"[18]"},{"why":"Gives the lemma that a 1-category monad on the underlying functor of a 2-functor is enough for a 2-monad, used in Theorem C.9.","marker":"[23]"},{"why":"Provides the factorization-system presentation of the bo-ff factorization used in Appendix C to transfer the monad structure.","marker":"[24]"}],"fun_headline_variants":["Directories: a strict formalism for products and coproducts","File-system paths make categorical products and coproducts strict","Named-tuple directories remove associator bookkeeping in categories","Strict algebras from dot-separated directory names in categories","A 2-monad for directories yields strict product and coproduct categories"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Directories: a strict formalism for products and coproducts","File-system paths make categorical products and coproducts strict","Named-tuple directories remove associator bookkeeping in categories","Strict algebras from dot-separated directory names in categories","A 2-monad for directories yields strict product and coproduct categories"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000855,"raw_usage":{"total_tokens":3694,"prompt_tokens":901,"completion_tokens":2793,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":517,"completion_tokens_details":{"reasoning_tokens":2704}},"tokens_in":517,"tokens_out":2793,"duration_ms":21234,"temperature":1.0,"reasoning_tokens":2704,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T05:54:02.681125+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the transfinite construction of free algebras used to form the free monad on non-empty finite sets of symbols."},{"cited_title":"Varkor, Original reference for the fam construction (2021)","cited_arxiv_id":null,"evidence_quote":"Documents the classical Fam construction whose morphism structure is grafted onto Dtry via the bo-ff factorization."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Gives the notion of algebraically-free monad used to identify functor algebras with monad algebras in Appendix A."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the exercise that distributive laws correspond to liftings of monads to Eilenberg-Moore categories, used in Lemma A.7."},{"cited_title":"Power, Unicity of enrichment over cat or gpd, Applied Categorical Structures 19 (1) (2009) 293–299.doi:10.1007/s10485-009-9202-7","cited_arxiv_id":null,"evidence_quote":"Gives the lemma that a 1-category monad on the underlying functor of a 2-functor is enough for a 2-monad, used in Theorem C.9."},{"cited_title":"the free monad","cited_arxiv_id":null,"evidence_quote":"Provides the factorization-system presentation of the bo-ff factorization used in Appendix C to transfer the monad structure."}],"review_version":1}