{"id":"92314870-8d1a-40fc-b510-1846a9428ddc","arxiv_id":"2607.23671","paper_version":2,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":6.5,"correctness_risk":"low","formal_verification":"full","parameter_count":0,"one_line_summary":"Displayed setoids in IRU give a sound semantics for ETU and a machine-checked proof of ETU consistency inside safe Agda.","lead":"A simplified notion of displayed setoid in intensional type theory is shown to interpret extensional type theory with universes, fully formalized in safe Agda. The construction yields a machine-checked relative consistency proof of extensional type theory inside intensional type theory with induction-recursion.","discovery_kind":"extension","skeptic_critique":{"model":"moonshotai/kimi-k3","headline":"No internal gap found. The remaining load-bearing exposure is the unmechanized assurance that the checked Agda artifact actually stays within the intended IRU fragment.","rationale":"The reader’s weakest-assumption entry identifies the same exposure: safe Agda is only a hand-restricted stand-in for IRU, and the final consistency statement is relative to that meta-theory. I found no more internal weakness in the displayed-setoid definitions, semantic relations, totality/single-valuedness argument, or the short derivation of Theorem 6.8. The extensive Agda formalization is substantial independent support for the construction. The proposed audit is worthwhile because the relevant exclusion is not enforced by the compiler flags alone, but absent a concrete artifact violation it does not warrant moving the verdict to CONDITIONAL. The unproved consistency of IRU limits the foundational interpretation of the corollary, yet the paper states its claim in precisely that relative form, so the ACCEPT verdict remains appropriate.","tokens_in":31438,"tokens_out":6269,"duration_ms":157746,"concrete_test":"From a clean checkout, build the artifact with Agda 2.8.0 under global --safe --without-K. Compute the transitive import cone of Semantics.Consistency and AST-lint it for coinductive declarations, Prop/SProp or irrelevance annotations, and OPTIONS pragmas relaxing the flags; also re-check a closed goal ascribing consisETU the exact type ¬(Σ[a ∈ Tm] (⋄ ⊢ a :₀ Emp)). A forbidden construct or failed ascription would substantiate the concern; a clean result would settle this fragment-compliance issue.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Theorem 6.8 is explicitly relative to IRU, and the semantic route to it is coherent as presented. The soft spot is the identification of the compiled artifact with IRU. As the paper notes, Agda’s --safe option still permits coinductive types and proof-irrelevance annotations, while those are excluded only “by hand”; --safe --without-K therefore does not itself carve out the advertised fragment. If any transitive dependency of Semantics.Consistency used such a feature, or an OPTIONS pragma weakened the stated flags, the result would remain an Agda theorem but not necessarily the claimed theorem within IRU. The broader assumption that this inductive-recursive fragment is consistent is also external, but that is the stated relative-consistency form of the result rather than an internal inconsistency. There is no textual evidence that forbidden features were used.","agreement_with_reader":"agree"},"referee_report":{"model":"moonshotai/kimi-k3","summary":"The paper constructs, inside intensional type theory with a universe closed under inductive-recursive definitions (IRU, realized as Agda with --safe --without-K), a setoid-based model of extensional type theory with a countable hierarchy of universes (ETU). The syntax of ETU is given extrinsically using a well-scoped locally nameless representation. The semantics uses a simplified notion of displayed setoid (Definition 3.2): a type-valued heterogeneous equivalence relation over a base equivalence, with cartesian rather than path-over products in comprehension, plus coe/coh operations. Inductive-recursive definitions supply setoid universes of codes for types (§4.1–4.2) and a novel setoid universe of codes for contexts (§4.3). Because IRU cannot express partial functions directly, the semantics is given via type-valued input-output relations, proved single-valued (Theorem 6.5) and total and sound for definitional equality (Theorem 6.7), from which proof-irrelevant semantic functions are extracted (§6.5). As a corollary, consistency of ETU is proved within IRU (Theorem 6.8). The entire development is machine-checked in Agda 2.8.0 and publicly available.","tokens_in":31696,"tokens_out":4357,"duration_ms":91345,"significance":"If the development checks as claimed — and the paper ships the complete machine-checked artifact (Pitts 2026a), which is a major strength — this closes a real gap: Palmgren (2022) gave setoid closure constructions but not the semantic functions or the soundness proof. The paper delivers a fully formalized Streicher-style semantics with the hard parts (single-valuedness of proof-relevant relations, totality, soundness for definitional equality) actually carried out in a bare-bones intensional meta-theory, plus a machine-checked relative consistency corollary. The simplified displayed setoid (Definition 3.2, replacing path-over products with cartesian products plus coe/coh) and the setoid universe of context codes (§4.3) appear to be genuinely new and reusable. The foundational point — that extensionality can be modelled inside a very weak intensional system — is of clear interest to the type-theory and formalized-metatheory communities, independent of applications.","major_comments":[{"comment":"The main corollary is stated as 'a proof within IRU of the consistency of ETU' (also Theorem 6.8 and the abstract). IRU is defined as Safe Agda with --without-K, plus a manual exclusion of coinductive types and proof-irrelevance annotations, which --safe itself permits (footnote 1). The internal mathematics is fully machine-checked, but the identification of the checked artifact with the advertised fragment IRU currently rests on an unmechanized, by-hand assurance. There is no textual evidence that forbidden features are used, and the fix is small: please (a) state explicitly that Semantics.Consistency and its transitive dependency closure contain no coinductive records, no Prop/@irrelevant annotations, and no module-level OPTIONS pragmas weakening --safe/--without-K, and ideally (b) ship a small script in the artifact that checks this mechanically. This is the only point touching the * ","section":null}],"minor_comments":[{"comment":"Terminology: the title and most of the text use 'intensional', but the abstract and several passages (e.g., p. 2, 'intentional type theory is logically quite weak') use 'intentional'. If the latter is a deliberate echo of Martin-Löf, please say so once; otherwise unify.","section":"Abstract/§1"},{"comment":"The type of coh is printed as (y : ∥B∥), but ∥B∥ : |A| → Set, so this is ill-formed as printed; it should be (y : ∥B∥ x). The Agda code presumably has the correct type.","section":"Definition 3.2, Eq. (15)"},{"comment":"Clauses (59) and (60) are copied from §4.1 without updating subscripts: they read Eq0 ... ∼0 and Pi+ ... ∼0, but should be Eq+ ... ∼+ and Pi+ ... ∼+. Similarly clause (43) omits the subscript on ≈0, and the html anchor 'SucessorUniverse' is misspelled.","section":"§4.2, Eqs. (59)–(60)"},{"comment":"The Agda-style universe rule for Π-types (Γ ⊢ Π_{l,l'} A B : U_{max l l'}) is first stated in §6.2 during the semantics; it belongs with the other formation rules in §5 (or at least a forward reference should be given).","section":"§5/§6.2"},{"comment":"Typos: 'Defintion' (first line of §4); 'Foreward' → 'Foreword' (§1); duplicated 'can can' in Notation 2.1; 'transporing' → 'transporting' (§4.3); stray closing quote in 'engineering formal meta-theory\"' (Conclusion).","section":"Various"},{"comment":"The text cites 'Brunerie and de Boer (2020)' but the bibliography lists only 'M. de Boer, A Proof and Formalization of the Initiality Conjecture...' — please reconcile the citation (presumably G. Brunerie and M. de Boer).","section":"References"},{"comment":"The cofinite-quantification notation ∀x y  x#y#S  ... used in Figure 2 could be glossed inline before first use; readers unfamiliar with the WSLN library may not parse x#y#S.","section":"§5, Figure 2"},{"comment":"The remark that Π-structure on the strict CwF of displayed setoids satisfies η only up to setoid equality (and similarly for identity types) is important motivation for the universe-oriented approach of §6.1; a pointer to where in the artifact this limitation manifests (or a one-line example) would help readers.","section":"§3, after Definition 3.5"}],"recommendation":"minor_revision","confidential_remarks":"The relationship to Palmgren (2022) — the closest prior work — is disclosed prominently and characterized accurately (Palmgren gives closure constructions but not the semantic functions or soundness). Self-citations (Pitts 2026a, 2026b) supply the artifact and the syntax library; both look like legitimate infrastructure rather than salami slicing, though 2026b underpins the WSLN representation and should ideally be reviewed alongside. I recommend asking the authors to archive the Agda artifact with a persistent DOI (e.g., Zenodo), since the main results are stated with links to github.io pages whose longevity is not guaranteed. Subject to the fragment-verification item in my major comments, I see no obstacle to publication."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The one thing worth knowing is that this paper actually delivers the missing piece. Palmgren built setoid infrastructure that looked like it could interpret extensional type theory; Pitts defines the semantic functions, proves single-valuedness and totality of the partial relations, gets soundness for definitional equality, and extracts consistency of ETU as an IRU term. That is the result, and it is machine-checked in safe Agda.\n\nWhat is new is not the broad idea of setoid models—Hofmann, Altenkirch, Palmgren, Coquand, Pujet are all cited and used—but the combination that makes the construction go through in a very bare IRU: the simplified displayed setoid (cartesian product for the heterogeneous relation plus coe/coh, Def. 3.2), a setoid universe of context codes, and the deliberate identification of families with elements of universe codes so the CwF-with-universes structure sits definitionally. The extrinsic, well-scoped locally nameless syntax is ordinary but cleanly executed, and the Streicher-style graph-of-a-partial-function approach is carried all the way to Theorems 6.5–6.8 without handwaving. The linked Agda development is real evidence; treat it as such.\n\nSoft spots are proportionate and mostly external. Consistency is relative to IRU, as stated. The paper itself notes that --safe still allows coinduction and proof-irrelevance annotations and that those are excluded only by hand; there is no textual sign they were used, but the identification of the artifact with the advertised fragment is unmechanized. That is the usual relative-consistency exposure, not an internal hole in the argument. Novelty is program-internal rather than paradigm-shifting; significance is solid inside foundations of type theory and proof assistants.\n\nThis is for people who care about relative consistency, setoid models, and what you can still do inside a weak intensional meta-theory with IR. If that is your reading group, bring it. I would cite it when the topic is models of extensionality or formalized meta-theory of MLTT. A serious editor should send it to referees; the formalization earns the time.","headline":"Pitts finishes the unfinished Palmgren program: a complete, Agda-checked setoid semantics of ETU inside IRU, with a relative consistency corollary.","tokens_in":27652,"tokens_out":548,"would_cite":true,"duration_ms":17306,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B15","03F50","68V15"],"pacs":[],"model":"grok-4.5","headline":"A simple notion of displayed setoids inside intensional type theory supplies a full semantics for extensional type theory with universes and proves its consistency.","keywords":["setoids","displayed setoids","intensional type theory","extensional type theory","universes","inductive-recursive definitions","relative consistency","Agda"],"falsifier":"Exhibit a well-typed IRU term of type “there exists a raw term a such that the empty context derives a : Emp”, or show that the Agda formalization of totality or single-valuedness fails to type-check.","tokens_in":27668,"feed_emoji":"⊥","tokens_out":820,"duration_ms":30918,"temperature":0.7,"pith_summary":"The paper constructs, inside a strictly intensional meta-theory, a model of full extensional Martin-Löf type theory with a hierarchy of universes. The meta-theory is safe Agda without axiom K, equipped with a universe closed under inductive-recursive definitions. Object-theory syntax is given extrinsically via a well-scoped locally nameless representation; its meaning is given by type-valued semantic relations on raw terms that are proved total and single-valued precisely on the well-formed judgments. The model uses a deliberately simple notion of displayed setoid (a family equipped with a heterogeneous equivalence plus coercion maps). As a corollary one obtains a machine-checked proof that the extensional theory is consistent relative to the intensional one. A reader cares because the result shows how much classical extensional reasoning can be recovered, and verified, without ever leaving a purely intensional foundation.","feed_headline":"Setoids prove extensional type theory consistent in Agda","feed_subtitle":"A machine-checked model inside intensional type theory yields relative consistency of ETU","key_machinery":"Displayed setoids: families of types over a base setoid carrying a heterogeneous equivalence relation together with coercion and coherence operations. Combined with an inductively-recursively defined hierarchy of setoid universes of codes, they interpret contexts, types, terms and definitional equality.","core_discovery":"Inside IRU (safe Agda), the displayed-setoid model interprets every well-formed judgment of extensional type theory with universes soundly for definitional equality; consequently there exists an IRU term proving that the empty type is uninhabited in the empty context of the extensional theory.","pith_inferences":["The same infrastructure supplies a foundation for intensional versions of gluing or normalization-by-evaluation arguments for dependent type theories.","The displayed-setoid universes can likely host other extensional features (function extensionality plus uniqueness of identity proofs) without leaving the meta-theory.","Because every definition and proof is machine-checked, the development can serve as a reference for comparing competing notions of setoid in the literature."],"forward_implications":["Extensional type theory with universes is consistent relative to intensional type theory plus induction-recursion.","The simple displayed-setoid notion is strong enough to interpret a full cumulative hierarchy of universes without proof-irrelevant propositions.","Further relative-consistency results about extensionality principles can now be attempted inside a machine-checked intensional setting.","Semantic constructions that classically rely on extensional equality become candidates for fully formal intensional development."],"fun_headline_variants":["Displayed setoids model ETU inside safe Agda IRU","IRU setoid semantics prove ETU consistency","Setoid model interprets ETU judgments soundly in IRU","Displayed-setoid model yields IRU consistency proof of ETU","Safe Agda hosts setoid semantics for extensional type theory"],"cache_read_input_tokens":16512,"weakest_assumption_plain":"The whole consistency claim is only relative to the meta-theory; it stands only if safe Agda with inductive-recursive definitions is itself consistent and faithfully represents the intended intensional type theory.","fun_headline_variants_meta":{"raw":{"variants":["Displayed setoids model ETU inside safe Agda IRU","IRU setoid semantics prove ETU consistency","Setoid model interprets ETU judgments soundly in IRU","Displayed-setoid model yields IRU consistency proof of ETU","Safe Agda hosts setoid semantics for extensional type theory"]},"model":"grok-4.5","effort":"low","cost_usd":0.003715,"raw_usage":{"total_tokens":1119,"prompt_tokens":641,"num_sources_used":0,"completion_tokens":67,"cost_in_usd_ticks":37148000,"prompt_tokens_details":{"text_tokens":641,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":411,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":641,"tokens_out":67,"duration_ms":7273,"temperature":1.0,"reasoning_tokens":411,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-30T16:15:25.883165+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"Exhibit a well-typed IRU term of type “there exists a raw term a such that the empty context derives a : Emp”, or show that the Agda formalization of totality or single-valuedness fails to type-check.","supporting_citations":[],"review_version":1}