{"id":"fea82232-6ad5-4ef4-ba4e-6aa918ddc4bc","arxiv_id":"2607.13662","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A domain-theoretic logical-relations technique proves injectivity and no-confusion of type constructors for non-normalising dependent type theories with η laws, including type-in-type systems, without relying on normalisation.","lead":"This paper introduces a domain-theoretic proof technique for proving definitional inversion properties — injectivity and no-confusion of type constructors — in dependent type theories that need not normalise, covering even type-in-type systems with η-conversion. It reports the first such result for this combination and says all proofs are mechanised in Agda, Lean and Rocq.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Adequacy/Fundamental Lemma (Thm 2.35–2.36) is asserted, not proved; injectivity of Π rests entirely on it, and the claimed mechanizations are not inspectable in this version.","rationale":"The paper's novelty is the claim that a domain-theoretic logical relation proves definitional inversion without normalisation. Everything downstream (SR, progress) is derived from injectivity of Π, which is one step from the fundamental lemma. The high-level structure is coherent: the domain equation, finitary projectors, semantic typing, and the logical relation clauses are plausible, and the stage/n index makes the definition well-founded. I did not find an obvious mathematical contradiction or a circular use of injectivity inside the logical-relation definition: the syntactic equalities in the Π clause are discharged in the congruence base case and propagated through the stated closure properties. The genuine uncertainty is whether the large adequacy induction actually goes through for all conversion rules, particularly η and head-expansion. The text gives no proof sketch of the hard cases and the artifacts are anonymized. This is a verification-transparency concern, not a demonstrated flaw, so the correct disposition is to keep the CONDITIONAL verdict until the mechanizations are public and checked.","tokens_in":28392,"tokens_out":23249,"duration_ms":252325,"concrete_test":"Make the three mechanizations public with fixed commits. In each, locate and check the theorem corresponding to Thm 2.35/2.36 (e.g. adequacy/fundamental lemma) and Corollary 2.37. Run the respective kernel (Agda, Lean, Rocq) and use `#print axioms`/`Print Assumptions` to confirm the Adequacy theorem is accepted, with no axioms beyond the three explicitly declared in the Rocq version; if any file fails or the theorem name is absent, the concern lands.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central corollary 2.37 depends on Theorem 2.36 (and its substitution-relative version 2.35), which is stated without proof: the text only says it is proved by induction and verified in supplementary mechanizations. The logical relation in §2.6 is defined by recursion on the stage and semantic witness, and the properties in §2.7 (Symm, Trans, Conv, Mono, Join, HeadRed, Stability) are also stated without proof. Any failure of one of these closure properties in the induction on conversion derivations—especially cases involving the η rule or head-expansion—would break the proof of injectivity. The formalizations are anonymized supplementary material, so this version does not allow a reader to check the crucial induction. The Rocq version additionally relies on three axioms (funext, propext, proof irrelevance), and the coverage table shows it does not cover the extensions; neither fact by itself is fatal, but it makes the unverified core more consequential.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces a domain-theoretic proof technique for establishing definitional inversion principles (injectivity and no-confusion of type constructors) in dependent type theories without relying on normalization. The technique is demonstrated on MLTTη, a type theory with Π-types, a universe with type-in-type, and β/η conversion, which is both non-normalizing and has η laws—features that defeat confluence-based and normalization-based approaches. The authors build a finitary projection model of the syntax, define a stage-indexed logical relation over compact elements of a recursive domain, and claim an adequacy/fundamental lemma (Theorems 2.35–2.36) from which they derive injectivity of Π (Corollary 2.37), subject reduction (Theorem 2.38), and progress (Theorem 2.39). They then sketch extensions to Σ-types, unit type, fixed points, natural numbers, identity types, and a strict Prop universe. Three mechanized proofs (Agda, Lean, Rocq) are claimed, but only as anonymized supplementary material.","tokens_in":28574,"tokens_out":5231,"duration_ms":52923,"significance":"If the central adequacy theorem is correct, this is a significant advance for the metatheory of dependent type systems. It offers a route to injectivity/no-confusion in non-normalising systems with η laws, using only simple induction on natural numbers in a weak ambient logic, and with claimed machine-checked implementations in three proof assistants. The potential applications to verified kernel projects such as Lean4Lean and MetaRocq are real and well-motivated. The main weakness is that the crucial Theorem 2.35–2.36 is stated without proof in the text and the mechanized artifacts are not available for inspection in this version, so the core result is not independently verifiable from the paper alone. The extensions in Section 3 are also presented as sketches rather than full proofs.","major_comments":[{"comment":"The central claim rests on the Adequacy and Fundamental Lemma (Theorems 2.35–2.36), which are stated without proof. The text only says they are proved by induction and verified in the supplementary mechanizations. Corollary 2.37 derives injectivity of Π directly from Theorem 2.36, so any gap in this induction—particularly in the η-law or head-expansion cases—invalidates the main result. A journal version must either prove these theorems in the text/appendix or make the mechanized proofs available and inspectable. As it stands, the central derivation is not independently verifiable from the paper alone.","section":"§2.7–2.8, Thms 2.35–2.36, Cor 2.37"},{"comment":"The listed properties of the logical relation are stated without proof. The fundamental lemma proceeds by induction on conversion derivations and necessarily uses all of these closures; for example, the Head Reduction lemma (2.34) is what makes the η-rule and head-expansion cases tractable. A failure in any one of these closures would break Theorem 2.36. Please include at least proof sketches or an explicit statement of which mechanization proves which property.","section":"§2.7, closure properties (Symm–Join, Cor 2.33, Lemma 2.34)"},{"comment":"The formalizations are anonymized and not available for inspection in this submission. Moreover, the coverage table shows non-uniform coverage (e.g., Rocq's row for the extensions is marked '0 and S only', and Lean's Id is 'transport only'), and the Rocq development relies on three axioms (funext, propext, proof irrelevance). The reader cannot check that the core MLTTη result—which all three systems are claimed to verify—is actually mechanized. Please provide the artifacts or a detailed proof, and clarify the table entries.","section":"§4, supplementary material / coverage table"}],"minor_comments":[{"comment":"The small-caps macros produce non-words: PRoof, TheoRem, CoRollaRy, PRoposition, PRop, etc. Standardize these for final publication.","section":"Throughout"},{"comment":"The proof should justify why Π(⊥,⊥) satisfies the preconditions of Theorem 2.36: it must be shown that Π(⊥,⊥) ≤ JΠx:A B K⊥ and Π(⊥,⊥) : U. This is not explicit.","section":"§2.8, proof of Cor 2.37"},{"comment":"The coverage table should state explicitly what the symbols ('3', '0') mean for each cell, and which proof-assistant files correspond to which extension. This is necessary to interpret the claimed mechanization coverage.","section":"§4, Table 1"},{"comment":"The extensions are presented as sketches; if they are meant as concrete contributions, add at least a map from each extension to the corresponding mechanization files or state clearly which results are proved versus conjectured.","section":"§3"},{"comment":"The 'grey premises' convention should be rendered robustly (e.g., with italics or brackets) so that the distinction survives black-and-white printing or ordinary PDF viewers.","section":"§2.7"},{"comment":"Several references are to preprints or drafts (Felicissimo–Winterhalter 2026, Liu–Weirich 2026, Felicissimo et al. 2026). Add DOIs or stable identifiers where available, and mark those still in submission.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The main barrier to acceptance is that the paper's central theorem (Thms 2.35–2.36) is not proved in the text and the mechanized artifacts are not available. The authors should be encouraged to include a proof sketch or to make the relevant formalizations available for review. The 'Use of AI' statement is unusual but not a technical concern."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The headline is simple: this is the first credible-looking proof of injectivity of Π for a type-in-type theory with η, and the domain-theoretic trick — a logical relation indexed by compact elements, interpreted over a degenerate ⊥ environment — is a genuine advance. The paper also gives subject reduction and progress for that system, and sketches extensions to Σ, unit, Y, ℕ, identity types, and strict Prop. That is a real result, not a rediscovery.\n\nWhat I like: the technique is conceptually clean. The finitary projection model collapses lots of structure, but the logical relation still reads off syntactic conversions, and the authors are transparent about what the model cannot do — no inversion for neutrals, no refutation of inhabitation. The connection to Coquand–Huber's adequacy theorem is well explained, and the paper explicitly solves the open problem they posed. The three claimed mechanisations (Agda, Lean, Rocq) are strong evidence if the code is genuine; the authors even disclose the use of AI assistance, which is more honest than most.\n\nThe soft spot is just where the stress-test note points: Theorem 2.35/2.36, the fundamental adequacy lemma, is stated and not proved. The text only says it is proved by induction and verified in the mechanisations. The properties in §2.7 (Symm, Trans, Mono, Join, Conv, HeadRed, Stability) are also stated without proof. This matters because Corollary 2.37 — injectivity of Π — rests entirely on that induction. I don't see a hidden circularity: the logical-relation clause at Π does exactly what the conclusion needs, and the real work is in the induction on conversion derivations, especially around η and head expansion. But I also cannot verify that induction from the submitted text. The formalisations are the load-bearing evidence, and they are anonymized, so I can't inspect them. The Rocq version uses funext, propext, and proof irrelevance and doesn't cover the full extension table — again not fatal, but it makes the unverified core more consequential.\n\nIf the mechanisations check out, this is a top-venue result. If some closure property fails in that induction, it collapses. Nothing in the paper suggests a failure, but the burden is on the artifacts.\n\nI would send this to a strong referee and ask for the formalisations to be public with commit hashes, plus at least a proof sketch of the adequacy induction in an appendix. For the next reading group, I'd bring it — the technique deserves discussion even before verification.","headline":"Promising new technique for definitional inversion without normalisation, but the central adequacy lemma is unproved in the text and the mechanisations are not yet inspectable — worth a real refereeing.","tokens_in":29142,"tokens_out":3115,"would_cite":true,"duration_ms":31884,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B15","68Q55"],"pacs":[],"model":"deepseek-v4-flash","headline":"A domain-theoretic model proves definitional inversion for dependent types without any normalisation theorem, even in the presence of η laws and type-in-type.","keywords":["definitional inversion","injectivity of type constructors","domain theory","finitary projectors","logical relations","eta laws","type-in-type","subject reduction"],"falsifier":"One concrete way to settle it: in the paper's system, search for a conversion Γ ⊢ Πx:A B ≡ Πx:A' B' with A and A' not convertible; if such a derivation exists, Corollary 2.37 is false. Short of that, inspect the mechanised proof of adequacy for a single unclosed case in the induction on conversion — one rule whose logical-relation closure fails would collapse subject reduction and progress along with injectivity.","tokens_in":28266,"feed_emoji":"λ","tokens_out":8728,"duration_ms":82082,"temperature":0.7,"pith_summary":"The paper's central claim is that definitional inversion — the principle that equal type-forming expressions have equal parts, for example Πx:A B ≡ Πx:A' B' forces A ≡ A' and B ≡ B' — can be proved by a domain-theoretic logical relation indexed by compact elements, with no appeal to normalisation. This matters because normalisation fails for type theories with type-in-type, for dependently typed languages with general recursion, and is unavailable inside a logic trying to reason about itself. The method handles η laws, which have long defeated confluence-based arguments, and scales to sums, unit, fixed points, natural numbers, identity types, and a universe of proof-irrelevant propositions. The immediate corollaries are subject reduction and progress for a minimal dependent type theory with universe-in-universe, β, and η.","feed_headline":"Prove type-constructor injectivity without normalisation","feed_subtitle":"Compact-element logical relations give injectivity, subject reduction, and progress for dependent type theory with η and type-in-type.","key_machinery":"The key object is a recursive domain D, realised through its compact elements (a conditional upper semi-lattice) built as a colimit of finite stages. Its coalesced sum validates η by identifying λ(⊥) with ⊥. Types are finitary projectors, i.e. continuous idempotent approximations; semantic typing u : a is a stage-indexed relation on compact elements. The logical relation Γ ⊨ A ≡ A' type | a and Γ ⊨ M ≡ N : A | u:a is defined by recursion on the stage and on the compact witnesses, with a degenerate clause at ⊥; the Π-clause requires both syntaxes to head-reduce to Π-types with related parts. Adequacy (Theorems 2.35 and 2.36) is the bridge from witnesses to syntax, proved by induction on deriv","core_discovery":"The paper establishes that in a dependent type theory with universe-in-universe plus β and η, equality Γ ⊢ Πx:A B ≡ Πx:A' B' : 𝒰 forces A ≡ A' and B ≡ B', and from this derives subject reduction and progress. Types are interpreted as finitary projectors on a recursive domain built from compact elements; a stage-indexed semantic typing and a logical relation indexed by compact witnesses, proved adequate by induction, turn semantic witnesses into object-level conversions. The same model yields disjointness of Π and 𝒰 and refutes definitional UIP for the identity type.","pith_inferences":["Inference: the same 'add a code, add a logical-relation clause, extend soundness and adequacy' recipe should transfer to coinductive types, quotient types, or gradual dependent types, all areas where normalisation is unavailable; the paper targets this direction but does not prove it.","Inference: because the compact witness functions as a generalised step index, the construction suggests a way to derive a conversion-checking algorithm or completeness statement from the logical relation, which the paper leaves unexplored.","Inference: the model can only refute equality rules, never inhabitation (every semantic type is inhabited by ⊥), so it cannot say anything about propositional consistency; users of the technique should not expect consistency-style meta-theorems from it.","Inference: the paper's open problem — proving definitional inversion for neutral terms — could be attacked by combining this domain model with a separate typed confluence argument, since the two tools cover complementary parts of the conversion relation."],"forward_implications":["In the minimal system with type-in-type and η, every equality between Π-types decomposes into equalities of domains and codomains (Corollary 2.37).","Subject reduction and progress follow, giving a well-behaved operational semantics for a theory that was previously out of reach of confluence- and normalisation-based tools.","The construction extends to Σ with surjective pairing, unit with η, a fixed-point combinator, natural numbers with large elimination, the identity type with transport, and a Prop universe with definitional proof irrelevance; it can also read off sort injectivity for universe hierarchies.","Because the ambient logic is weak (essentially induction on natural numbers), the method is usable in projects that formalise a type theory inside itself, where proving normalisation is impossible.","The model refutes the rule of definitional uniqueness of identity proofs, showing that the identity type is genuinely proof-relevant in this setting."],"fun_headline_variants":["Injectivity without normalization: a new proof technique","Prove type-constructor injectivity sans normalization","Definitional inversion without normalisation: domain theory","First proof of type-constructor injectivity with η and type-in-type","Logical relations prove injectivity without normalization"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The proof stands or falls on the fundamental lemma (Adequacy): the induction showing that every typing and conversion rule, including η, lands in the logical relation at the appropriate compact witnesses, with the listed closure laws (symmetry, transitivity, monotonicity, joins, head reduction) verified; the paper outsources the verification to the accompanying mechanisations rather than displaying the induction.","fun_headline_variants_meta":{"raw":{"variants":["Injectivity without normalization: a new proof technique","Prove type-constructor injectivity sans normalization","Definitional inversion without normalisation: domain theory","First proof of type-constructor injectivity with η and type-in-type","Logical relations prove injectivity without normalization"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000419,"raw_usage":{"total_tokens":1960,"prompt_tokens":675,"completion_tokens":1285,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":419,"completion_tokens_details":{"reasoning_tokens":1211}},"tokens_in":419,"tokens_out":1285,"duration_ms":11520,"temperature":1.0,"reasoning_tokens":1211,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-02T04:30:32.105212+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"One concrete way to settle it: in the paper's system, search for a conversion Γ ⊢ Πx:A B ≡ Πx:A' B' with A and A' not convertible; if such a derivation exists, Corollary 2.37 is false. Short of that, inspect the mechanised proof of adequacy for a single unclosed case in the induction on conversion — one rule whose logical-relation closure fails would collapse subject reduction and progress along with injectivity.","supporting_citations":[],"review_version":1}