{"id":"11a1f3da-ff71-4ca9-a068-d51ca970cebb","arxiv_id":"2601.21843","paper_version":2,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"low","formal_verification":"full","parameter_count":0,"one_line_summary":"A Segal type — a type with unique (2,1)-horn fillers — has unique fillers for every inner (n,k)-horn.","lead":"This mathematics paper proves that in homotopy type theory with a directed interval, if two composable arrows always have a unique filling triangle, then every higher-dimensional compositional coherence condition automatically holds. The proof is formalized in Cubical Agda, so a computer checked it.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified","rationale":"The reader's weakest assumption pointed to the interval's lattice structure and to Remark 4.10 regarding set-pushouts. I do not regard either as load-bearing. The lattice structure is an explicit framework axiom, not a hidden assumption; without it the retraction could not be defined, but with it the argument works. The set-pushout remark is not used in the formal construction: the retract diagram is built in the wild category of types using the elimination principle of the pushout, so no transfer from set-pushouts is needed. I also checked the boundary cases in the definition of r (i≤k vs i>k, the cases y1=1 and y2=0) and they are handled correctly, relying only on 0<k<n. The formalization, if it type-checks as claimed, would be decisive evidence. The only blemish I found is a typo in the definition of ≤, but the surrounding text and the proof itself unambiguously use the standard order. Therefore I recommend no change to the ACCEPT verdict.","tokens_in":14182,"tokens_out":28632,"duration_ms":283998,"concrete_test":"Recompile the Cubical Agda formalization at the pinned commit (Agda 2.8.0, cubical library commit a6cf6b5) and confirm that the Theorem 4.9 retraction equations type-check. As an additional independent check, verify by hand the pointwise identity r∘s = id using the absorption laws with the intended order x≤y iff x∧y=x; if either step fails, the central claim would need revision.","verdict_should_be":"UNCHANGED","load_bearing_attack":"I reviewed the central proof of Theorem 4.9 and found no load-bearing gap. The retraction r is constructed directly in the wild category of types via the HIT pushout eliminator, and the required algebraic identities are exactly the stated bounded distributive lattice laws. The proof of r∘s = id uses absorption (x∨(x∧y)=x and x∧(x∨y)=x) with the intended order where 0 is bottom and 1 is top; a small typo in the displayed definition of ≤ (x∧y=y instead of x∧y=x) is corrected by the surrounding text and footnote, and does not affect the formalized statement. Remark 4.10's set-pushout discussion is not load-bearing: the construction does not transfer a set-pushout retract to types but defines r out of the type-theoretic pushout directly, so the preservation claim is explanatory rather than essential. The claimed full Cubical Agda formalization provides strong independent support. I therefore do not see a concrete mathematical weakness that threatens Theorem 4.9.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper works in homotopy type theory with a postulated interval type I assumed to be a set equipped with a bounded distributive lattice structure. It develops the Leibniz adjunction for the wild category of types: the pushout-product is left adjoint to the pullback-hom (Theorem 3.16), proved via an equivalence between the wild category of maps and the wild category of families. Using this, it proves Theorem 4.9: every inner horn inclusion λ^n_k is inner anodyne, so that any type with unique fillers for the (2,1)-horn has unique fillers for all inner (n,k)-horns. The proof constructs a retraction of λ^n_k onto λ^n_k b× λ²₁ via the lattice operations and transfers orthogonality using the Leibniz adjunction and closure properties. The results are claimed to be fully formalized in Cubical Agda, with /cog links to the formalization.","tokens_in":14358,"tokens_out":19394,"duration_ms":195708,"significance":"If correct, this is a substantial contribution to simplicial type theory. It internalizes and generalizes Riehl–Shulman's Proposition 5.12 from n=3 to all n, turning a meta-theoretic schema into a single theorem inside HoTT with an internal interval. The proof strategy via the Leibniz adjunction is elegant and the assumptions on the interval are minimal (no totality, no modalities). The formalization is a major strength: the paper pins Agda 2.8.0 and a specific Cubical library commit, and nearly every key statement is linked to a machine-checked proof. No ad-hoc axioms beyond the bounded distributive lattice structure are introduced, and the derivation is parameter-free. The paper should be of significant interest to the HoTT and higher-category communities.","major_comments":[],"minor_comments":[{"comment":"The displayed definition 'x ≤ y (and y ≥ x) for x ∧ y = y' is backwards: in a lattice the standard convention is x ≤ y iff x ∧ y = x (equivalently x ∨ y = y, as the footnote says). The surrounding text and the proof of Theorem 4.9 use the intended order, so this is a presentation typo, but it should be corrected.","section":"§4.2, definition of ≤"},{"comment":"The equivalence 'Λ²₁ ≃ Σ(x, y : I). (x = 0) ∨ (y = 1)' appears to have the two sides swapped. With the convention x = x₁, y = x₂, the condition should read (x = 1) ∨ (y = 0). The proof of Theorem 4.9 correctly uses 'y₁ = 1 or y₂ = 0', so the error is local and does not affect the main argument.","section":"§4.2, displayed equivalence for Λ²₁"},{"comment":"In the statement of Proposition 3.7, the first displayed type writes 'Fam((A, B) ⋔ (A′, B′); ...)' where the pushout-product '(A, B) b× (A′, B′)' is clearly intended. This notational slip could confuse readers.","section":"§3.1.2 / Proposition 3.7"},{"comment":"In the final sentence of the proof, 'the codomain ∆ 2 is a set' should read '∆n': the lower horizontal row in diagram (4) has codomain ∆n. The point that the relevant hom types are sets because ∆n is a set is correct, but the symbol is wrong.","section":"§4.2, proof of Theorem 4.9"},{"comment":"The verification that rcod maps into ∆n (in particular the decreasing condition at the seam i = k, k+1) is summarized rather than shown in detail. The argument follows from monotonicity of the lattice operations and the assumptions 0 < k < n, and the /cog formalization covers it; adding one sentence with the lattice identity would improve readability.","section":"§4.2, proof of Theorem 4.9"}],"recommendation":"minor_revision","confidential_remarks":"The central mathematical claim is sound and the formalization is a strong asset. The requested changes are purely local notation fixes and a small addition for readability. I would support acceptance after these edits are made; I chose minor_revision only to ensure the typos are corrected before publication."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper's central result is exactly what the title says: in simplicial type theory with an internal interval, every Segal type has unique fillers for all inner (n,k)-horns. That is a genuine advance over Riehl–Shulman, who only got n=3 and whose statement is necessarily meta-theoretic. The new technical core is the Leibniz adjunction internalized in the wild category of types, proved via the equivalence between maps and families. That is a real tool, not just a stepping stone. The Cubical Agda formalization is the strongest part of the package: the paper pins Agda 2.8.0 and a specific cubical library commit, and nearly every key claim carries a /cog link to the code. I did not run the Agda myself, but the evidence is concrete and checkable, which puts this well above the typical \"formalized in principle\" claim.\n\nThe proof of Theorem 4.9 is a retract argument: the inner horn inclusion λₙₖ is a retract of λₙₖ ⊗ λ²₁, and the algebraic identities needed for the retraction are exactly the bounded distributive lattice laws on the interval. I read the retraction definition and the composition check; it works. The interval being a bounded distributive lattice is an extra axiom, but it is explicit, mild, and not hidden. The one delicate point is Remark 4.10 about set-pushouts not automatically being homotopy pushouts. That remark is slightly hand-wavy, but the stress-test is right that it is not load-bearing: the retraction is defined directly in types, not transferred from sets. There is also a small typo in the displayed definition of ≤ (x∧y=y rather than x∧y=x), but the surrounding text and footnote correct it, and it does not affect the formalized statements.\n\nThe authors are also honest about the cost of their internal approach: Section 5 admits that the meta-theoretic version is easier precisely because definitional equalities make it set-based. That is a fair trade-off, not a flaw. On citations, they acknowledge Bakke and Toth's prior Agda work and explain what is new here; I see no citation problem.\n\nThis paper should go to a serious referee. It is a strong candidate to become a standard citation in synthetic ∞-category theory and formalized HoTT. I would cite it and would bring it to a reading group.","headline":"Solid, machine-checked proof that all inner horn inclusions follow from the Segal condition in simplicial type theory—worth serious referee time.","tokens_in":14903,"tokens_out":1600,"would_cite":true,"duration_ms":17734,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B38","18N65"],"pacs":[],"model":"deepseek-v4-flash","headline":"The Segal composition condition forces all higher coherences in directed type theory","keywords":["homotopy type theory","simplicial type theory","Segal types","inner anodyne maps","Leibniz adjunction","pushout-product","pullback-hom","orthogonality"],"falsifier":"Construct a model of homotopy type theory with an interval that is a bounded distributive lattice but where a type has unique (2,1)-horn fillers yet lacks a unique filler for some inner (n,k)-horn; in particular, test the specific lattice identities x∨(x∧y)=x and x∧(x∨y)=x that make r∘s equal the identity.","tokens_in":14035,"feed_emoji":"🔺","tokens_out":5376,"duration_ms":50224,"temperature":0.7,"pith_summary":"The paper proves that in homotopy type theory with a postulated interval type, the single requirement that directed morphisms compose — the Segal condition, unique fillers for the basic (2,1)-horn — automatically forces unique fillers for every inner horn in every dimension. This collapses the infinite hierarchy of higher coherences of directed types into one condition, generalizing an earlier result that covered only the 3-dimensional case. The proof is carried out internally, using an adjunction between pushout-product and pullback-hom in the 'wild' category of types, together with a classical retract argument. A machine-checked formalization accompanies the paper, so the combinatorial bookkeeping is verified.","feed_headline":"One composition condition fills all inner horns","feed_subtitle":"In directed type theory, a single 2-horn filler rule forces unique fillers in every dimension.","key_machinery":"The pushout-product functor, left adjoint to the pullback-hom, in the wild category of types. The adjunction is proved via the equivalence between the wild category of maps and the wild category of families, a consequence of the univalence axiom; this shifts the work to a setting where the definitions are simpler. The interval type is assumed to form a bounded distributive lattice, and its operations define the retraction r(x,y)_i = x_i ∨ y_1 for i ≤ k and x_i ∧ y_2 for i > k; the lattice laws ensure that r composed with the section s is the identity.","core_discovery":"The central claim is Theorem 4.9: for every n and every inner k, the horn inclusion λⁿₖ is inner anodyne, meaning any Segal type has unique fillers for all inner (n,k)-horns. The proof exhibits λⁿₖ as a retract of the pushout-product λⁿₖ ×̂ λ²₁, then uses the Leibniz adjunction and closure properties of orthogonality to transfer the Segal property from λ²₁ to λⁿₖ. This is an internal version of a classical quasi-category result, obtained in plain homotopy type theory with an interval merely assumed to be a bounded distributive lattice.","pith_inferences":["The same retract formula might adapt to prove outer horn lifting under additional assumptions on the interval, opening a route to synthetic weak factorization systems.","The internal Leibniz adjunction could serve as a foundation for developing quasi-category theory synthetically, such as the theory of (∞,1)-categories, without moving to a two-level type theory.","The proof's reliance on distributive lattice laws suggests a testable boundary: if the interval is only a poset or lacks distributivity, the specific retraction no longer composes to the identity, and the theorem may fail."],"forward_implications":["Segal types in this setting satisfy the full inner horn lifting condition, so composition, associativity, and all higher coherences follow from a single axiom.","The closure of left-orthogonal maps under pushout-products and retracts becomes a general toolkit for orthogonality arguments in homotopy type theory.","The result extends from Segal types to Segal fibrations: any map right orthogonal to the (2,1)-horn inclusion is right orthogonal to every inner horn inclusion.","Because the interval needs only a bounded distributive lattice structure, the theorem applies to a wide family of interval types, not just the total order."],"fun_headline_variants":["One 2-horn rule fills all inner horns, proven in Cubical Agda","Unique fillers for (2,1)-horns imply all inner horns in simplicial HoTT","The Leibniz adjunction: a single Segal condition suffices for all dimensions","In directed type theory, one horn filler condition forces every inner horn"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The argument assumes the interval type is a bounded distributive lattice satisfying the stated absorption, commutativity, associativity, and distributivity equations; if the lattice laws fail, the retraction r∘s is not provably the identity, and the transfer collapses.","fun_headline_variants_meta":{"raw":{"variants":["One 2-horn rule fills all inner horns, proven in Cubical Agda","Unique fillers for (2,1)-horns imply all inner horns in simplicial HoTT","The Leibniz adjunction: a single Segal condition suffices for all dimensions","In directed type theory, one horn filler condition forces every inner horn"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000879,"raw_usage":{"total_tokens":3643,"prompt_tokens":755,"completion_tokens":2888,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":499,"completion_tokens_details":{"reasoning_tokens":2799}},"tokens_in":499,"tokens_out":2888,"duration_ms":21239,"temperature":1.0,"reasoning_tokens":2799,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-03T06:44:04.383870+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Construct a model of homotopy type theory with an interval that is a bounded distributive lattice but where a type has unique (2,1)-horn fillers yet lacks a unique filler for some inner (n,k)-horn; in particular, test the specific lattice identities x∨(x∧y)=x and x∧(x∨y)=x that make r∘s equal the identity.","supporting_citations":[],"review_version":1}