{"id":"ee7d636e-84cd-42c2-b611-0a0c1f1ecf2c","arxiv_id":"2507.07208","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A display map 2-category semantics for axiomatic type theory is shown sound, yielding a semantic proof that the identity type computation rule is not admissible.","lead":"The paper builds a 2-categorical semantics for axiomatic type theory, a version of dependent type theory where computation rules are weakened to propositional equalities. It uses this semantics to show that the usual computation rule for identity types is not derivable in the axiomatic theory.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The independence result rests on unproved coherence claims for the weakened groupoid model; the omitted stability check for Definition 4.1 is load-bearing.","rationale":"The reader's weakest assumption identifies precisely the load-bearing gap: Section 5 asserts, without proof, that the weakened groupoid model satisfies all the compatibility conditions of Definitions 4.1 and 4.2. Theorem 5.1, which gives the paper's headline non-admissibility result, depends on this assertion because Theorem 4.11 converts a display map 2-category into a model of ATT only when those conditions hold. I agree with the reader that this is a genuine missing-proof concern rather than a demonstrated contradiction. The paper contains substantial independent support for the general framework: Theorem 4.11 is built from many detailed constructions, and the syntactic soundness theorem 3.6 is plausibly standard. However, the groupoid model is the only place where a concrete independence result is obtained, and its model status is exactly where the proof is sketched rather than supplied. My concrete test targets the most intricate omitted compatibility, the stability of the cloven isofibration structure under re-indexing, because if that fails, the model is not a display map 2-category and the counterexample disappears. I do not see a reason to change the reader's CONDITIONAL verdict: the concern is addressable in revision, but it prevents the central independence claim from being treated as fully established.","tokens_in":48328,"tokens_out":20523,"duration_ms":258207,"concrete_test":"Independently verify the stability equalities for the groupoid model by direct calculation from the definitions in Section 5 and Appendix C: for an explicit non-strict pseudofunctor A and a non-strict pseudofunctor C over Γ.A, compute t^p_g[f.A] and t^{p[f]}_{g'} for a non-identity 2-cell p whose PA-postcomposition is the identity, and check whether t^p_g[f.A] = t^{p[f]}_{g'} and τ^p_g[f.A] = τ^{p[f]}_{g'} from Definition 4.1. If the equality fails, the model is not a display map 2-category and Theorem 5.1 collapses; if it holds, repeat the check for the arrow-object stability condition αA[f] = α_{A[f]} in Definition 4.2.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Theorem 5.1, the paper's headline independence result, depends on (Grpd, D) being a display map 2-category with axiomatic =-types in the sense of Definitions 4.1 and 4.2. Section 5 asserts this ('Without delving too deeply into the details, we state that...') but does not verify the compatibility conditions. In particular, Definition 4.1's fourth condition requires the chosen cloven isofibration lift t^p_g and 2-cell τ^p_g to be stable under re-indexing: t^p_g[f.A] = t^{p[f]}_{g'} and τ^p_g[f.A] = τ^{p[f]}_{g'} for every display map Γ.A.C → Γ.A and every 2-cell p over Γ.A. The groupoid model's lifts are defined by explicit formulas involving inverses of pseudofunctor coherence maps; whether these formulas are preserved by re-indexing is not shown. Likewise, the arrow object αA must satisfy αA[f] = α_{A[f]} to meet Definition 4.2. Without these equalities, the model may fail to induce a display map category via Theorem 4.11, so the counterexample to the computation rule would not exist. The claimed calculation that 'in general Jc[rA] and c will not coincide' also assumes that the reconstructed choices r, φ, and J are the ones from the asserted structure. This is a missing-proof concern, not an observed contradiction.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper develops a 2-categorical semantics for axiomatic type theory (ATT), a dependent type theory in which computation rules are replaced by propositional computation axioms. It introduces display map 2-categories, a 2-dimensional analogue of display map categories, and shows that a display map 2-category endowed with axiomatic identity, Σ, Π, 0, 1, 2, and N types and function extensionality induces an ordinary display map category that is a model of ATT (Theorem 4.11). The paper then proposes a weakened groupoid model, claims it is a display map 2-category with axiomatic identity types, and concludes that it fails the intensional computation rule for identity types, so that rule is not admissible in ATT (Theorem 5.1). Section 6 shows that every such model validates the discreteness rule and uses a syntactic display map 2-category, imported from the author's thesis, to state a completeness theorem for ATT plus discreteness.","tokens_in":48476,"tokens_out":8037,"duration_ms":87428,"significance":"The paper's conceptual contribution is attractive: encoding computation axioms as relaxed 2-categorical universal properties, rather than 1-categorical ones, yields a semantics that generalizes Garner's intensional models and distinguishes axiomatic from intensional type formers. The explicit stability conditions and the appendices show care in the syntactic-to-categorical passage. The weakened groupoid model, if fully verified, would provide a clean semantic proof that the intensional computation rule is not admissible in ATT. However, as it stands, the verification that the groupoid model is a display map 2-category is asserted rather than proved, and a number of stability proofs needed for Theorem 4.11 are deferred or only sketched. The central idea is sound and the missing material appears to be fillable, but the current manuscript is not yet self-contained at the load-bearing points.","major_comments":[{"comment":"Theorem 5.1, the paper's headline independence result, depends on (Grpd, D) being a display map 2-category in the sense of Definition 4.1. The text says 'Without delving too deeply into the details, we state that...' and Appendix C only says that the cloven isofibration structure 'is compatible with this re-indexing choice in the sense of Definition 4.1' and that the arrow object 'can be verified to be compatible with the re-indexing choice in the sense of Definition 4.2.' No proof is given for the crucial fourth condition of Definition 4.1, namely the equalities t^p_g[f.A] = t^{p[f]}_{g'} and τ^p_g[f.A] = τ^{p[f]}_{g'} for the chosen cloven isofibration lifts. Since Theorem 5.1 relies on this structure to induce a model of axiomatic identity types, this is a load-bearing gap. Please supply the full verification, or a precise reference where it is carried out.","section":"Section 5, 'Re-indexing structure and arrow object structure on display maps'; Appendix C"},{"comment":"Theorem 4.11 asserts that every display map 2-category with the axiomatic type-former data induces a display map category with the corresponding syntactic data, and the proof of that theorem rests on Propositions 4.3, 4.5, 4.8, and 4.10. Appendix B proves Proposition 4.3 and parts of Proposition 4.8, but Proposition 4.5 (for Σ-types) and Proposition 4.10 (for 0-, 1-, 2-, N-types) are only declared to be 'completely analogous' or 'analogous.' These stability conditions are exactly what makes the induced display map category split, so they are essential for Theorem 4.11. The paper should include complete proofs of these propositions, or at least a detailed treatment of the non-obvious cases such as Σ and N.","section":"Appendix B; Propositions 4.5 and 4.10"},{"comment":"The proof of Theorem 5.1 hinges on the claim that 'following the construction at paragraphs Elim Rule and Comp Axiom for =-types, one can reconstruct the choice functions r, φ, and J and observe that Jc acts on objects as...' This calculation is asserted rather than derived, even though it depends on the specific chosen arrow object and cloven isofibration structure on the weakened groupoid model. Because the inequality Jc[rA] ≠ c is the entire content of the non-admissibility claim, the calculation should be presented explicitly or accompanied by a complete proof.","section":"Appendix C, computation of Jc[rA]"}],"minor_comments":[{"comment":"In the Comp Axiom clauses for 2-types, the display map for β^{2,⊤}_{c,d} is written as Γ.Id_{C[⊤]}[ind^2_{c,d}[⊤]; c], and the displayed arrow is written as ind^2_{c,d}[⊤]; c; the second occurrence of c should be d.","section":"Definition 3.5, 2-types"},{"comment":"In the bullet for axiomatic 2-types, the 2-functor U is written as (D/Γ.1)† → (C/Γ.1)2; the context should be Γ.2, not Γ.1.","section":"Definition 4.9, 2-types"},{"comment":"Diagram (10) is referenced in Section 2.1 before it is introduced in Appendix A; please add a forward reference or introduce the diagram earlier.","section":"Section 2.1 and Appendix A"},{"comment":"The completeness theorem 6.3 is obtained by importing the syntactic display map 2-category and its type-former structure from the author's thesis [38], with only a sentence saying that the remaining type formers can be handled analogously. Since this is a claimed theorem of the paper, please state explicitly which parts are new and which are cited, and consider expanding the proof if completeness is to be counted as a contribution.","section":"Section 6"},{"comment":"Theorem 4.12 is stated without a proof; the surrounding paragraphs give a helpful discussion but not a formal verification. Either provide a proof or label the statement as a remark.","section":"Section 4.5"}],"recommendation":"major_revision","confidential_remarks":"The main theorems are plausible and the approach is worth publishing once the missing verifications are supplied. The heavy reliance on the author's thesis [38] for the syntactic 2-category is a fit-for-purpose concern, but the core results of the paper (Theorems 4.11 and 5.1) do not reduce to that citation; they need their own missing proofs. I recommend major revision rather than rejection because the gaps appear fillable within the manuscript's scope."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Main thing you should know: this is a real contribution to categorical semantics, not a repackaging. Spadetto generalizes Garner's display map 2-categories to axiomatic type theory by weakening normal isofibrations to cloven isofibrations, injective equivalence to homotopy equivalence, and right adjoints to right biadjoints. Those relaxations look like the right way to separate axiomatic from intensional type formers. Theorem 4.11, turning such a 2-category into a display map category model of ATT, is a lot of work; many stability conditions are handled explicitly in Appendices A and B, and the syntactic soundness argument in Section 3 is plausible. The weakened groupoid model in Section 5, using arbitrary pseudofunctors rather than strict ones, is a neat new presentation.\n\nThe soft spot is exactly where the stress-test note points. The paper's headline claim, Theorem 5.1, depends on (Grpd, D) being a display map 2-category with axiomatic =-types. But the key passage in Section 5 says \"Without delving too deeply into the details, we state that...\" and then asserts the re-indexing, cloven isofibration, and arrow object structures satisfy the compatibilities in Definition 4.1. Those compatibilities are not merely cosmetic: Definition 4.1's fourth condition requires the chosen lifts and 2-cells to be stable under re-indexing, and Definition 4.2 requires the same for arrow objects. Appendix C provides some details but not the full verification of those equalities. The gap is addressable, and I would bet the structure does work, but as written the independence result is not fully established. I agree with the reader's conditional verdict.\n\nMinor soft spots: several proofs in Section 4 are delegated to \"completely analogous\" arguments, and Section 6 leans on the author's thesis. That is acceptable for a paper this size, but a referee will have to do real checking work. The citation pattern is honest; the self-citations are for background and completeness, not hiding the main argument.\n\nWho this is for: people working on higher-categorical semantics of dependent types. It deserves serious refereeing. My recommendation: send it out, ask the author to prove the groupoid model compatibility in detail and integrate it into the paper, then accept.","headline":"Genuinely new 2-categorical semantics for axiomatic type theory with a plausible independence result, but Section 5 needs a real proof of the compatibility claims before Theorem 5.1 should be trusted.","tokens_in":49097,"tokens_out":3404,"would_cite":true,"duration_ms":41025,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B15","03G30","18N10"],"pacs":[],"model":"deepseek-v4-flash","headline":"Display map 2-categories give a sound semantics for axiomatic type theory, and a weakened groupoid model shows the identity-type computation rule is not admissible.","keywords":["axiomatic type theory","computation axioms","dependent type theory","display map 2-categories","categorical semantics","groupoid model","identity types","function extensionality"],"falsifier":"Take a non-strict pseudofunctor in the weakened groupoid model and compute the re-indexing pastings and isofibration transport required by Definitions 4.1 and 4.2; if any required equality fails, the model is not a display map 2-category and Theorem 5.1 collapses. Separately, any derivation in ATT of the judgemental equality $J(c,x,x,r(x)) \\equiv c(x)$ would directly refute the paper's main non-admissibility claim.","tokens_in":48009,"feed_emoji":"📐","tokens_out":12810,"duration_ms":126589,"temperature":0.7,"pith_summary":"Axiomatic type theory (ATT) is the variant of dependent type theory in which each type former's computation rule is downgraded from a judgemental equality, like $t \\equiv t'$, to a propositional equality, like $p : t = t'$, called a computation axiom. This paper proves that such theories have a uniform 2-categorical semantics: every display map 2-category equipped with axiomatic identity, $\\Sigma$-, $\\Pi$-, function extensionality, and 0-, 1-, 2-, $N$-types induces an ordinary display map category that models ATT, and that interpretation is sound. The proof works by encoding each axiomatic type former as a 2-dimensional universal property, so that the 1-dimensional choice functions needed for a syntactic model arise automatically. As an application, a weakened groupoid model in which types are pseudofunctors into the category of groupoids models axiomatic identity types without validating their judgemental computation rule, establishing that the computation rule of identity types is not admissible in ATT. If the paper is right, checking a handful of 2-categorical properties is enough to build models of very intensional dependent type theories, and a specific meta-theoretic independence question is settled.","feed_headline":"Weakened groupoid model refutes identity computation rule","feed_subtitle":"2-categorical display-map semantics for axiomatic type theory show the identity computation rule is not admissible.","key_machinery":"The load-bearing object is the display map 2-category: a $(2,1)$-category whose chosen display maps are cloven isofibrations, with a split re-indexing structure and, for identity types, an arrow object $\\alpha_A$ for each display map $P_A$ that represents 2-cells between sections of $P_A$ as sections of the identity-type display map. The arrow object is what turns the syntax of axiomatic identity types into data: elimination terms are first built as 'pseudo-terms' whose codomain is a display map only up to a 2-cell, and the cloven isofibration structure strictifies them into genuine sections while producing exactly the 2-cells that are then read as computation axioms. Relaxing normal isofibrations to merely cloven ones is what keeps the computation axioms from collapsing into the judgemental computation rules. The same machinery, with homotopy equivalences, biadjoints, and bireflections in place of their retract versions, encodes the remaining axiomatic type formers.","core_discovery":"The central claim is that the intensional type formers of axiomatic type theory admit a 2-categorical description, and that this description is strong enough to carry the semantics. Concretely, axiomatic identity types are encoded by arrow objects for display maps, axiomatic $\\Sigma$-types by closure of display maps under composition up to homotopy equivalence, axiomatic $\\Pi$-types and function extensionality by a right biadjoint, and axiomatic 0-, 1-, 2-, $N$-types by bireflections. Any display map 2-category carrying these structures induces a split display map category with all the choice functions of Definitions 3.1--3.5, so by the standard soundness argument the interpretation of ATT is well defined and sound (Theorems 3.6 and 4.11). The decisive application is a display map 2-category based on the groupoid model in which display maps are cloven, but not necessarily normal, isofibrations: it validates axiomatic identity types and their computation axiom, yet fails the judgemental computation rule $J(c,x,x,r(x)) \\equiv c(x)$, proving that rule is not admissible in ATT (Theorem 5.1).","pith_inferences":["The paper leaves implicit that the discreteness obstruction is a feature of any 2-categorical display-map semantics: the arrow object forces a type to behave like a 1-type, so a complete semantics for ATT without discreteness will have to go one dimension higher, as the paper's own closing discussion suggests.","One testable extension is to apply the same encoding to directed identity types: replacing arrow objects by directed hom-objects in a display map 2-category should produce a model of directed versions of ATT, paralleling existing categorical models of directed type theory.","Because the weakened groupoid model separates the computation axiom from the computation rule by the strictness of the pseudofunctor, one can vary the pseudofunctor to generate further independence results, including analogous $\\Sigma$ or $\\Pi$ computation rules, although the paper only carries out the identity-type case.","Since type checking in ATT is already known to be decidable in quadratic time, a practical consequence is that 2-categorical models could serve as the underlying denotational description for implementations of objective type theory; this is an inference, not a claim of the paper."],"forward_implications":["Any display map 2-category endowed with the listed axiomatic type-former data is automatically a model of ATT, so model construction reduces to checking 2-dimensional universal properties rather than choosing interpretation functions rule by rule.","The interpretation is sound: in any such structure every derivable judgement of ATT receives a well-defined denotation, and judgemental equalities are respected.","The weakened groupoid model $(\\mathrm{Grpd}, D)$ is a model of axiomatic identity types that does not validate the computation rule for identity types; hence that rule is not admissible in ATT.","Every display map 2-category validates the discreteness rule, so the semantics is sound for ATT plus discreteness; because that rule is not derivable in ATT, this class of models cannot be complete for ATT alone.","If, in the same data, all the equivalence 2-cells are identities and the display maps are normal isofibrations, the induced model validates the full intensional computation rules and is a model of ITT."],"supporting_citations":[{"why":"Supplies the 2-categorical framework of arrow objects and isofibrations for intensional type theory that the paper relaxes to the axiomatic case.","marker":"[17]"},{"why":"Provide the groupoid model that the paper weakens by taking display maps to come from arbitrary pseudofunctors instead of strict functors.","marker":"[24, 25, 41]"},{"why":"Supplies the notion of display map category and the closure-property characterizations of extensional type formers that the paper generalizes.","marker":"[27]"},{"why":"Gives the standard soundness argument by induction on derivations that Theorem 3.6 relies on.","marker":"[40]"},{"why":"Provides the standard syntax-semantics correspondence for dependent type theory used in the interpretation clauses and soundness proof.","marker":"[23]"},{"why":"Contains the syntactic construction of a display map 2-category from ATT plus the discreteness rule, used in the completeness section and for the axiomatic identity and Sigma type data.","marker":"[38]"}],"fun_headline_variants":["Weakened groupoid model refutes identity computation rule","Axiomatic identity types: computation rule not admissible","2-categorical semantics: identity rule fails","Display map 2-categories show identity rule inadmissible","Semantic proof: identity computation rule not admissible"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the weakened groupoid model of Section 5 really is a display map 2-category: the paper asserts, without proving, that its re-indexing, cloven isofibration, and arrow-object structures satisfy all the compatibility laws of Definitions 4.1 and 4.2, and the independence result rests on that.","fun_headline_variants_meta":{"raw":{"variants":["Weakened groupoid model refutes identity computation rule","Axiomatic identity types: computation rule not admissible","2-categorical semantics: identity rule fails","Display map 2-categories show identity rule inadmissible","Semantic proof: identity computation rule not admissible"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000834,"raw_usage":{"total_tokens":3697,"prompt_tokens":1062,"completion_tokens":2635,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":678,"completion_tokens_details":{"reasoning_tokens":2560}},"tokens_in":678,"tokens_out":2635,"duration_ms":20205,"temperature":1.0,"reasoning_tokens":2560,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T18:45:49.359973+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a non-strict pseudofunctor in the weakened groupoid model and compute the re-indexing pastings and isofibration transport required by Definitions 4.1 and 4.2; if any required equality fails, the model is not a display map 2-category and Theorem 5.1 collapses. Separately, any derivation in ATT of the judgemental equality $J(c,x,x,r(x)) \\equiv c(x)$ would directly refute the paper's main non-admissibility claim.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the 2-categorical framework of arrow objects and isofibrations for intensional type theory that the paper relaxes to the axiomatic case."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the notion of display map category and the closure-property characterizations of extensional type formers that the paper generalizes."},{"cited_title":"Streicher","cited_arxiv_id":null,"evidence_quote":"Gives the standard soundness argument by induction on derivations that Theorem 3.6 relies on."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the standard syntax-semantics correspondence for dependent type theory used in the interpretation clauses and soundness proof."},{"cited_title":"Spadetto","cited_arxiv_id":null,"evidence_quote":"Contains the syntactic construction of a display map 2-category from ATT plus the discreteness rule, used in the completeness section and for the axiomatic identity and Sigma type data."}],"review_version":1}