On the dependent product in toposes

Olivia Caramello; Riccardo Zanfa

REVIEW 2 major objections 6 minor 11 references

On the dependent product in toposes

T0 review · 2 major / 6 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The dependent product in any elementary topos admits an explicit construction from power objects and finite limits.

desk verdict A genuinely useful elementary formula for dependent products, with a Grothendieck section that hinges on an unproved equivalence from the authors' companion preprint. read the letter →

arxiv 1908.08488 v1 pith:4XTVJGVD submitted 2019-08-22 math.CT

Olivia Caramello , Riccardo Zanfa This is my paper · ORCID

classification math.CT MSC 18B2518F1003G30

keywords dependentproductelementarytoposGrothendieckpowerobjectsslicecategoryofelementssitecomorphisminternallanguage

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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$.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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$.

Load-bearing premise

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.

Editorial extensions

If this is right

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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

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.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the 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.

The 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.

Also 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.

Who'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.

Referee Report

2 major / 6 minor

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).

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 (2)

[Section 2, Proposition 2.1] 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 1, Theorem 1.3] 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.

minor comments (6)

[Abstract, p. 2] There are typographical errors in the abstract: 'i n' and 'constructi on' should be corrected to 'in' and 'construction'.
[Notation, p. 3] 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.
[Lemma 1.2, proof] 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.
[Proposition 2.1] 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).
[Corollary 2.4] 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.
[Reference [6]] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the elementary construction is self-contained, and the Grothendieck section's reliance on the cited site-equivalence [6] is a dependency, not a circular reduction.

full rationale

The paper's Section 1 does not assume the existence of dependent products. Theorem 1.3 constructs an object ∀_{f×1}(S)∩T^f_1∩T^h_2 from power objects and finite limits and proves, via Lemma 1.2's bijection between graphs and classifying arrows, that it has the universal property of the right adjoint to f^*. The ∀-functor is later shown in Proposition 1.4 to be definable by a pullback using power objects, so the construction is elementary. The only external input is Proposition 2.1, the equivalence Sh(C,J)/a(P) ≃ Sh(∫P,J_P), whose proof is cited from the authors' companion preprint [6]. This is a self-citation and an omitted proof in the present paper, and the site-theoretic description of Section 2 is therefore not fully self-contained. However, it is not a circular step: the cited equivalence is a general site/slice equivalence stated for arbitrary presheaves and sites, and its assumptions do not include the existence or formula for dependent products. Corollary 2.4 reduces the sheaf dependent product to the presheaf right Kan extension, not to the theorem being proved. No fitted parameters, ansatz-cited constructions, or self-imported uniqueness theorems occur. The construction is checkable in the topos Set, giving independent content.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The central construction relies on standard topos-theoretic assumptions. The main external input is Proposition 2.1 from the authors' companion preprint. No free parameters or invented entities appear.

assumptions (3)

domain assumption The internal language of an elementary topos is sound and supports functional completeness (elementwise definition of arrows).
Invoked in Proposition 1.1 to transfer the set-theoretic construction to any topos; standard metatheorem, not proved in the paper.
standard math Power objects and finite limits define the universal-image functor ∀ via the pullback in Proposition 1.4.
Proposition 1.4 is proved in the text using the internal language and standard properties of power objects.
domain assumption The slice of a Grothendieck topos Sh(C,J)/a(P) is equivalent to Sh(∫P,J_P), the topos of sheaves on the category of elements.
Proposition 2.1, with proof deferred to the authors' companion preprint [6]; this equivalence is central to Section 2.

how reviews work

0 comments

Cite this review

Pith. "Pith review of On the dependent product in toposes." pith.science (2026). https://pith.science/paper/4XTVJGVD

@misc{pith2026190808488,
  author       = {Pith},
  title        = {Pith review of: On the dependent product in toposes},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4XTVJGVD}},
  note         = {Machine review of arXiv:1908.08488}
}

read the original abstract

We give an explicit construction of the dependent product in an elementary topos, and a site-theoretic description for it in the case of a Grothendieck topos.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

11 extracted references · 10 canonical work pages

[6]

Caramello, Denseness conditions, morphisms and equi valences of toposes, preprint available as arxiv:math.CT/1906.08737v2, 68 pages (2019)

