{"id":"d3e9ca23-51a2-4764-8749-8df90487559f","arxiv_id":"2411.09950","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"In homotopy type theory, the Kleisli category of the exponential comonad on spans is equivalent to the category of V-ary polynomials, yielding a new model of linear logic.","lead":"This paper proves a formal bridge between two areas of mathematics: polynomial functors and linear logic. It shows that in homotopy type theory, the category whose morphisms are polynomials is the Kleisli category for a natural comonad on spans, giving a new model of linear logic.","discovery_kind":"unification","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The unproven truncation step before Theorem 4.14 is load-bearing: if ‖-‖1 does not preserve the Seely structure, the advertised linear-logic model fails even if Theorem 5.9 is correct.","rationale":"The reader's weakest-assumption analysis is accurate: the truncation preservation claim is the most load-bearing unsupported step. Theorem 5.9 itself is supported by explicit, checkable computations (Proposition 5.8 and the composition calculation), and the paper honestly discloses that higher coherence is left for future work. The concern is not that the paper is internally inconsistent—the wild-level arguments are plausible—but that the final bridge from wild to ordinary categories is asserted rather than proved. This matches the reader's CONDITIONAL verdict, so no change is needed. I agree with the reader's identification of the truncation step; the univalence of PolyV is a secondary sketch but less central because Theorem 5.9's equivalence can be read as transferring category structure, making PolyV univalence a derived property.","tokens_in":22093,"tokens_out":16420,"duration_ms":167698,"concrete_test":"Formalize the proof of Theorem 4.14 in a HoTT proof assistant (e.g., Agda with cubical features): construct the truncated tensor, finite products, comonad, and Seely isomorphisms on ‖Span(U)‖1 from the wild structures of Theorem 4.13 by truncation elimination, and verify all axioms of Definition 2.7. If the verification fails or requires additional coherence axioms not present in the wild structure, Theorem 4.14 is not justified.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's advertised conclusion that polynomials give a model of linear logic relies on Theorem 4.14, which states that ‖Span(U)‖1 is a Seely category. The proof is one sentence: 'It is not difficult to show that the categorical structures are preserved by truncation (definition 2.5), and preservation of univalence was shown in proposition 2.6.' No proof is supplied that the symmetric monoidal closed structure, finite products, the exponential comonad, and the Seely isomorphisms m2, m0 survive the truncation, nor that the Seely diagram of Definition 2.7 commutes after truncation. Truncation changes the object type from U to ‖U‖1 and each hom-type to its 0-truncation, so every structure morphism must be redefined by truncation elimination and every naturality/coherence proof rechecked. This is not automatic: the universal property of the internal hom, for example, is an equivalence of hom-types, and while truncation preserves equivalences, naturality in truncated objects needs an argument. If any one of these structures fails to be preserved, Theorem 4.14 is false, and the 'homotopical model of linear logic' claim is not established, even though the wild-level Theorem 4.13 and the Kleisli equivalence Theorem 5.9 may be correct. The paper's own framing (Section 1) says the ∞-categorical version is out of reach; the truncation step is the bridge to an actual category, and it is currently unsupported.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper constructs, in homotopy type theory, the V-ary exponential !_V A := Σ_{E:V}(E→A), shows that it is a monad on the universe U, lifts it to a comonad on the wild category Span(U), and proves that the resulting wild Kleisli category is equivalent to the wild category Poly_V of V-ary polynomials (Theorem 5.9). Along the way, it establishes that Span(U) is symmetric monoidal closed with finite products, assembles these structures into a wild Seely category (Theorem 4.13), and asserts that truncation to a 1-category preserves this structure, yielding an ordinary Seely category and therefore a model of linear logic (Theorem 4.14). The paper also relates the construction to Melliès' template games and to Street's earlier Kleisli observation.","tokens_in":22268,"tokens_out":8943,"duration_ms":96223,"significance":"If the missing technical points are supplied, this is a valuable contribution: it gives a homotopical model of linear logic in which spans are the linear maps, the exponential modality is the free commutative monoid on types, and polynomials are exactly the Kleisli morphisms. The proof of the central Kleisli equivalence (Theorem 5.9) is direct and checkable, with explicit computations for the monad laws, pullback preservation, and composition compatibility. The paper is also honest about the unresolved ∞-categorical coherence issues and explicitly credits Street's prior observation. However, the advertised consequence for ordinary (truncated) categories currently rests on an unproved preservation statement, and the construction of the Seely isomorphisms in spans has a gap; these are load-bearing for the linear-logic model claim.","major_comments":[{"comment":"The sentence 'It is not difficult to show that the categorical structures are preserved by truncation' is not a proof, and the preservation is not automatic. Definition 2.5 replaces the object type by its 1-truncation and each hom-type by its 0-truncation, so the symmetric monoidal closed structure, finite products, the exponential comonad, and the Seely isomorphisms m2 and m0 all have to be redefined by truncation elimination, and the naturality and coherence diagrams of Definition 2.7 have to be rechecked for the truncated data. Proposition 2.6 only covers univalence, not structure preservation. Since Theorem 4.14 is the advertised passage from a wild category to an ordinary model of linear logic, this is a load-bearing gap that should be filled by a detailed proof, or the statement should be weakened to a conjecture.","section":"Section 4, before Theorem 4.14"},{"comment":"The claim that 'l2 being a natural isomorphism, its naturality squares are cartesian' is not generally true. For a commutative square whose top and bottom maps are isomorphisms, the square is a pullback if and only if the vertical map is an isomorphism; here the vertical map is !f × !g or its analogue, which is not an equivalence for arbitrary f and g. Proposition 3.7 only lifts natural transformations whose naturality squares are pullbacks, so the construction of m2 := R(l2) as a natural isomorphism of spans requires a separate proof of cartesianness. The same point applies to l0, though the verification there is easier. Because m2 and m0 are used in Theorem 4.13 and in Theorem 4.14, this gap is load-bearing.","section":"Section 4.2, after Proposition 4.12"},{"comment":"The definition of the wild category PolyV is not fully established. Proposition 5.7 says that unitality and associativity of composition 'will follow from Theorem 5.9', but Theorem 5.9 is stated as an equivalence of the Kleisli category with the wild category PolyV, so it presupposes that PolyV already satisfies the category laws. The proof of Theorem 5.9 does show that the assignment respects composition and identities, so the laws could be transferred from the Kleisli category, but this transfer is not spelled out. In addition, the univalence of PolyV is only sketched: the assertion that an invertible polynomial must have p an equivalence and hence be a span is stated without proof. These points should be made precise, for example by stating Theorem 5.9 for precategories and then deriving the category structure of PolyV, or by giving direct proofs in Section 5.1.","section":"Section 5.1, Proposition 5.7"}],"minor_comments":[{"comment":"There is a typo: 'gollowing' should be 'following'.","section":"Proof of Proposition 3.2"},{"comment":"The assertion that [8] 'only actually constructs a wild 2-coherent category' and is 3-truncated rather than a bicategory is a substantive correction to prior work and is stated without argument; it would be helpful to add a precise justification or a reference.","section":"Section 6.1"},{"comment":"The notation E →_V B for maps with V-small fibers is introduced only informally; a precise definition before Definition 5.5 would improve readability.","section":"Notation throughout"},{"comment":"The final sentence 'Like with η, one can check...' is an incomplete sentence; it should be completed, since the verification is part of the proof.","section":"Section 4.2, proof of Proposition 4.12"}],"recommendation":"major_revision","confidential_remarks":"The central Kleisli equivalence appears sound and is supported by explicit computations, but the advertised linear-logic model currently rests on the unproved truncation-preservation statement and on an incorrect inference about the cartesianness of l2. Both are likely fixable within the paper's scope. The paper also makes a strong claim correcting [8] that may need scrutiny. I would not reject, but I would require a substantive revision before acceptance."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear colleague,\n\nQuick take: this is a genuinely useful paper. It proves in HoTT that V-ary polynomials form the Kleisli category of the free-commutative-monoid comonad on spans (Theorem 5.9), and it builds a wild Seely structure on spans (Theorem 4.13). The proof of 5.9 is concrete and convincing; I checked the key equivalences and the composition computation. The V-ary generalization and the lifting of the exponential monad to spans are real innovations beyond Street's earlier observation, which the paper openly credits. The comparison with Mellies' template games is also helpful.\n\nWhere it gets soft: the advertised model of linear logic as an actual 1-category rests on Theorem 4.14, which is dispatched in one sentence: 'It is not difficult to show that the categorical structures are preserved by truncation.' That is load-bearing. To get a Seely category from the wild one, you need the symmetric monoidal closed structure, finite products, the comonad, and the Seely isomorphisms m2 and m0 to survive ||-||_1, and every naturality and coherence diagram to recheck. This is not automatic from Proposition 2.6, which only covers univalence. The reader's stress-test note is exactly right. It is fixable, probably, but it is not a trivial diagram chase. If truncation does not preserve all of that, Theorem 4.14 fails even though Theorems 4.13 and 5.9 stand.\n\nThere are two smaller gaps. Proposition 5.7 (univalence of Poly_V) is only sketched, and the paper explicitly leaves the associativity and unitality of Poly_V to follow from Theorem 5.9. That is acceptable only because the computation in 5.9 establishes compatibility with the Kleisli composition, but the ordering is awkward. Also, the whole paper works at the wild level, so the 'homotopical model' claim is really a promise about a future infinity-categorical refinement; the authors say this clearly in the introduction, so it is an honest limitation, not a hidden one.\n\nBottom line: the central equivalence is solid, the bridge to linear logic is plausible but under-proved at the truncation step. This deserves a serious referee; I would send it to review and ask for a real proof of Theorem 4.14 or a downgrade of that claim. I would cite it, and I would bring it to a reading group.","headline":"Solid HoTT proof that V-ary polynomials form the Kleisli category of the free-commutative-monoid comonad on spans; the advertised 1-categorical model of linear logic rests on an unproven truncation claim.","tokens_in":22932,"tokens_out":3309,"would_cite":true,"duration_ms":33280,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["18C20","18M05","18N99"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper shows that polynomials are exactly the Kleisli category of a comonad on spans.","keywords":["polynomial functors","Kleisli category","spans","linear logic","homotopy type theory","exponential comonad","Seely category","multisets"],"falsifier":"Compute, in the truncated category $\\|\\mathrm{Span}(U)\\|_1$, whether the truncated Seely isomorphisms $m_2$ and $m_0$ are still invertible and whether the defining Seely diagram commutes; a single non-invertible truncation of $m_2$ for finite types $A,B$ would falsify Theorem 4.14 without contradicting the Kleisli equivalence of Theorem 5.9. Equivalently, one can compare the hom sets of the truncated Kleisli category with those of the truncation of $\\mathrm{Poly}_V$ for $V = \\mathrm{Fin}$ to test whether the equivalence survives truncation.","tokens_in":21759,"feed_emoji":"🔗","tokens_out":7033,"duration_ms":62082,"temperature":0.7,"pith_summary":"The paper refines the construction of polynomials in homotopy type theory by showing that they arise from a universal construction on spans. The exponential modality $!_V A := \\sum_{E:V}(E \\to A)$, which forms the free commutative monoid on a type with arities in a universe $V$, lifts from types to the wild category of spans and becomes a comonad by self-duality. The central theorem states that the associated Kleisli category $\\mathrm{Span}(U)_{!_V}$ is equivalent to the wild category $\\mathrm{Poly}_V$ of $V$-ary polynomials. Since the span category is a wild Seely category, this equivalence makes polynomials a homotopical model of linear logic, and truncating to a 1-category is claimed to yield a Seely category in the usual sense.","feed_headline":"Polynomials are the Kleisli category of a span comonad","feed_subtitle":"In homotopy type theory, the exponential comonad on spans makes its Kleisli category exactly the V-ary polynomials — a model of linear…","key_machinery":"The central object is the exponential modality $!_V A := \\sum_{E:V}(E \\to A)$, the free commutative monoid on a type $A$ with arities in a universe $V$; when $V$ is the universe of finite types this is the homotopical analogue of the multiset construction. The argument shows that the unit $\\eta$ and multiplication $\\mu$ of this monad are cartesian natural transformations, so by the functoriality of the span construction the monad lifts to $\\mathrm{Span}(U)$, and the self-duality of spans turns it into a comonad. The Kleisli comparison rests on the equivalence $\\mathrm{Poly}_V(I,J) \\simeq \\mathrm{Span}(!_V I, J)$, which rewrites a polynomial as a span out of the bang of its source. The Seely isomorphisms $m_2$ and $m_0$ are transported from type-level isomorphisms $l_2$ and $l_0$, and the main technical labour is proving the required diagrams commute in the homotopy-theoretic sense.","core_discovery":"The paper's central discovery is Theorem 5.9: for a universe $V$ of small arities, the Kleisli wild category $\\mathrm{Span}(U)_{!_V}$ associated to the comonad $!_V$ on spans is equivalent to $\\mathrm{Poly}_V$, the wild category of $V$-ary polynomials. The comparison functor fixes objects and sends a polynomial $I \\leftarrow E \\to_V B \\to J$ to the span $!_V I \\leftarrow B \\to J$, reading each fiber of $E \\to B$ as the multiset of variables of one monomial. The paper verifies that this map preserves identities and composition, so the equivalence is a genuine equivalence of wild categories. As a corollary, the Seely structure built on $\\mathrm{Span}(U)$ transfers to polynomials, and after truncation the authors claim a Seely category and hence a model of linear logic.","pith_inferences":["An implication the authors leave implicit is that if the truncation claim holds, the resulting model has an underlying category equivalent to the homotopy category of spaces, which is known not to be concrete; the model is therefore of a different nature from set-based semantics such as coherence spaces.","The paper notes a connection to Melliès' template games; a natural extension, not developed here, is to refine the Seely structure into a model of differential linear logic, with the derivative operation carried by the polynomial data.","A testable extension would be to check whether varying $V$ yields a graded family of linear-non-linear adjunctions, interpolating between linear polynomials for contractible $V$ and arbitrary polynomials for large $V$."],"forward_implications":["If Theorem 5.9 is correct, the intuition that 'linear polynomials are spans' becomes a theorem: spans sit inside $V$-ary polynomials as the linear maps, and the bang modality accounts for the reuse of variables.","The Seely structure on $\\mathrm{Span}(U)$ transfers along the equivalence, so $V$-ary polynomials become a homotopical model of intuitionistic linear logic, with products and coproducts of types supplying the additive connectives.","Choosing $V$ as the finite types recovers finitary polynomial functors over groupoids, reconnecting the Kleisli presentation with the earlier bicategorical construction; choosing $V$ as contractible types recovers spans themselves, so the parameter $V$ interpolates from linear to arbitrary polynomial maps.","Because $\\mathrm{Span}(U)$ is $\\ast$-autonomous, the model extends from intuitionistic to classical linear logic without extra work."],"supporting_citations":[{"why":"supplies the prior definition of polynomials in homotopy type theory and the cartesian closed bicategory that this work refines","marker":"[8]"},{"why":"provides the homotopy type theory background, truncation, univalence, and identity-type machinery on which all constructions rest","marker":"[31]"},{"why":"introduces the bicategorical model of differential linear logic whose Kleisli category is identified with polynomials in Section 6.2","marker":"[25]"},{"why":"surveys polynomial functors and their composition, giving the classical notion that the paper generalizes","marker":"[11]"},{"why":"supplies the definitional framework of Seely categories and linear-non-linear adjunctions used in Theorem 4.13","marker":"[26]"},{"why":"adds the missing Seely axiom and is referenced in the definition of wild Seely category","marker":"[4]"},{"why":"is cited for the earlier observation that polynomial functors can be presented as a Kleisli category","marker":"[29]"},{"why":"introduces normal/finitary polynomial functors, the size restriction that motivates the universe parameter $V$","marker":"[13]"}],"fun_headline_variants":["Span comonad's Kleisli category equals polynomials","Polynomials as Kleisli category of span comonad","Kleisli of span comonad gives polynomials","Polynomials are span comonad's Kleisli category","HoTT polynomials = Kleisli of span comonad"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that truncating the wild span category to a 1-category preserves the entire Seely structure — the symmetric monoidal closed structure, finite products, the exponential comonad, and the Seely isomorphisms; the paper states this is 'not difficult' but gives no proof, and Theorem 4.14 collapses if any piece is lost.","fun_headline_variants_meta":{"raw":{"variants":["Span comonad's Kleisli category equals polynomials","Polynomials as Kleisli category of span comonad","Kleisli of span comonad gives polynomials","Polynomials are span comonad's Kleisli category","HoTT polynomials = Kleisli of span comonad"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000683,"raw_usage":{"total_tokens":3085,"prompt_tokens":915,"completion_tokens":2170,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":531,"completion_tokens_details":{"reasoning_tokens":2084}},"tokens_in":531,"tokens_out":2170,"duration_ms":16199,"temperature":1.0,"reasoning_tokens":2084,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T20:08:39.274485+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Compute, in the truncated category $\\|\\mathrm{Span}(U)\\|_1$, whether the truncated Seely isomorphisms $m_2$ and $m_0$ are still invertible and whether the defining Seely diagram commutes; a single non-invertible truncation of $m_2$ for finite types $A,B$ would falsify Theorem 4.14 without contradicting the Kleisli equivalence of Theorem 5.9. Equivalently, one can compare the hom sets of the truncated Kleisli category with those of the truncation of $\\mathrm{Poly}_V$ for $V = \\mathrm{Fin}$ to test whether the equivalence survives truncation.","supporting_citations":[{"cited_title":"Mimram, M","cited_arxiv_id":null,"evidence_quote":"supplies the prior definition of polynomials in homotopy type theory and the cartesian closed bicategory that this work refines"},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"provides the homotopy type theory background, truncation, univalence, and identity-type machinery on which all constructions rest"},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"supplies the definitional framework of Seely categories and linear-non-linear adjunctions used in Theorem 4.13"},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"adds the missing Seely axiom and is referenced in the definition of wild Seely category"},{"cited_title":"Polynomials as spans","cited_arxiv_id":"1903.03890","evidence_quote":"is cited for the earlier observation that polynomial functors can be presented as a Kleisli category"},{"cited_title":"https://doi.org/10.1016/0168-0072(88)90025-5","cited_arxiv_id":null,"evidence_quote":"introduces normal/finitary polynomial functors, the size restriction that motivates the universe parameter $V$"}],"review_version":1}