{"id":"8b12c9f3-aaf3-429f-ae54-7d53b660cb11","arxiv_id":"1908.08488","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"A direct construction of dependent products in toposes using power objects and finite limits, with a concrete site-level formula for Grothendieck toposes.","lead":"Dependent products are a core operation in topos theory, the categorical setting for constructive logic and type theory. This note gives a new one-step recipe for building them using only power objects and finite limits, plus an explicit site-level formula for Grothendieck toposes.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The Grothendieck description depends on the unproved equivalence of Prop. 2.1, cited from [6]; if that equivalence or the definition of J_P is wrong, the site-level formula does not follow.","rationale":"The reader's conditional verdict matches my independent reading. I looked for a genuine flaw in Section 1: the internal-language formula is bounded, the subobjects S, T^f_1, T^h_2 correspond exactly to the three clauses of the formula, and Lemma 1.2 supplies the graph-theoretic bijection behind Theorem 1.3. The naturality assertion is abbreviated but is a standard classifying-arrow chase, so I do not see an error in the elementary theorem. For the Grothendieck half, however, every formula in Section 2 is mediated by Proposition 2.1, and the text's proof is only a reference to the companion preprint [6]. The topology J_P is defined by an image condition that is not accompanied by a verification, and the equivalence for a non-sheaf P is not a standard textbook result. This is the same weakest assumption the reader identified. The requested proof or standard reference is therefore a legitimate condition, not a rejection. Because the reader already marked the paper CONDITIONAL, my stress test does not move the verdict.","tokens_in":13448,"tokens_out":37893,"duration_ms":399519,"concrete_test":"Check [6, Section 5.7] for the exact statement and then test the non-sheaf case on a minimal site: let C have two objects U,V with one arrow i:V→U, let J be generated by {i} on U, and take P with P(U)=∅ and P(V)={a,b}, so that a(P) is the constant sheaf at {a,b}. Compute Sh(C,J)/a(P) and Sh(∫P,J_P) explicitly with J_P defined by π_P-images, and verify that LJ_P and RJ_P are inverse equivalences by checking the unit and counit are isomorphisms on the two generating objects. If the equivalence fails, or if the topology must instead be generated by pullbacks of J-covering sieves, then Corollary 2.4 is not established as stated.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The elementary part of the paper is internally coherent: the bounded internal-language formula in Proposition 1.1 matches the subobjects S, T^f_1 and T^h_2 in Theorem 1.3, and Lemma 1.2 gives the required graph-theoretic bijection. The naturality assertion in Theorem 1.3 is brief, but it is a routine diagram chase with classifying arrows. The genuinely fragile premise is in Section 2: Theorem 2.2 and Corollary 2.4 transfer the dependent product ∏_{a(f)} to the direct image C(∫f)_* through the equivalence Sh(C,J)/a(P) ≃ Sh(∫P,J_P) of Proposition 2.1. That proposition is not proved in this paper; its proof is a citation to [6, Section 5.7], and the topology J_P is defined by the condition that a sieve is covering exactly when π_P sends it to a J-covering sieve. This definition is plausible and standard when P is a J-sheaf, but Corollary 2.4's first statement needs it for an arbitrary presheaf P. No verification of the topology axioms or of the unit/counit isomorphisms for the restriction of L_P⊣R_P is supplied here. If J_P or the equivalence is not exactly as stated, the identification ∏_{a(f)} = a_Q∘∏^{pr}_f∘i_P and the pointwise formula in Corollary 2.4 do not follow. This is the load-bearing assumption for the Grothendieck topos description.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper proposes an explicit construction of the dependent product functor ∏_f : E/P → E/Q in an elementary topos E, avoiding the usual two-step procedure through slices. For f:P→Q and h:H→P, the object ∏_f[h] is identified with the intersection of three subobjects of Q×P(H×P): the universal quantification ∀_{f×1}(S) of the functionality subobject S, the fiber condition T^f_1, and the graph condition T^h_2. The authors prove (Theorem 1.3) that this object with the projection to Q satisfies the universal property, via Lemma 1.2 which translates the factorization conditions into the properties of the graph of a morphism. They also give an elementary description of ∀ in terms of power objects (Proposition 1.4), simplify the intersection T^f_1 ∩ T^h_2 (Proposition 1.5), and show compatibility with subtoposes (Proposition 1.6). In Section 2, for a Grothendieck topos Sh(C,J), the paper describes the dependent product along a morphism f:P→Q in the topos via the equivalence Sh(C,J)/a(P) ≃ Sh(∫P, J_P) (Proposition 2.1, cited from the companion preprint [6]), leading to the identification ∏_{a(f)} ≅ a_Q ∘ ∏^{pr}_f ∘ i_P and an explicit pointwise formula (Corollary 2.4).","tokens_in":13748,"tokens_out":5592,"duration_ms":50537,"significance":"If all claims hold, the paper provides a genuinely alternative one-step construction of dependent products in elementary toposes, built only from power objects and finite limits, and a concrete site-level formula for Grothendieck toposes that may be useful for explicit computations. The main elementary construction is self-contained and the proof is based on a clear analysis of subobjects of H×P×K; the internal-language motivation in Proposition 1.1 is well matched by the categorical formulation. The paper honestly notes where the proof depends on external results: Proposition 2.1 is deferred to [6]. The site-level description is the most significant potential contribution but also the most fragile part, as discussed below.","major_comments":[{"comment":"The equivalence Sh(C,J)/a(P) ≃ Sh(∫P, J_P) is stated without proof, with a citation to the authors' unpublished preprint [6, Section 5.7]. This proposition is load-bearing for Theorem 2.2 and Corollary 2.4, and its topology J_P is defined for an arbitrary presheaf P, although the standard construction is only well-established for sheaves. The paper should either provide a proof of Proposition 2.1 (including the verification that J_P is a Grothendieck topology and that the unit and counit of the adjunction L^J_P ⊣ R^J_P are isomorphisms) or explicitly state Theorem 2.2 and Corollary 2.4 as conditional on the companion preprint, with a clear statement of the exact hypotheses needed. As written, the site-theoretic description is not self-contained.","section":"Section 2, Proposition 2.1"},{"comment":"The proof establishes the bijective correspondence for each object [k], but the naturality of this correspondence is asserted in a single sentence: 'The naturality of this correspondence is immediate, as all the arrows involved in it are defined by universal properties.' Since the theorem claims a natural isomorphism of functors, the proof should at least sketch the verification: given a morphism [k]→[k'] in E/Q, one must show that the two constructions (from α to ⟨k,β⟩ and back) commute with the induced maps. This is likely a routine diagram chase, but the current level of detail leaves the central adjunction property incomplete.","section":"Section 1, Theorem 1.3"}],"minor_comments":[{"comment":"There are typographical errors in the abstract: 'i n' and 'constructi on' should be corrected to 'in' and 'construction'.","section":"Abstract, p. 2"},{"comment":"The use of the character よ for the Yoneda embedding is unusual and the accompanying reference to an nLab revision is not stable; consider introducing the notation in words and citing a standard textbook instead.","section":"Notation, p. 3"},{"comment":"The rectangle at the beginning of the proof is helpful, but the definition of the lower composite arrow τ is not repeated; consider restating it in the caption or just before the diagram for readability.","section":"Lemma 1.2, proof"},{"comment":"The phrase 'whose sieves are precisely those sent to J-covering sieves by the canonical functor π_P' is imprecise; it should say that a sieve R on (X,p) is J_P-covering if and only if π_P(R) generates a J-covering sieve on X (or an equivalent explicit condition).","section":"Proposition 2.1"},{"comment":"The displayed formula for A^h_f(X) is difficult to parse; the set notation should be reformatted, and the condition involving H(γ)(x_{g,p}) = x_{g∘γ, P(γ)(p)} needs a clearer explanation of the indexing.","section":"Corollary 2.4"},{"comment":"Reference [6] is the authors' own preprint; it should be flagged as a companion paper, and ideally the relevant statement (Proposition 2.1) should be summarized in an appendix or the dependence removed.","section":"Reference [6]"}],"recommendation":"major_revision","confidential_remarks":"The heavy reliance on the companion preprint [6] for Proposition 2.1 is a concern for the integrity of the Section 2 results. The editor may wish to verify that [6] is publicly available in a stable form and that the cited statement is indeed proved there. If [6] is not intended for publication, the paper should be revised to include a proof of Proposition 2.1 or the Grothendieck results should be labeled as conditional."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's my read. The paper delivers exactly what the title says: an explicit construction of the dependent product in an elementary topos using only power objects and finite limits, plus a site-level description for Grothendieck toposes. The elementary part is the real contribution. Bell already had the internal-language formula, but the categorical packaging — Thm 1.3 expressing ∏_f[h] as ∀_{f×1}(S)∩T^f_1∩T^h_2 — is new and clean. Lemma 1.2 does the work, and Prop 1.4 gives a nice elementary handle on ∀. I checked the diagram chases; they're fine. The naturality assertion in Thm 1.3 is compressed to 'immediate', which is a bit quick, but it's a routine universal-property argument; a referee can ask for the diagram but it's not a correctness risk.\n\nThe Grothendieck section is more fragile. The whole thing rests on Prop 2.1, the equivalence Sh(C,J)/a(P) ≃ Sh(∫P,J_P), which is not proved here. The proof is a citation to the authors' companion preprint [6, Sec 5.7]. The stress-test note is right: that's load-bearing, especially for the arbitrary-presheaf case in Cor 2.4's first statement. The 'in particular' assumes P,Q are sheaves, where RJ_P is the restriction of RP, but the general formula for arbitrary presheaves depends on Prop 2.1 in its full generality. If there's a flaw in the definition of J_P or in the equivalence, the site-level description collapses. The authors should either prove it in this paper or point to a published version of [6]. Self-citation alone doesn't bother me; the cited result is used as an external equivalence theorem, not as an input that forces the conclusion.\n\nAlso worth saying: the paper is honest. It doesn't pretend to solve an open problem or claim the construction is 'better' — it says it's a one-step construction with a different flavor. I believe the elementary part works. The Grothendieck part is conditional.\n\nWho's this for? Specialists in topos theory, categorical logic, and anyone who wants an explicit formula for dependent products. It deserves referee time. The fix is straightforward: expand the naturality proof, and provide a self-contained proof of Prop 2.1 or a citation to a peer-reviewed source. I'd send it to a serious referee with that request.","headline":"A genuinely useful elementary formula for dependent products, with a Grothendieck section that hinges on an unproved equivalence from the authors' companion preprint.","tokens_in":14267,"tokens_out":2949,"would_cite":true,"duration_ms":27820,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["18B25","18F10","03G30"],"pacs":[],"model":"deepseek-v4-flash","headline":"The dependent product in any elementary topos admits an explicit construction from power objects and finite limits.","keywords":["dependent product","elementary topos","Grothendieck topos","power objects","slice topos","category of elements","site comorphism","internal language"],"falsifier":"Take a finite presheaf topos, for example presheaves on a two-object category, choose maps $f:P\\to Q$ and $h:H\\to P$, and compute both sides of Theorem 1.3 as finite sets: the construction is correct exactly when the hom-set bijection between arrows $f^*(k)\\to h$ and arrows $k\\to\\prod_f[h]$ holds for every $k:K\\to Q$. For the Grothendieck formula, compute $a_Q\\circ\\prod_f^{\\mathrm{pr}}\\circ i_P$ on a non-sheaf $P$ and compare with the pointwise compatible-family expression; a mismatch would trace back to the cited category-of-elements equivalence.","tokens_in":13241,"feed_emoji":"🧮","tokens_out":10427,"duration_ms":91240,"temperature":0.7,"pith_summary":"Dependent products are the right adjoints to pullback functors, and they give the category-theoretic meaning of quantified families in type theory. This paper establishes that in any elementary topos the dependent product $\\prod_f[h]$ along $f:P\\to Q$ can be identified with one explicitly built object, namely $\\forall_{f\\times 1}(S)\\cap T^f_1\\cap T^h_2$, where each piece is defined using only power objects and finite limits. The identification is a natural bijection of arrows, so it proves the universal property directly rather than through the standard detour into slice toposes or partial-arrow classifiers. For Grothendieck toposes, the paper transfers this to a site-level description $\\prod_{a(f)}=a_Q\\circ\\prod_f^{\\mathrm{pr}}\\circ i_P$, so the dependent product can be computed pointwise from compatible families indexed by morphisms out of a stage $X$.","feed_headline":"Dependent products in toposes get one explicit formula","feed_subtitle":"Built from power objects and finite limits, it also yields pointwise site-level formulas for Grothendieck toposes.","key_machinery":"The central object is the subobject formula $\\forall_{f\\times 1}(S)\\cap T^f_1\\cap T^h_2$, which packages the bounded internal-language description of dependent products as a geometric construction. The elementary machinery is the power-object calculus: $S$ is obtained as a pullback involving the singleton map $\\{\\cdot\\}_H$ and the classifying map of the membership subobject, and the universal-quantifier functor $\\forall$ is expressed in Proposition 1.4 as a pullback using the covariant power-object functor. The Grothendieck machinery is the category-of-elements presentation: a slice $\\mathrm{Sh}(\\mathcal{C},J)/a(P)$ is equivalent to $\\mathrm{Sh}(\\int P,J_P)$, and the arrow $f$ induces a comorphism of sites $\\int f$---a functor satisfying the covering-lifting property---whose direct image, a right Kan extension, becomes the dependent product.","core_discovery":"The central claim, Theorem 1.3, is that for any elementary topos $\\mathcal{E}$, any $f:P\\to Q$, and any object $h:H\\to P$ of $\\mathcal{E}/P$, the dependent product $\\prod_f[h]$ is isomorphic to $\\forall_{f\\times 1}(S)\\cap T^f_1\\cap T^h_2$. Here $S\\subseteq P\\times \\mathcal{P}(H\\times P)$ expresses that the variable $w$ is a functional graph over $H$, while $T^f_1$ and $T^h_2$ force $w$ to lie in the fibers of $f$ and on the graph of $h$. The isomorphism is witnessed by a natural bijection sending an arrow $f^*(k)\\to h$ in $\\mathcal{E}/P$ to the classifying arrow $k\\to \\forall_{f\\times 1}(S)\\cap T^f_1\\cap T^h_2$ in $\\mathcal{E}/Q$. For a Grothendieck topos, Corollary 2.4 computes the same construction as $a_Q\\circ\\prod_f^{\\mathrm{pr}}\\circ i_P$, and when $P,Q$ are sheaves the value at a stage $X$ is a set of compatible tuples indexed by arrows $g:Y\\to X$.","pith_inferences":["The boundedness strategy suggests that other type-theoretic constructors, such as W-types, quotient types, or general inductive schemas, might admit similarly explicit power-object and finite-limit presentations in arbitrary elementary toposes.","The stage-by-stage formula of Corollary 2.4 offers a practical route to computing dependent products in sheaf toposes: take limits over morphisms out of $X$, and let the topology enter only through sheafification.","The same site-comorphism analysis could be pushed further to describe not just the object $\\prod_f[h]$ but the whole functor $\\prod_f$ as a right adjoint between categories of sheaves, making preservation properties easier to read off."],"forward_implications":["Dependent products along any morphism $f:P\\to Q$ can be computed in one step from power objects and finite limits, without first replacing the problem by a slice topos or invoking partial-arrow classifiers.","In a Grothendieck topos, the dependent product reduces to the presheaf dependent product followed by sheafification, so explicit site computations are available.","If $P$ and $Q$ are sheaves, the Grothendieck topology does not affect the pointwise formula: the value at a stage $X$ is a set of compatible families indexed by morphisms out of $X$.","The construction is compatible with subtoposes: for a morphism inside a subtopos, the dependent product computed in the ambient topos restricts to the dependent product computed in the subtopos.","The internal-language reading gives a type-theoretic interpretation: dependent products are defined by bounded quantification over power objects, matching the syntactic $\\prod_{p\\in P}h^{-1}(p)$ description."],"supporting_citations":[{"why":"supplies the elementary power-object and covariant power-object machinery used to express the universal-quantifier functor in Proposition 1.4.","marker":"[7]"},{"why":"provides the slice power-object formula, the category-of-elements presentation, and the Set-level description of dependent products on which the construction is modeled.","marker":"[10]"},{"why":"is the companion preprint from which Proposition 2.1, the equivalence $\\mathrm{Sh}(\\mathcal{C},J)/a(P)\\simeq\\mathrm{Sh}(\\int P,J_P)$, is cited; this equivalence is the bridge to Grothendieck toposes.","marker":"[6]"},{"why":"supplies the internal-language and local-set-theory framework in which the bounded formulas leading to Theorem 1.3 are first expressed.","marker":"[4]"}],"fun_headline_variants":["Explicit dependent product formula for every elementary topos","Dependent products via power objects and finite limits","Site-level dependent products for Grothendieck toposes","One formula unifies dependent products across toposes"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"For the site-level half of the paper, the load-bearing premise is the cited equivalence between a slice of a sheaf topos and sheaves on the category of elements with the induced topology; if that equivalence is wrong, the explicit pointwise formula for the dependent product does not follow.","fun_headline_variants_meta":{"raw":{"variants":["Explicit dependent product formula for every elementary topos","Dependent products via power objects and finite limits","Site-level dependent products for Grothendieck toposes","One formula unifies dependent products across toposes"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000428,"raw_usage":{"total_tokens":2125,"prompt_tokens":819,"completion_tokens":1306,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":435,"completion_tokens_details":{"reasoning_tokens":1244}},"tokens_in":435,"tokens_out":1306,"duration_ms":10077,"temperature":1.0,"reasoning_tokens":1244,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T11:39:14.414290+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a finite presheaf topos, for example presheaves on a two-object category, choose maps $f:P\\to Q$ and $h:H\\to P$, and compute both sides of Theorem 1.3 as finite sets: the construction is correct exactly when the hom-set bijection between arrows $f^*(k)\\to h$ and arrows $k\\to\\prod_f[h]$ holds for every $k:K\\to Q$. For the Grothendieck formula, compute $a_Q\\circ\\prod_f^{\\mathrm{pr}}\\circ i_P$ on a non-sheaf $P$ and compare with the pointwise compatible-family expression; a mismatch would trace back to the cited category-of-elements equivalence.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"supplies the elementary power-object and covariant power-object machinery used to express the universal-quantifier functor in Proposition 1.4."},{"cited_title":"Mac Lane and I","cited_arxiv_id":null,"evidence_quote":"provides the slice power-object formula, the category-of-elements presentation, and the Set-level description of dependent products on which the construction is modeled."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"supplies the internal-language and local-set-theory framework in which the bounded formulas leading to Theorem 1.3 are first expressed."}],"review_version":1}