O. Caramello, Denseness conditions, morphisms and equi valences of toposes, preprint available as arxiv:math.CT/1906.08737v2, 68 pages (2019). 17

arXiv 2019
[1]

Dependent product in nLab (revision 51 - July 2019), http://ncatlab.org/nlab/revision/dependent%20product/51

work page 2019
[2]

Artin, A

M. Artin, A. Grothendieck and J. L. Verdier, Théorie des topos et co- homologie étale des schémas - (SGA 4), Séminaire de Géométrie Al- gébrique du Bois-Marie, année 1963-64; second edition publi shed as Lecture Notes in Math., vols 269, 270 and 305, Springer-Verl ag (1972)

work page 1972
[3]

Barr and C

M. Barr and C. Wells, Toposes, triples and theories , corrected reprint of the 1985 original, Reprints in Theory and Applications of Categories 12, x+288 (2005)

work page 2005
[4]

J. L. Bell, Toposes and Local Set Theories , vol. 14 of Oxford Logic Guides, Oxford University Press (1988)

work page 1988
[5]

Borceux, Handbook of categorical algebra , vol

F. Borceux, Handbook of categorical algebra , vol. 3, Cambridge Univer- sity Press (1994)

work page 1994
[7]

P. T. Johnstone, Sketches of an Elephant: a topos theory compendium. Vols. 1 and 2 , vols. 43 and 44 of Oxford Logic Guides, Oxford University Press (2002)

work page 2002
[8]

P. T. Johnstone, Topos theory, Academic Press (1977)

work page 1977

Show all 11 references

[9]

Goldblatt, Topoi: the categorial analysis of logic , Studies in Logic and the Foundations of Mathematics vol

R. Goldblatt, Topoi: the categorial analysis of logic , Studies in Logic and the Foundations of Mathematics vol. 98, North-Holland P ublishing Co., Amsterdam-New York (1979)

1979
[10]

Mac Lane and I

S. Mac Lane and I. Moerdijk, Sheaves in geometry and logic: a ﬁrst introduction to topos theory , Springer-Verlag (1992)

1992
[11]

McLarty, Elementary categories, elementary toposes , vol

C. McLarty, Elementary categories, elementary toposes , vol. 21 of Ox- ford Logic Guides , Oxford University Press (1992). Olivia Caramello and Riccardo Zanf a Dipartimento di Scienza e Alta Tecnologia, Università degli Studi dell’Insubria, via V alleggio 11, 22100 Como, Italy...

1992

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [6]

Caramello, Denseness conditions, morphisms and equi valences of toposes, preprint available as arxiv:math.CT/1906.08737v2, 68 pages (2019)

O. Caramello, Denseness conditions, morphisms and equi valences of toposes, preprint available as arxiv:math.CT/1906.08737v2, 68 pages (2019). 17

arXiv 2019

[2] [1]

Dependent product in nLab (revision 51 - July 2019), http://ncatlab.org/nlab/revision/dependent%20product/51

work page 2019

[3] [2]

Artin, A

M. Artin, A. Grothendieck and J. L. Verdier, Théorie des topos et co- homologie étale des schémas - (SGA 4), Séminaire de Géométrie Al- gébrique du Bois-Marie, année 1963-64; second edition publi shed as Lecture Notes in Math., vols 269, 270 and 305, Springer-Verl ag (1972)

work page 1972

[4] [3]

Barr and C

M. Barr and C. Wells, Toposes, triples and theories , corrected reprint of the 1985 original, Reprints in Theory and Applications of Categories 12, x+288 (2005)

work page 2005

[5] [4]

J. L. Bell, Toposes and Local Set Theories , vol. 14 of Oxford Logic Guides, Oxford University Press (1988)

work page 1988

[6] [5]

Borceux, Handbook of categorical algebra , vol

F. Borceux, Handbook of categorical algebra , vol. 3, Cambridge Univer- sity Press (1994)

work page 1994

[7] [7]

P. T. Johnstone, Sketches of an Elephant: a topos theory compendium. Vols. 1 and 2 , vols. 43 and 44 of Oxford Logic Guides, Oxford University Press (2002)

work page 2002

[8] [8]

P. T. Johnstone, Topos theory, Academic Press (1977)

work page 1977