{"id":"2f8f59be-6fbc-490b-8534-483565a1f4df","arxiv_id":"2607.25706","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Tagged lenses form a symmetric monoidal category, and imposing change-dependence or first-last-dependence on tags compositionally entails the getput or putput lens laws.","lead":"The paper defines tagged lenses, which attach a counter or side-effect to an ordinary lens, and shows these form a symmetric monoidal category. It then proves that two natural design laws for the tag, change-dependence and first-last-dependence, are sufficient to guarantee the standard getput and putput lens laws.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The category and functor claims rest on closure of the tag commutation axiom under TL-composition; the composite tag is never defined algebraically and the only proof is corrupted string diagrams, leaving Proposition 2 uncheckable.","rationale":"Read the paper in good faith: the intended contribution is a compositional account of lens laws via tag axioms, with two main theorems: TL(C) is a strict symmetric monoidal category (Prop 2) and L is a strict monoidal injective-on-objects functor into pgL(C) (Prop 3). The entailment results (Props 6,7) are algebraic and check out in Set; I verified the putput calculation and it uses the underlying putput plus the tag axiom. The weakest point is the construction of the category: the composite tag is not given by a formula, only by a diagram, and the appendix proof is a series of diagrams, all corrupted in this version. The reader's specific mechanism (that putget of L(phi) depends on the tag axiom) is inaccurate, but the underlying worry is correct: without a checkable definition and proof, the central categorical claim cannot be endorsed. Agreement with reader is partial: same target, different rationale.","tokens_in":11491,"tokens_out":23409,"duration_ms":183610,"concrete_test":"Reconstruct the algebraic definition of the composite tag from Proposition 2's diagram (types: T_comp: S''×V×V→S'' with S'' the codomain state). Verify by direct calculation in Set that (i) T_comp satisfies put(T_comp(s,a,b),c)=T_comp(put(s,c),a,b) using only the corresponding laws for T1,T2 and vwb-laws of the underlying lenses, and (ii) L(phi2∘phi1) and L(phi2)∘L(phi1) have the same put and get for all phi1:V→V', phi2:V'→V''. If either identity fails on a concrete instantiation (e.g., the paper's own counting tags), Proposition 2 is false; if both hold, the corruption is purely presentational and the verdict can be upgraded.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The most load-bearing assumption is Definition 2's commutation law put(T(s,v1,v2),v3) = T(put(s,v3),v1,v2). Note, however, that the reader's stated reason is not quite right: the induced put P(s,v)=put(T(s,g(s),v),v) satisfies putget by the underlying lens's putget alone, without using the tag axiom. The axiom is instead load-bearing for the central categorical claims: TL(C) is closed under sequential composition only if the composite tag again satisfies the law, and L is functorial only if the composite tag is chosen so that L(phi2∘phi1)=L(phi2)∘L(phi1). Proposition 2 defines the composite tag purely by a string diagram; in the arXiv text that diagram is corrupted and no algebraic formula is given. The appendix proof of the axiom for T_comp is likewise a sequence of unreadable diagram equalities. If the intended composite tag fails the law (e.g., because the diagram has been mangled), Proposition 2 is false, the category TL(C) does not exist, and the strict monoidal functor L collapses. Since the identity and associativity proofs are also diagrammatic, the central claim is currently unverifiable from the text as submitted.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces \"tagged lenses\": a vwb lens (get, put) equipped with a tag T:S×V×V→S satisfying the commutation law put(T(s,v1,v2),v3)=T(put(s,v3),v1,v2). Each tagged lens induces an ordinary lens P(s,v)=put(T(s,g(s),v),v). The paper proves that every induced lens satisfies putget, that change-depending tags (T(s,v,v)=s) force getput, and that first-last-depending tags (T(T(s,v,v'),v',v'')=T(s,v,v'')) force putput. It further claims that tagged lenses form a strict symmetric monoidal category TL(C), that change-depending and first-last-depending tags define symmetric monoidal subcategories, and that the induced-lens construction is a strict monoidal injective-on-objects functor L:TL(C)→pgL(C). The main text gives algebraic proofs for the getput entailment; the categorical and closure claims are relegated to diagrammatic appendix proofs.","tokens_in":11799,"tokens_out":5792,"duration_ms":53248,"significance":"If the categorical claims are correct, the paper gives a clean, elementary demonstration that lens laws can be entailed compositionally by simple side-effect laws, and the change-dependence/first-last-dependence distinction is a genuinely useful organising idea. The algebraic getput argument in Proposition 6 is correct: P(s,g(s))=put(T(s,g(s),g(s)),g(s))=put(s,g(s))=s. The putput argument in Proposition 7 also checks out algebraically when the tag commutation law and the underlying putput law are used. The examples are well chosen and illustrate the intended phenomena. However, the central category and functor claims (Propositions 2, 3, and 5) are not verifiable from the submitted text because their proofs are sequences of string-diagram equalities that are largely unreadable in the provided rendering, and no algebraic formula for the composite tag is supplied. This is a load-bearing gap that must be fixed before the paper can be accepted.","major_comments":[{"comment":"The sequential composition of tags is defined only by a string diagram; no pointwise or point-free algebraic formula for the composite tag T_comp is given. The proof of Proposition 2 then consists of a long chain of diagram equalities that are not legible in the submitted rendering: boxes and wires are misaligned, and several steps appear to duplicate or drop components. Since the tag commutation law is exactly what makes TL(C) a category, the existence of the category is not checkable as written. Please give an explicit algebraic definition of T_comp and a readable proof that it satisfies Definition 2.","section":"§4 and Appendix A"},{"comment":"Proposition 3, the strict monoidal functoriality of L:TL(C)→pgL(C), is proved only by diagrammatic equalities. The text says the composite tag is chosen so that L(ϕ2∘ϕ1)=L(ϕ2)∘L(ϕ1), but the proof that this equality holds with the displayed T_comp is unreadable. This is the second load-bearing claim of the paper. Please provide a direct algebraic verification of L(ϕ2∘ϕ1)=L(ϕ2)∘L(ϕ1), and similarly for the monoidal coherence.","section":"Appendix C"},{"comment":"The proof that first-last-depending tags are closed under sequential composition is again a long diagrammatic equality sequence and is not legible in the submitted text. This closure is needed for Proposition 5, i.e., for fldepTL(C) to be a subcategory. Since the paper's advertised contribution is compositional entailment, this closure proof must be checkable; please supply an algebraic proof.","section":"Appendix D"},{"comment":"The tag commutation law put(T(s,v1,v2),v3)=T(put(s,v3),v1,v2) is load-bearing: it is used in the proof that g∘T is trivial and in the putput argument, and the category TL(C) exists only if the composite tag again satisfies it. The paper does not explain why this specific law is the natural or minimal axiom. Please add a short discussion of the choice, ideally showing how the law is preserved by the composite-tag construction rather than merely asserting it.","section":"Definition 2"}],"minor_comments":[{"comment":"The abstract contains \"definetagged\" with a missing space; throughout the paper there are similar spacing issues, e.g., \"set-basedlenses\" and \"definetagged vwb-lenses\".","section":"Abstract and §1"},{"comment":"Examples 3, 4, 5, 6, and 7 each repeat the sentence \"Note that PutCount satisfies putget...\" even when the example is not PutCount; this is confusing and should be corrected so each example reports its own laws.","section":"Examples 3–7"},{"comment":"There is an inconsistency in the PutScaled example: Example 7 defines put((x,y),v)=(v,vy/x), while Example 10 defines the underlying put as ↑((x,y),v)=(v,y) and the tag as Scale((x,y),v,v')=(x,v'y/v). These formulas do not agree; please fix the typo and make the example self-consistent.","section":"Example 7 and Example 10"},{"comment":"The string-diagram notation is introduced only informally, and the appendix refers to colours (\"orange\", \"green\") that are not present in the monochrome rendering, making the intended picture impossible to reconstruct. Either include properly typeset coloured diagrams or replace the colour references with explicit wire labels.","section":"§2.2 and Appendix B"},{"comment":"The associativity proof contains an equality that appears to switch the order of T2 and T1 without comment and several steps where wires labelled ↑1, ↑2, g2, g3 are duplicated or dropped. If these are rendering artifacts, the source should be recompiled; otherwise the proof step is unjustified.","section":"Appendix A"}],"recommendation":"major_revision","confidential_remarks":"The core mathematical idea is simple and likely correct, and the algebraic parts of the paper that I could check (Propositions 6 and 7, and the getput entailment) are sound. The problem is that the central categorical claims rest on appendix proofs that are not readable in the submitted PDF. I would ask the editor to require the authors to replace the diagrammatic proofs with explicit algebraic definitions and proofs for the composite tag, associativity, unitality, and functoriality of L. This is a substantial but local revision, not a rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The new thing here is the tag morphism T: S×V×V→S together with the commutation law, and the observation that tag-level design laws entail lens laws. I checked the main entailments by hand. Change-depending tags give getput: P(s,g(s)) = put(T(s,g(s),g(s)), g(s)) = put(s,g(s)) = s. First-last-depending tags give putput, using the commutation law to move the tag inside the put. Those two results are correct and are a real, if modest, formalization of what Fischer–Hu–Pacheco and Nakano discussed heuristically.\n\nThe soft spot is the categorical framework. Propositions 2 and 3 claim TL(C) is a symmetric monoidal category and L is a strict monoidal functor, but the only proofs are string diagrams, and in the arXiv text those diagrams are corrupted to the point of being unreadable. The composite tag is defined only by a diagram; no algebraic formula is given. That matters because closure under composition of the tag commutation law is the load-bearing step. If the intended composite tag does not satisfy the law, the category does not exist and the functor collapses. I could not verify it from the text. That is a presentation failure, not evidence of a false claim, but it has to be fixed before the paper is usable.\n\nAlso minor: Examples 3–6 have copy-paste errors, saying “PutCount” instead of the actual example being defined. Section 5 defines change-depending as T(s,v,v)=id, which is a type error; it should be T(s,v,v)=s. And “strict symmetric monoidal” is asserted for TL(C) while C is only assumed cartesian monoidal; either assume strict cartesian or drop “strict.” The putget result in Proposition 1 is really just the underlying vwb putget, not a consequence of the tag axiom; that is harmless but the paper implies otherwise.\n\nWho is this for? People working on categorical optics and bidirectional transformations. The category/functor claims need a full algebraic proof before I would trust them, but the core idea and the getput/putput results are worth publishing. I would send it to review with a request for a rewritten appendix.","headline":"A genuinely new formalization of lens-law entailment via tags, with correct getput/putput proofs, but the central categorical claims are uncheckable because the appendix diagrams are corrupted and no algebraic composite-tag formula is given.","tokens_in":12288,"tokens_out":9695,"would_cite":true,"duration_ms":80916,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["18M05"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper proves that tagged lenses form a strict symmetric monoidal category, with a strict monoidal functor into the category of putget lenses; two additional tag laws independently force getput and putput.","keywords":["tagged lenses","lens laws","putget","very-well-behaved lenses","cartesian monoidal categories","symmetric monoidal categories","change-depending tags","first-last-depending tags"],"falsifier":"Checking in small finite sets whether every tuple satisfying the tag commutation axiom yields $g(\\mathrm{put}(T(s,g(s),v),v)) = v$ would settle Proposition 1; finding a single counterexample, or a composed tag that fails the commutation law, would refute the category and functor claims.","tokens_in":11276,"feed_emoji":"🏷️","tokens_out":5861,"duration_ms":49411,"temperature":0.7,"pith_summary":"Tagged lenses are a formal way to add side-effect counters to very-well-behaved lenses. The paper shows that whenever such a tag commutes with the lens's update operation, the induced lens automatically satisfies the putget law, and the tagged lenses themselves form a strict symmetric monoidal category. The induced-lens construction is then a strict monoidal functor into the category of putget lenses. Two additional design laws for tags—recording only genuine changes, or recording only first and last values—are shown to be compositional and to force the getput and putput laws respectively. Together these results give a categorical explanation of why relaxed lens laws can be understood through tag behaviour.","feed_headline":"Tagged lenses form a category that preserves putget","feed_subtitle":"One commutation rule for side-effect tags yields the putget law; two tag conditions force the other lens laws.","key_machinery":"The central object is a tag, a morphism $T: S \\times V \\times V \\to S$ recording a side effect indexed by the prior and future view values. The defining axiom requires the tag to commute with the underlying put: $\\mathrm{put}(T(s,v_1,v_2),v_3) = T(\\mathrm{put}(s,v_3),v_1,v_2)$, which also forces $g(T(s,v_1,v_2)) = g(s)$. From a tagged lens the induced put is $P(s,v) = \\mathrm{put}(T(s,g(s),v),v)$. Two tag laws carry the argument: change-dependence $T(s,v,v)=\\mathrm{id}$ makes trivial updates invisible, and first-last dependence $T(T(s,v,v'),v',v'')=T(s,v,v'')$ collapses intermediate updates. The composition rule for tags is chosen so that $L$ is functorial, and the proofs use string diagrams for cartesian monoidal categories.","core_discovery":"The central claim is that for every cartesian monoidal category $\\mathbb{C}$, tagged vwb-lenses form a strict symmetric monoidal category $\\mathrm{TL}(\\mathbb{C})$, and the construction sending a tagged lens $(\\mathrm{put}, g, T)$ to the putget lens with put $P(s,v) = \\mathrm{put}(T(s,g(s),v),v)$ is a strict symmetric monoidal, injective-on-objects functor $L: \\mathrm{TL}(\\mathbb{C}) \\to \\mathrm{pgL}(\\mathbb{C})$. The same construction guarantees putget for every tagged lens. If the tag is change-depending ($T(s,v,v)=\\mathrm{id}$), the induced lens additionally satisfies getput; if the tag is first-last-depending ($T(T(s,v,v'),v',v'')=T(s,v,v'')$), it additionally satisfies putput; a tag satisfying both induces a very-well-behaved lens. The paper's examples—counters, flags, and scaled views—are all recovered as induced lenses of such tags.","pith_inferences":["If the tag commutation axiom is the exact condition separating putget from the other lens laws, then relaxing or generalising that axiom should produce a taxonomy of partial lens-law entailments; the paper does not explore this.","The two tag laws could be tested for independence: since each forces a distinct lens law, a tag satisfying neither should induce a lens satisfying only putget, and the examples suggest such tags exist.","The construction is stated for cartesian monoidal categories; a natural extension would be to replace the copying and deletion structure by a non-cartesian monoidal structure, where the string-diagram proofs would need to be reworked.","Because composition, unitality, and associativity of tags all reduce to the same commutation axiom, any collection of putget lenses admitting a coherent tag assignment would automatically form a subcategory of $\\mathrm{pgL}(\\mathbb{C})$, suggesting a route to classifying which putget subcategories arise from tags."],"forward_implications":["Every tagged lens induces a putget lens, so tagged updates compose exactly as putget lenses compose, with the induced put factoring through the tag.","A change-depending tag is enough to upgrade putget to well-behaved: the induced lens satisfies getput.","A first-last-depending tag is enough to force putput, and combining both tag laws yields a very-well-behaved lens.","The subcategories of change-depending and first-last-depending tagged lenses are themselves symmetric monoidal, giving a chain of embeddings from tagged lenses down to vwb lenses.","Known examples like counters that record only changes, flags, and scaled views are unified as induced lenses of tags, with their lens laws following from the two tag laws rather than ad hoc checks."],"supporting_citations":[{"why":"Supplies the definition of very-well-behaved lenses and the putget, getput, and putput laws that tagged lenses build on.","marker":"[12]"},{"why":"Supplies the symmetric monoidal category of lenses over a cartesian monoidal category, whose composition the tagged-lens category mirrors.","marker":"[21]"},{"why":"Supplies the string-diagram presentation of cartesian monoidal categories used throughout the proofs.","marker":"[14]"}],"fun_headline_variants":["Tagged lenses form a category that forces putget","New lens category: tags enforce putget law","Tag conditions yield getput and putput lenses","Tagged lenses: a monoidal category preserving lens laws","Two tag properties unlock all lens laws"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"All results collapse if the requirement that a tag commute with the underlying put—$\\mathrm{put}(T(s,v_1,v_2),v_3) = T(\\mathrm{put}(s,v_3),v_1,v_2)$—is not the right way to model side effects, since the putget proof and the composition rule both depend on it.","fun_headline_variants_meta":{"raw":{"variants":["Tagged lenses form a category that forces putget","New lens category: tags enforce putget law","Tag conditions yield getput and putput lenses","Tagged lenses: a monoidal category preserving lens laws","Two tag properties unlock all lens laws"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000531,"raw_usage":{"total_tokens":2494,"prompt_tokens":821,"completion_tokens":1673,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":437,"completion_tokens_details":{"reasoning_tokens":1601}},"tokens_in":437,"tokens_out":1673,"duration_ms":11378,"temperature":1.0,"reasoning_tokens":1601,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T15:25:08.086994+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Checking in small finite sets whether every tuple satisfying the tag commutation axiom yields $g(\\mathrm{put}(T(s,g(s),v),v)) = v$ would settle Proposition 1; finding a single counterexample, or a composed tag that fails the commutation law, would refute the category and functor claims.","supporting_citations":[{"cited_title":"Categories of optics.arXiv: Category Theory, 2018","cited_arxiv_id":null,"evidence_quote":"Supplies the symmetric monoidal category of lenses over a cartesian monoidal category, whose composition the tagged-lens category mirrors."}],"review_version":1}