{"id":"6f00b97d-aee7-4c58-9bdc-2779f06d2ed8","arxiv_id":"2501.01363","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"In infinity-category theory, factorization systems embed fully faithfully into double infinity-categories, with an unstraightening theorem and a complete Z/2Z automorphism group for adequate systems.","lead":"This mathematics paper shows that two classical ways of structuring the arrows in a category, factorization systems and double categories, actually describe the same data in the infinite-categorical setting. The result gives a translation tool and computes the full symmetry group of an important subclass.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Construction 3.17 extends [HHLN23b, Prop. 4.8] from adequate triples to all factorization systems by assertion only; if that extension fails, the unit of the adjunction and hence Theorem 3.19 break.","rationale":"I agree with the reader that the most load-bearing point is the unit of the claimed equivalence, specifically the adequacy-independence assertion in Construction 3.17. The paper's main theorem is an equivalence, and the proof has two candidate weak spots: Lemma 3.12 leaves a combinatorial detail to the reader, and Construction 3.17 rests on an unverified generalization of HHLN23b Prop. 4.8. The second is more dangerous because it directly controls the natural transformation id => Cnr∘Fact; if it fails, there is no equivalence. I do not see an internal contradiction, and the claim that Prop. 4.8 does not use adequacy is plausible: for n=2 one can construct the inverse using the unique factorization of a composite, and recursive factorizations look as though they fill Ar([n]) without computing pullbacks. But plausibility is not a proof, and the paper is too dependent on that assertion to leave it as a remark. Therefore I keep the reader's conditional verdict rather than accepting or rejecting. The issue is a missing verification, not a demonstrated error.","tokens_in":16900,"tokens_out":25892,"duration_ms":270101,"concrete_test":"Independently re-derive the equivalence in Construction 3.17 without invoking adequacy. Concretely, open [HHLN23b, Prop. 4.8], list the steps of its proof, and mark every place where the assumption that ambigressive cospans have pullbacks is used. Then test a non-adequate factorization system: take a category with an ambigressive cospan lacking a pullback and equip it with an orthogonal factorization system (for example, one obtained by saturating a declared egressive class), and compute both sides of map_OFS(Ar([2]), C†) → map_Cat1([2], C) for n=2. If the two sides are not equivalent, Construction 3.17 is false and Theorem 3.19 needs an adequacy hypothesis; if they are equivalent and the proof of Prop. 4.8 nowhere invokes a pullback, the unit step is sound.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The unit of the claimed equivalence OFS ≅ DCat_OF is built in Construction 3.17 and Proposition 3.18. Construction 3.17 needs the natural map map_OFS(Ar([n]), C†) → map_Cat1([n], C) to be an equivalence for every factorization system C†. The paper cites [HHLN23b, Prop. 4.8] for this, although that result is stated for orthogonal adequate triples, and justifies the extension with the sentence 'the proof makes no essential use of the adequate triple property.' No verification is supplied. This is load-bearing: if the map fails for some non-adequate C†, then the functor C → cnr(Fact(C†)) is not an equivalence, so the unit id → Cnr∘Fact is not invertible and Theorem 3.19 does not follow. The gap is not merely cosmetic: adequate triples are exactly the factorization systems with pullbacks of ambigressive cospans (Definition 5.1, Lemma 5.2), and the construction of the inverse map for n ≥ 2 is where such pullbacks could enter. A second combinatorial check, the saturation claim in Lemma 3.12, is also left to the reader, but the unit of the adjunction is the more direct reliance.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper constructs a functor Fact from the ∞-category of orthogonal factorization systems to the ∞-category of double ∞-categories, and proves (Theorem 3.19) that it restricts to an equivalence OFS ≃ DCat_OF, where DCat_OF is the full subcategory of factorization double categories satisfying the cartesian condition of Proposition 3.1. The paper then proves an (un)straightening equivalence for (cocart,right)-fibrations of double categories (Theorem 4.6), uses it to identify curved orthofibrations and op-Gray fibrations of factorization systems with (cocart,right)- and (cart,right)-fibrations over the associated double categories (Proposition 4.5), and finally computes the automorphism group of the ∞-category of adequate factorization systems (Theorem 5.5).","tokens_in":17125,"tokens_out":4320,"duration_ms":40606,"significance":"If the main theorem is correct, the paper provides a clean and elegant equivalence between orthogonal factorization systems and a natural class of double ∞-categories, making precise a long-standing intuition and giving a functorial embedding that respects the ∞-categorical structure. The straightening theorem for (cocart,right)-fibrations and its specialization to orthofibrations of factorization systems is a useful contribution, and the computation of the automorphism group of the category of adequate factorization systems is a nice application. The paper is well organized, builds on a substantial body of prior work, and offers several explicitly constructed functors that will likely be reusable. The main weakness is a load-bearing unproven extension of a cited result from [HHLN23b] beyond its stated hypotheses.","major_comments":[{"comment":"The equivalence map_OFS(Ar([n]), C†) ≃ map_Cat1([n], C) is taken from [HHLN23b, Prop. 4.8], a result stated for orthogonal adequate triples. The paper extends it to all factorization systems by asserting that the proof 'makes no essential use of the adequate triple property', but no verification of this extension is provided. This equivalence is precisely the input that makes the natural transformation id =⇒ Cnr∘Fact an equivalence in Proposition 3.18, and it is therefore load-bearing for Theorem 3.19. If the extension fails for some non-adequate factorization system, the unit of the adjunction is not invertible and the main equivalence does not follow. Please supply a full proof that map_OFS(Ar([n]), C†) ≃ map_Cat1([n], C) holds for arbitrary factorization systems, or restrict the statement of Theorem 3.19 to the class for which the cited result is verified.","section":"Construction 3.17 and Proposition 3.18"},{"comment":"Lemma 3.12 asserts that the saturation of the single morphism (2) agrees with the spine inclusions (3). This claim is essential for Proposition 3.13, which establishes that cnr(C) is a complete Segal space exactly when C is a factorization double category, and hence is needed for the construction of the inverse functor Cnr. The proof leaves the crucial combinatorial verification to the reader: 'We leave the details to the reader' for the retract direction, and later 'an explicit combinatorial argument shows ... We leave the details to the reader' for the pushout square. Since the claim is nontrivial and load-bearing, please include a detailed proof of the saturation equality or provide a reference that contains it.","section":"Lemma 3.12"},{"comment":"Proposition 3.16, which proves that the counit of the adjunction is an equivalence, is dispatched by reducing to the cases m,n ≤ 1, excluding (1,1), and then saying that 'in the remaining three cases, one verifies that the map is an equivalence by unwinding the definitions.' These cases are the entire content of the counit equivalence in Theorem 3.19, and at least the case (m,n) = (1,0) is used again in the proof of Proposition 3.18. Please spell out these cases explicitly, or give a conceptual argument that covers them uniformly.","section":"Proposition 3.16"}],"minor_comments":[{"comment":"In the proof of Proposition 3.13, the sentence 'Similarly, one can show that it has a left inverse and so does f' appears garbled; presumably the intended statement is that g has a left inverse and so does f, or something analogous.","section":"Proposition 3.13"},{"comment":"In Definition 5.3, the line 'We denote the full subcategory of adequate factorization double categories by DCat ⊥ ⊂ DCat⊥' seems to contain a typo; the intended inclusion is probably DCat⊥ ⊂ DCat.","section":"Definition 5.3"},{"comment":"The reference [Ště23] spells the author's name as 'Miloslac ˇStˇ ep´ an' in the bibliography; please check and correct the spelling.","section":"References"},{"comment":"In Construction 3.17, the phrase 'embedding [n] into Ar([n]) by sending each element to the identity arrow' would benefit from a precise description of the functor; presumably it sends i to the identity morphism id_i of i.","section":"Construction 3.17"}],"recommendation":"major_revision","confidential_remarks":"The central concern is the unproven extension of [HHLN23b, Prop. 4.8] from adequate triples to all factorization systems in Construction 3.17. This is a load-bearing step, and the authors should be required to provide a proof or a precise citation that establishes the statement in the needed generality. The rest of the paper is promising and the issues seem fixable within the scope of a revision."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick read: this is a real result, not a repackaging. The paper constructs an ∞-categorical version of Stepan's 1-categorical embedding, proves an unstraightening equivalence for (cocart,right)-fibrations, and computes the automorphism group of the category of adequate factorization systems. Theorems A, B, and C go beyond the cited literature, and the citations are appropriate. No circularity; the reliance on HHLN23b is normal use of prior work.\n\nWhat I like: Theorem 3.19 gives exactly the right dictionary between orthogonal factorization systems and double categories satisfying the corner-filling condition. Theorem 4.6 is a substantive straightening result with independent value. Theorem 5.5, computing Aut(OFS⊥) ≅ Z/2Z, is a nice payoff that refines earlier results. The paper is clearly organized and the proof strategy is visible.\n\nSoft spots, in order of seriousness. Construction 3.17 extends [HHLN23b, Prop. 4.8] from adequate triples to all factorization systems with one sentence: “the proof makes no essential use of the adequate triple property.” That is load-bearing for the unit of the adjunction and thus for Theorem 3.19. The stress-test note is right to flag it. I do not think it is fatal—Prop 4.8 plausibly uses orthogonality and completeness rather than pullbacks of ambigressive cospans—but the paper should prove the extension or at least state it as a lemma with a proof sketch. As written, it is an unverified assertion in the middle of the main theorem. Second, Lemma 3.12, which supplies the saturation that makes cnr land in Segal spaces, leaves “the details to the reader” twice. The described combinatorial strategy probably works, but for a central lemma it is under-supplied. Third, the proof of Theorem 5.5 has several “a computation shows” and “it turns out” steps; these should be filled in or moved to an appendix.\n\nNone of this changes my overall read. The central argument is credible and the gaps are verification gaps, not conceptual mismatches. The paper deserves a serious referee. I would send it to peer review and ask the author to firm up Construction 3.17 and Lemma 3.12 before acceptance. Anyone working with factorization systems, double ∞-categories, or straightening results will get value from this paper; I would bring it to a reading group and would cite Theorem 3.19 in my own work.","headline":"A credible, genuinely new dictionary between factorization systems and double ∞-categories, with one load-bearing extension claim that needs proof before acceptance.","tokens_in":17677,"tokens_out":2551,"would_cite":true,"duration_ms":26314,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["18N45","18N40"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper proves that the ∞-category of orthogonal factorization systems is equivalent to the ∞-category of factorization double categories, via an explicit pair of functors Fact and Cnr, and derives an (un)straightening equivalence for…","keywords":["orthogonal factorization systems","double ∞-categories","∞-categories","Segal spaces","fibrations","straightening","span category","adequate triples"],"falsifier":"A direct computation of the unit map for a non-adequate factorization system would settle the matter: if for some system $C^\\dagger$ and some $n \\ge 1$ the map $\\mathrm{map}_{\\mathrm{OFS}}(\\mathrm{Ar}([n]), C^\\dagger) \\to \\mathrm{map}_{\\mathrm{Cat}_1}([n], C)$ is not a homotopy equivalence, then Proposition 3.18 fails and Theorem 3.19 is false. The paper gives no example, so testing any non-adequate system, such as a category admitting an ambigressive square that is not a pullback, would resolve the gap.","tokens_in":16615,"feed_emoji":"🔷","tokens_out":10896,"duration_ms":93008,"temperature":0.7,"pith_summary":"The paper establishes a full and faithful embedding of orthogonal factorization systems into double $\\infty$-categories, and proves the embedding is an equivalence onto the subcategory of 'factorization double categories'—those double categories in which every bottom-left corner has a unique square filler. This makes precise the classical intuition that double categories generalize orthogonal factorization systems: the 'wrong order' composition of an egressive and an ingressive morphism is uniquely rewritten in the correct order, which is exactly the lifting property of a factorization system. The author also proves an (un)straightening equivalence for double $\\infty$-categories, showing that certain fibrations over a double category are classified by maps into a specific double category, and recovers the span category construction of adequate factorization systems as the horizontal opposite.","feed_headline":"Factorization systems are double categories in disguise","feed_subtitle":"An equivalence of ∞-categories makes this classical analogy exact, with new results on fibrations and span categories.","key_machinery":"The load-bearing object is the functor $\\mathrm{Fact}$ (Construction 3.3), defined by restricting the Yoneda embedding along the bicosimplicial object $([m],[n]) \\mapsto [m] \\bar{\\times} [n]$, where the factorization system on $[m] \\times [n]$ has egressive morphisms those constant in the second factor and ingressive those constant in the first. The inverse functor $\\mathrm{Cnr}$ (Construction 3.14) sends a factorization double category to its 'category of corners': the complete Segal space $\\mathrm{cnr}(C)$ with $C(-,0)$ and $C(0,-)$ as the two subcategories. The equivalence is proved by showing the unit (Proposition 3.18) and counit (Proposition 3.16) are natural equivalences; the counit uses the Segal and factorization conditions, while the unit relies on the equivalence $\\mathrm{map}_{\\mathrm{OFS}}(\\mathrm{Ar}([n]), C^{\\dagger}) \\simeq \\mathrm{map}_{\\mathrm{Cat}_1}([n], C)$ imported from [HHLN23b, Prop. 4.8]. The cartesian condition of Proposition 3.1—that $C(1,1)$ is the pullback of $C(1,0)$ and $C(0,1)$ over $C(0,0)$—characterizes the essential image.","core_discovery":"The central claim is Theorem 3.19: the functor $\\mathrm{Fact} : \\mathrm{OFS} \\to \\mathrm{DCat}$, sending a factorization system $C^{\\dagger} = (C, C_{\\mathrm{eg}}, C_{\\mathrm{in}})$ to the double $\\infty$-category with horizontal morphisms the egressive maps and vertical morphisms the ingressive maps, induces an equivalence of $\\infty$-categories $\\mathrm{OFS} \\simeq \\mathrm{DCat}_{\\mathrm{OF}}$, where $\\mathrm{DCat}_{\\mathrm{OF}}$ is the full subcategory of double $\\infty$-categories satisfying the cartesian condition of Proposition 3.1—equivalently, double categories in which every 'corner' has a unique square filling it. The inverse $\\mathrm{Cnr}$ sends a factorization double category to its category of corners, with the vertical and horizontal morphisms as the two classes. The paper further shows that curved orthofibrations and op-Gray fibrations over $C^{\\dagger}$ correspond exactly to (cocart,right)- and (cart,right)-fibrations over $\\mathrm{Fact}(C^{\\dagger})$, and that the (un)straightening equivalence of Theorem 4.6 restricts to these classes. Finally, the automorphism group of the $\\infty$-category of adequate factorization systems is $\\mathbb{Z}/2\\mathbb{Z}$, generated by the span category construction, which is shown to coincide with taking the horizontal opposite of $\\mathrm{Fact}(C^{\\dagger})$.","pith_inferences":["If the unproved extension of [HHLN23b, Prop. 4.8] fails, Theorem 3.19 would reduce to a statement about adequate systems; the paper itself only needs the general statement for Theorem A, so checking that extension is the most direct test of the main result.","The corner-filling condition suggests a concrete recipe for building factorization systems from double categories: given any double $\\infty$-category, take the subcategory of 'corners' that are uniquely fillable and see whether the two morphism classes are closed under composition.","The automorphism computation for adequate systems may generalize to other full subcategories of factorization systems defined by closure properties, where the horizontal-opposite operation would still provide an involution."],"forward_implications":["Every orthogonal factorization system is completely determined by its factorization double category, so the two theories are equivalent and factorization systems can be studied through the well-developed machinery of double $\\infty$-categories.","Curved orthofibrations and op-Gray fibrations over a factorization system are exactly (cocart,right)- and (cart,right)-fibrations over the associated double category, so fibrations of double categories subsume the earlier notion.","The (un)straightening equivalence of Theorem 4.6 classifies (cocart,right)-fibrations over a double category by maps into the large double category $\\mathrm{Sq}^{\\mathrm{oplax}}(\\mathrm{Cat}_1^{(2)})$, giving a uniform straightening statement.","For adequate factorization systems, the span category functor is the same as taking the horizontal opposite of the associated double category, and the only other automorphism is the identity, so there are no hidden symmetries of the adequate theory."],"supporting_citations":[{"why":"Supplies the equivalence map_OFS(Ar([n]), C†) ≅ map_Cat1([n], C) that Construction 3.17 and Proposition 3.18 depend on; the paper extends it beyond adequate triples.","marker":"[HHLN23b, Prop. 4.8]"},{"why":"Provides the definition of double ∞-categories and of (cocart,right)-fibrations used throughout, and Theorem 4.6 fulfills the expectation recorded in [Nui24, Rem. 2.14].","marker":"[Nui24]"},{"why":"Characterizes factorization systems by the restricted composition map being an equivalence, a fact used in Lemma 3.4 and Proposition 3.18.","marker":"[BS24, Prop. A.0.4]"},{"why":"Joyal–Tierney embedding of categories into complete Segal spaces is used to identify Fact(C†) as a double category and cnr(C) as a category.","marker":"[JT07]"},{"why":"Supplies the right Kan extension strategy used in the proof of the (un)straightening equivalence Theorem 4.6.","marker":"[AF20]"},{"why":"Establishes that the span category functor is an automorphism of adequate factorization systems, used in Corollary 5.6 and Theorem 5.5.","marker":"[HHLN23b, Thm. 4.12]"}],"fun_headline_variants":["Factorization systems are double categories, ∞-categorically","Double ∞-categories capture all factorization systems","An ∞-equivalence: factorization systems meet double categories","Factorization systems shown equivalent to double categories","The hidden double life of factorization systems"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The paper assumes, without proving it, that a certain comparison between mapping spaces that was previously proved for 'adequate' factorization systems also holds for all factorization systems; this step is what makes the inverse construction a true inverse, and if it fails the whole equivalence collapses.","fun_headline_variants_meta":{"raw":{"variants":["Factorization systems are double categories, ∞-categorically","Double ∞-categories capture all factorization systems","An ∞-equivalence: factorization systems meet double categories","Factorization systems shown equivalent to double categories","The hidden double life of factorization systems"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000264,"raw_usage":{"total_tokens":1579,"prompt_tokens":894,"completion_tokens":685,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":510,"completion_tokens_details":{"reasoning_tokens":615}},"tokens_in":510,"tokens_out":685,"duration_ms":7220,"temperature":1.0,"reasoning_tokens":615,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T22:28:36.572047+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"A direct computation of the unit map for a non-adequate factorization system would settle the matter: if for some system $C^\\dagger$ and some $n \\ge 1$ the map $\\mathrm{map}_{\\mathrm{OFS}}(\\mathrm{Ar}([n]), C^\\dagger) \\to \\mathrm{map}_{\\mathrm{Cat}_1}([n], C)$ is not a homotopy equivalence, then Proposition 3.18 fails and Theorem 3.19 is false. The paper gives no example, so testing any non-adequate system, such as a category admitting an ambigressive square that is not a pullback, would resolve the gap.","supporting_citations":[],"review_version":1}