{"id":"a99ac962-3885-403c-ab61-c9ae6ed0a3be","arxiv_id":"2411.19239","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The authors show that the predicative effective topos pEff carries a fibred structure of 'sets', whose fibres are locally cartesian closed list-arithmetic pretoposes with a small subobject classifier and formal Church's thesis.","lead":"This paper shows how to organize the 'sets' inside a predicative version of Hyland's effective topos into a fibred topos, with good categorical properties in every fibre. The result gives a constructive and predicative model that could interpret the Minimalist Foundation with inductive and coinductive predicates and formal Church's thesis.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 7.1's proof invokes a small map [g]:R'→R in Propr_s(A×A) although R,R' are arbitrary realized propositions; the base-change construction is therefore unproved as written, though likely repairable via the realizer R'→Colr_{p×p}(R).","rationale":"Read in good faith, the paper's goal is to equip pEff with a fibred structure of small families. The constructions in Sections 3-5 are detailed and largely inherited from [MM21]; the comparison with van den Berg-Moerdijk is reasonable, and the embedding into discrete objects is a useful and plausible contextualization. The principal soft spot is exactly the base-change stability of the small family fibration, Lemma 7.1. The reader's weakest assumption identifies the same lemma. My check confirms the proof as written is defective: it places a realizer between R' and R in Propr_s, but those relations are not small in general. However, I do not see a reason the lemma is false; a corrected construction using the actual realizer e into Colr_{p×p}(R) appears to go through, so the verdict should remain conditional pending repair rather than rejection. The explicit 'leave to the reader' in Proposition 6.8 and the countable-choice caveat in Remark 6.9 are additional incompletenesses but less central than Lemma 7.1.","tokens_in":23313,"tokens_out":11267,"duration_ms":98966,"concrete_test":"Re-prove Lemma 7.1 using the realizer e:R'->Colr_{p×p}(R) instead of [g]∈Propr_s(A×A). Explicitly define B'=Setr_p(B), S'=(Propr_s)_{Σ(p,B×B)}([S]), and σ'(a',b',r')=σ(p(a'),p(b'),e(a',b',r'),b'); then check the three axioms of Definition 6.2 and that K(B',S',σ') is isomorphic to the pullback [p]^*K(B,[S],σ). Success confirms the fibration is well-defined; failure shows Lemma 7.1 is false.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Lemma 7.1 is the only result guaranteeing that the base-change operation used to define the fibration pEff_set lands in the fibre of extensional dependent sets; Theorem 8.5 therefore depends on it. The proof chooses a representative [g]:R'→R in Propr_s(A×A), recalling that Propr_s(A×A) is the poset reflection of Setr(A×A). But R and R' are arbitrary objects of Propr(A×A), not necessarily small, so such a [g] need not exist. What an arrow [p]:(A',[R'])->(A,[R]) does give is a realizer e:R'->Colr_{p×p}(R) in Colr(A'×A') witnessing [R'] ≤ Propr_{p×p}([R]); this is not a small map into R. Without an argument showing how to build the transported action from e (or some other data), Lemma 7.1 does not prove stability of small families under pullback, and pEff_set is not known to be a well-defined fibration. The flaw appears repairable: one can define σ' using e and the original σ, and use condition 4 of Definition 6.2 to handle different realizers. But as written, the central fibred structure is unproved.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper continues the authors' earlier work [MM21] on the predicative effective topos pEff, a predicative and constructive variant of Hyland's Effective Topos. The paper defines, for each object (A,[R]) of pEff, categories DeppEff(A,R) and DeppEff_set(A,R) of extensional dependent collections and sets, and constructs a functor K from these to the slice category pEff/(A,[R]). The main structural claim, Theorem 8.5, is that pEff carries two fibrations, pEff_set and the codomain fibration, whose fibres are locally cartesian closed list-arithmetic pretoposes, that there is a small-subobject classifier Omega, and that formal Church's thesis holds, so that pEff is 'a fibred predicative variant of Hyland's Effective Topos'. The paper also sketches, in Section 9, how this structure could support a direct interpretation of the extensional level emTT of the Minimalist Foundation, and compares the base category pEff with van den Berg--Moerdijk's predicative realizability categories in Section 10.","tokens_in":23557,"tokens_out":5457,"duration_ms":44841,"significance":"If Theorem 8.5 is correct, the paper delivers a substantial result: the full subcategory of discrete objects of Hyland's Effective Topos contains a fibred predicative topos that validates formal Church's thesis in a constructive metatheory. This is a natural next step after [MM21] and connects the fibrational approach to the Minimalist Foundation with realizability semantics. The paper is constructive and predicative throughout, building on Feferman's ID_1 and extensions of CZF. The authors are explicit about relying on prior published work for the basic definitions of pEff, which is a normal dependency. The main weakness is that the construction of the central fibration contains a proof gap: Lemma 7.1, which is required to ensure that pullback preserves small families, is not proved as written. The issue appears repairable, but until a correct proof is supplied, the well-definedness of pEff_set and hence Theorem 8.5 are not established.","major_comments":[{"comment":"The proof of Lemma 7.1 selects a representative [g]:R'→R in Propr_s(A×A), but R and R' are arbitrary objects of Propr(A×A), not necessarily small. An arrow [p]:(A',R')→(A,R) does not give a small map R'→R; it gives a realizer e:R'→Colr_{p×p}(R) witnessing the inequality R' ≤ Propr_{p×p}(R). Consequently the pullback of a small family along [p] is not shown to land in DeppEff_set(A,R'). Since Lemma 7.1 is the only result in the paper that guarantees that the base-change operation defining pEff_set preserves the fibre of extensional dependent sets, the well-definedness of the fibration and all parts of Theorem 8.5 that use it (items 2--6) are not established as written. Please supply a direct construction of the transported action from the realizer e, verifying condition 4 of Definition 6.2, or provide an alternative proof of smallness of the pullback.","section":"Lemma 7.1"},{"comment":"The proof of essential surjectivity of K is incomplete: after defining B_f and [S]_f, the authors state 'Finally, we can define σ_f ... We leave this to the reader.' This is a load-bearing omission because the verification that σ_f satisfies the three conditions of Definition 6.2 is needed to conclude that (B_f,[S]_f,σ_f) is an object of DeppEff(A,R). Without this, K is not known to be essentially surjective. Remark 6.9 itself points out that the categorical consequences depend on whether one has an equivalence or merely preservation/reflection of limits. Please include the full definition of σ_f and the verification of conditions 1--3.","section":"Proposition 6.8"},{"comment":"The proof of Theorem 7.5 contains two 'one can check' assertions that are load-bearing. For stable finite coproducts, the text says 'One can check that these injections are mono, and that coproducts are stable under pullbacks using pullbacks constructed through the finite limits of DeppEff(A,R) and DeppEff_set(A,R) described above'; the stability under pullback is not shown. For exactness, the proof says that 'Stability and effectiveness follow from the pullback property in Lemma 7.1', but Lemma 7.1 is exactly the result whose proof is defective (see Major Comment 1), and the stability of the constructed coequalizer under pullback is not demonstrated. Since items 2 and 4 of Theorem 8.5 assert that the fibres are list-arithmetic pretoposes, these details are part of the central claim. Please provide full proofs of coproduct stability and of exactness, explicitly using a corrected Lemma 7.1.","section":"Theorem 7.5"}],"minor_comments":[{"comment":"In Proposition 6.8, the notation tσ, dR and the arrows in the commutative diagram are not defined in the text; please define all arrows appearing in the diagram or refer to a specific equation.","section":"Section 6, page 13"},{"comment":"In the first paragraph of Section 7, 'loose their functoriality' should be 'lose their functoriality'.","section":"Section 7, 'loose'"},{"comment":"The statement 'Given an element (B,[S],σ) ∈ DeppEff (A, [R])' should read 'DeppEff(A,R)', since the category is indexed by a representative R, not an equivalence class [R].","section":"Lemma 8.2"},{"comment":"The displayed condition defining pEff_props(A,[R]) is 'Propr_{p1}([P]) ∧ [R] ≤ Propr_{p2}([P])'; it may be clearer to state explicitly that [P] is an object of Propr(A) satisfying this invariance condition with respect to [R].","section":"Section 8, equation (10)"},{"comment":"The diagram involving 'Cr /d31 /d127 i' is corrupted in the arXiv rendering; please redraw it so that the embedding of Cr and pEff into the corresponding assembly categories is readable.","section":"Section 10, diagram"},{"comment":"The sentence 'Since Cr is a full subcategory of recursive objects and pEff is the ex/lex completion of Cr we have an embedding of pEff in Disc_E[T] that extends to fibers, trivially' is too quick; please spell out how the embedding extends to the fibrations, or mark this as future work.","section":"Section 10, final paragraph"}],"recommendation":"major_revision","confidential_remarks":"The gap in Lemma 7.1 appears repairable: one can define the transported action using the realizer e and the original σ, and then verify condition 4 of Definition 6.2. However, as written the central fibration pEff_set is not proved to be well-defined, and Theorem 8.5 depends on it. The paper also leaves several verification steps to the reader in Proposition 6.8 and Theorem 7.5. I recommend major revision with a request for full proofs of these points. The topic and results are significant for the intended readership."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know this paper is the real thing in intent: it claims to equip the predicative effective topos pEff of Maietti-Maschio with a fibred structure of sets, giving a fibred predicative topos validating Church's thesis in a constructive metatheory. If the main theorem holds, it is the first categorical model of the full Minimalist Foundation extended with (co)inductive predicates, a goal the authors have been chasing since [MM21]. The constructions are genuinely new: extensional dependent collections and sets over pEff, a subfibration of the codomain fibration, and a small-subobject classifier. None of this appears in [MM21] or [BM11]. The paper is careful about the metatheory, working predicatively in ID1 or CZF+REA+RDC, and the comparison with van den Berg-Moerdijk is reasonable.\n\nThe soft spots are real but not fatal. The proof of Lemma 7.1, which is load-bearing for the fibration, picks a representative [g]:R'->R in Propr_s(AxA) although R and R' are arbitrary realized propositions. The stress-test note is right: an arrow [p] gives a realizer e:R'->Colr_{p x p}(R), not a small map, so the transported action is not constructed as written. This can likely be repaired using e and the original sigma, but as it stands pEff_set is not shown to be a fibration. Similarly, Proposition 6.8 leaves the construction of sigma_f to the reader, and Theorem 7.5 has several 'one can check' steps in the stability arguments. These are presentation gaps rather than contradictions; the overall strategy looks sound and the pieces fit together.\n\nThe citation pattern is normal: they build on their own prior work and on [BM11], but not circularly. No invented entities or free parameters. I disagree with any suggestion that the central claim is fitted or assumed; it is derived, with identifiable repair points.\n\nWho is this for? People working on categorical models of predicative type theory, realizability, and the Minimalist Foundation. A serious referee should get this paper; it deserves referee time, but the referee should demand a complete proof of Lemma 7.1 and a fleshed-out Proposition 6.8 before acceptance. I would bring it to a reading group if the group tolerates work-in-progress.","headline":"A serious fibred predicative topos construction with a real but repairable gap in the base-change lemma; worth refereeing.","tokens_in":24141,"tokens_out":1858,"would_cite":true,"duration_ms":15706,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03G30","03F50"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper establishes that the predicative effective topos pEff carries two fibrations whose fibres are locally cartesian closed list-arithmetic pretoposes, a small-subobjects classifier Ω, and formal Church's thesis, making it a fibred…","keywords":["predicative topos","effective topos","fibration of sets","realizability","formal Church's thesis","elementary quotient completion","Minimalist Foundation","constructive set theory"],"falsifier":"Find an arrow $[p]:(A',[R'])\\to(A,[R])$ in $\\mathbf{pEff}$ and an extensional dependent set $(B,[S],\\sigma)$ over $(A,[R])$ such that the pullback $[p]^*K(B,[S],\\sigma)$ is not isomorphic to $K$ of any extensional dependent set over $(A',[R'])$. Concretely, try to construct $R'$ as a realized proposition not representable by a small proposition in $\\mathbf{Prop}_r^s(A'\\times A')$ while $R$ is small, and check whether the chosen representative $[g]:R'\\to R$ can exist in $\\mathbf{Prop}_r^s(A\\times A)$. If no such $[g]$ can be supplied in general, the proof of Lemma 7.1 fails and the fibration is not well-defined.","tokens_in":23076,"feed_emoji":"","tokens_out":10343,"duration_ms":81663,"temperature":0.7,"pith_summary":"This paper sets out to show that the predicative effective topos $\\mathbf{pEff}$, previously built inside the classical predicative theory of non-iterative fixpoints $\\widehat{ID_1}$, carries a full fibred structure of sets. Its central result is that $\\mathbf{pEff}$ is equipped with two fibrations, one for collections and one for sets, whose fibres are locally cartesian closed list-arithmetic pretoposes, together with a small-subobjects classifier and the formal Church's thesis. If this result is right, the full subcategory of discrete objects inside Hyland's Effective Topos already contains a fibred predicative topos, even when both are formalized in a constructive metatheory. The structure is aimed at modelling both levels of the Minimalist Foundation, so that $\\mathbf{pEff}$ would serve as a computational realizability model for a constructive and predicative foundation extended with inductive and coinductive predicates.","feed_headline":"Discrete objects of the effective topos contain a full fibred topos","feed_subtitle":"The fibres are locally cartesian closed pretoposes with a small-subobject classifier; formal Church's thesis holds throughout.","key_machinery":"The load-bearing object is the subfibration $\\mathbf{pEff}_{\\mathrm{set}} \\to \\mathbf{pEff}$ of the codomain fibration, which sends each object to its slice category and is here presented via extensional dependent sets $(B,[S],\\sigma)$. Here $B$ is a realized family of sets over a base $A$, $[S]$ is a small fibred equivalence relation on $B$, and $\\sigma$ moves elements of $B(a)$ to $B(a')$ along realizers of the equivalence relation $R$ on $A$, respecting identity and composition; the functor $K$ sends such a triple to an arrow $(\\Sigma(A,B), \\exists_{d_R}(\\mathrm{Prop}_r^{t_\\sigma}([S]))) \\to (A,[R])$ in $\\mathbf{pEff}$. Smallness of $B$ and $[S]$ is what separates the set-fibration from the collection-fibration, and Proposition 8.3 identifies small subobjects with the small-proposition doctrine, so Theorem 8.4 can supply the classifier $\\Omega$. Around this, the proofs use the presentation of $\\mathbf{pEff}$ as the exact completion of $\\mathbf{Cr}$ and descent theory for internal groupoids.","core_discovery":"The paper's central claim is that the indexed structure of realized sets and small propositions on the category $\\mathbf{Cr}$ lifts to a subfibration of the codomain fibration on $\\mathbf{pEff}$. For each object $(A,[R])$ it forms the category of extensional dependent collections: a realized family $B$ over $A$, a fibred equivalence relation $[S]$ on $B$, and a transport action $\\sigma$ along realizers of $R$ satisfying identity and composition laws; a subset of these, where $B$ is a realized set family and $[S]$ is small, gives the extensional dependent sets. The functor $K$ embeds these categories into the slice $\\mathbf{pEff}/(A,[R])$, and the paper proves that the set-fibres are locally cartesian closed list-arithmetic pretoposes whose structure is preserved by pullback along every arrow of $\\mathbf{pEff}$. It then shows that small subobjects are classified by an object $\\Omega$ and that formal Church's thesis holds, concluding that $\\mathbf{pEff}$ is a fibred predicative variant of Hyland's Effective Topos and that the discrete objects of $\\mathbf{Eff}$ already contain such a structure in a constructive metatheory.","pith_inferences":["Editorial inference: The construction gives a concrete template for a general notion of fibred predicative topos and a predicative tripos-to-topos construction, the two notions the paper names as future goals.","Editorial inference: A full fibred comparison with the predicative realizability categories of algebraic set theory, which the paper leaves to future work, would show whether the set-fibration here coincides with the small-map fibration on the common subcategory.","Editorial inference: A proof-assistant formalization of Lemma 7.1 would test the base-change smallness step directly and would make the constructive metatheory explicit enough to extract programs from the interpretation.","Editorial inference: If the interpretation of the extensional level goes through, one would expect $\\mathbf{pEff}$ to yield a computational model for the classical version of the Minimalist Foundation via the equiconsistency result cited in the paper."],"forward_implications":["If Theorem 8.5 is correct, the discrete objects of Hyland's Effective Topos contain a fibred predicative topos that validates formal Church's thesis, formalized in a constructive metatheory.","For every base object $(A,[R])$, the fibre over it is a locally cartesian closed list-arithmetic pretopos, so the sets over any fixed base form a full categorical universe.","Pullback along any arrow of $\\mathbf{pEff}$ preserves the locally cartesian closed list-arithmetic pretopos structure, so substitution in the dependent type theory is interpreted by structure-preserving functors.","The object $\\Omega$ classifies small subobjects in $\\mathbf{pEff}$, giving a predicative analogue of the subobject classifier of an ordinary topos.","The fibred structure is designed to interpret the extensional level of the Minimalist Foundation, with inductive and coinductive predicates, inside $\\mathbf{pEff}$."],"supporting_citations":[{"why":"Builds the base category pEff as the elementary quotient completion of Propr and supplies the theorems that pEff is a locally cartesian closed list-arithmetic pretopos with formal Church's thesis, on which the fibred structure is erected.","marker":"[MM21]"},{"why":"Defines the classical predicative metatheory of non-iterative fixpoints in which the realized collections are formalized.","marker":"[Fef82]"},{"why":"Supplies CZF and its extensions used as constructive and predicative metatheories for carrying out the structural analysis.","marker":"[AR01]"},{"why":"Provides the realizability interpretation of the intensional level of the Minimalist Foundation and the encoding of the universe of sets used to define families of realized sets.","marker":"[IMMS18]"},{"why":"Supplies the elementary quotient completion and the monomorphism characterization used in Lemma 7.3 and in the exact-completion presentation of pEff.","marker":"[MR13b]"},{"why":"Provides the descent theory for internal groupoids used in Proposition 6.11 to connect extensional dependent collections with descent data.","marker":"[JT94]"},{"why":"Gives the comparison target, a predicative realizability category from algebraic set theory, into which pEff with small equivalence relations embeds.","marker":"[BM11]"},{"why":"Identifies the discrete objects of the effective topos as the exact completion of recursive objects, locating the ambient category where the fibred predicative topos lives.","marker":"[HRR90]"},{"why":"Shows how the CZF extensions with REA and RDC support inductive and coinductive topological generation, used for the constructive version of the metatheory.","marker":"[MMR22]"}],"fun_headline_variants":["Discrete objects of Eff hide a fibred predicative topos","Predicative fibred topos emerges from Eff's discrete objects","Church's thesis holds within a fibred topos in Eff","Eff's discrete objects yield a fibred topos constructively","Fibred topos with Church's thesis found in Eff's discrete part"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole fibred structure depends on Lemma 7.1: pulling back a small family over $(A,[R])$ along any arrow $(A',[R'])\\to(A,[R])$ must again be a small family. The proof needs a representative $[g]:R'\\to R$ that is itself a small realized proposition, while $R'$ and $R$ are only arbitrary realized propositions; if that small representative cannot always be found, the set-fibration is not known to exist and Theorem 8.5 does not follow.","fun_headline_variants_meta":{"raw":{"variants":["Discrete objects of Eff hide a fibred predicative topos","Predicative fibred topos emerges from Eff's discrete objects","Church's thesis holds within a fibred topos in Eff","Eff's discrete objects yield a fibred topos constructively","Fibred topos with Church's thesis found in Eff's discrete part"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000738,"raw_usage":{"total_tokens":3283,"prompt_tokens":920,"completion_tokens":2363,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":536,"completion_tokens_details":{"reasoning_tokens":2273}},"tokens_in":536,"tokens_out":2363,"duration_ms":14700,"temperature":1.0,"reasoning_tokens":2273,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T10:22:35.200187+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Find an arrow $[p]:(A',[R'])\\to(A,[R])$ in $\\mathbf{pEff}$ and an extensional dependent set $(B,[S],\\sigma)$ over $(A,[R])$ such that the pullback $[p]^*K(B,[S],\\sigma)$ is not isomorphic to $K$ of any extensional dependent set over $(A',[R'])$. Concretely, try to construct $R'$ as a realized proposition not representable by a small proposition in $\\mathbf{Prop}_r^s(A'\\times A')$ while $R$ is small, and check whether the chosen representative $[g]:R'\\to R$ can exist in $\\mathbf{Prop}_r^s(A\\times A)$. If no such $[g]$ can be supplied in general, the proof of Lemma 7.1 fails and the fibration is not well-defined.","supporting_citations":[],"review_version":1}