{"id":"9594a9a8-b69b-439d-a797-3cef60f3489b","arxiv_id":"2412.19946","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Nearly every categorical model of dependent type theory embeds as a usually full sub-2-category of comprehension categories, with each model distinguished by which maps its comprehension functor represents.","lead":"This paper maps out the many different categorical structures used to model dependent type theory, showing that almost all of them are special cases of one structure: comprehension categories. It gives researchers a reference diagram for translating between models like categories with families, display map categories, and contextual categories.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified: the comparison theorems are coherent in the paper's stated set-theoretic scope, and the strict-equality caveat is explicitly flagged.","rationale":"The reader's weakest assumption correctly identifies a foundational sensitivity, and I agree it is the most substantive limitation. However, I do not classify it as load-bearing for the central claim because the paper explicitly declares a set-theoretic setting and flags the affected results in Further Directions. The abstract's claim that 'almost all established notions embed as sub-2-categories' is a theorem about a specific 2-categorical framework; within that framework, the proofs are consistent with standard category theory and I found no counterexample to the stated isomorphisms or equivalences. The distinction between isomorphism and equivalence, and between strict and pseudo maps, is handled carefully in examples such as Example 2.23. A conditional verdict is appropriate given the survey nature and sketchy proofs, but the reader's concern about strict equality does not require a stronger rejection; it is a scoping caveat. Hence I recommend UNCHANGED.","tokens_in":23112,"tokens_out":18869,"duration_ms":191461,"concrete_test":"Formalize the proof of Theorem 1.16 (DMC ≅ CompCat^{str2}_{repl}) in UniMath with set-based categories and strict equality, then attempt the same statement with univalent categories. If the proof requires 'injective on objects' in an essential way and the theorem only holds as an equivalence in the univalent setting, the reader's caveat is substantiated; if the isomorphism can be stated and proved without strict object equality, the caveat is immaterial.","verdict_should_be":"UNCHANGED","load_bearing_attack":"I read the central claim as a set-theoretic 2-categorical statement: comprehension categories with strict maps and strict equality of objects are taken as the unifying language. Within that scope, the embeddings and isomorphisms (DMC ≅ CompCat^{str2}_{repl}, sDMC ≅ CompCat^{str2}_{sub}, Clan ≅ CompCat^{str2}_{rtd,repl,compcl}, and the Section 4 comparisons) are internally coherent. The main caveat, strict equality of objects, is not hidden: the authors state in Further Directions that 'some 1- and strict 2-categorical results in Section 4 rely on a setting where strict equality of objects in a category is available.' This is a real scope limitation, especially for readers working in univalent foundations, but it does not invalidate the central claim as stated, since the paper explicitly declares its foundational agnosticism and identifies the affected results. I found no concrete mathematical error in the comparison theorems or the adjunctions; the proofs marked 'routine' align with standard constructions in the cited literature. The closest thing to a load-bearing risk is the sensitivity of the taxonomy to non-equivalence-invariant properties, but the authors flag this in Remark 7a as well. Thus, while the reader's conditional is reasonable, I do not see a concern that rises to the level of changing the verdict.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes comprehension categories with pseudo maps as a unifying 2-categorical language for models of dependently-sorted algebraic theories. It establishes, or sketches, a series of embeddings, isomorphisms, and equivalences between display-map-style models (display map categories, structured display map categories, clans, finite-limit categories) and type-primitive models (categories with attributes, categories with families, natural models, contextual categories, C-systems, B-systems). The relationships are summarised in diagrams for the rooted and unrooted cases, and the paper distinguishes carefully between strict maps, pseudo maps, and transformations. The authors flag at the end that some results rely on a setting with strict equality of objects.","tokens_in":23275,"tokens_out":24711,"duration_ms":271916,"significance":"If correct, the paper provides a valuable systematisation of a scattered literature, organizing the main categorical models of dependent type theory around comprehension categories and making explicit where the comparisons are equivalences, adjunctions, or mere embeddings. Its strengths include a clear 2-categorical treatment of pseudo versus strict maps, a uniform notation for the relevant subclasses of comprehension categories, and an honest discussion of non-invariance and foundational caveats. The main comparisons are coherent within the stated set-theoretic scope, and I agree with the reader that the strict-equality caveat is a scope limitation rather than a hidden error.","major_comments":[{"comment":"The stated isomorphism sDMC ≅ CompCat^{str2}_{sub} is asserted without a proof; the text immediately contrasts it with Theorem 1.16 but gives no argument. Since the non-replete case is precisely where the paper claims strict and pseudo maps diverge, and since this result is one of the headline identifications of Section 3.1, please provide a proof or at least a complete sketch, showing that the object map, the 1-cell map, and the 2-cell map are bijections on the nose.","section":"§3.1, Theorem 2.22"},{"comment":"The pseudo-map equivalences CwA^{ps} ≃ CompCat^{ps}_{disc} and CwA^{ps} ≃ CompCat^{ps,spl}_{full,spl} are not established by the cited Blanco results, which are 1-categorical. The proofs say 'similarly direct'/'direct'; because the paper's contribution is precisely the 2-categorical comparison, please expand these proofs or provide precise references for the 2-categorical statements.","section":"§4.1, Propositions 3.8 and 3.9"}],"minor_comments":[{"comment":"The sentence 'All our 2-categories and functors are strict' is potentially confusing, since the paper's main 1-cells are pseudo maps; please clarify that strictness refers to the composition of 2-cells and the sense in which functors between the 2-categories are strict.","section":"§1 and Definition 1.1"},{"comment":"The notation CompCat^{str1,spl}_{full,spl} and CompCat^{ps,spl}_{full,spl} is hard to parse, with 'spl' appearing both as a condition on objects and as a restriction on maps; please define the convention explicitly at first use.","section":"Definition 7.3 and Proposition 3.9"},{"comment":"The description of the display maps in C' appears garbled: the sentence contrasting left and right point inclusions is self-contradictory as printed. Please correct the example so that the intended failure of strict preservation of display maps is unambiguous.","section":"§3.1, Example 2.23"},{"comment":"The diagrams use ⊥ to denote adjunctions but do not indicate whether the displayed arrow is the left or right adjoint; the text states the directions, but a note in the captions would make the figures self-contained.","section":"Figures 3–5"},{"comment":"The strict-equality caveat is placed only in the final section; since it affects the isomorphisms in Theorems 1.16 and 2.22 as well as Section 4, please state the caveat in the introduction or at the first use of these comparison results.","section":"Further Directions"}],"recommendation":"major_revision","confidential_remarks":"The paper is a survey-style systematisation rather than a new-theorem paper, and it overlaps with the authors' APLAS proceedings version; the related-work section is adequate and I see no disclosure concern. The main revision request is to make the load-bearing 2-categorical comparison proofs sufficiently explicit for the journal readership."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear Colleague,\n\nThe one thing to know: this paper delivers a genuinely useful 2-categorical map of the model zoo for dependently-sorted algebraic theories, and the central claim—that comprehension categories are a unifying hub—holds up in the set-theoretic setting the authors declare. I read the full text and found no load-bearing errors.\n\nWhat is new: several adjunctions and equivalences that were folklore or scattered. The right adjoint from clans to finite-limit categories (Thm 3.6) and the strict/pseudo equivalence for contextual categories (Prop 4.6, Cor 4.7) are real additions. The repletion/fullification adjunctions (Thm 1.17) organize the subcategory lattice nicely. The paper is careful with citations: it credits Blanco, Coraglia–Emmenegger, and others, and it does not oversell its novelty.\n\nWhat is soft, in proportion: many proofs are left as \"routine\" or \"immediate\". That is acceptable for a survey, but a referee will want a few more details. The bigger caveat, which the authors explicitly flag in Further Directions, is that some strict-categorical results rely on strict equality of objects. For univalent foundations, several structure/property distinctions collapse. This is a genuine scope limitation, but it is not hidden, and the paper's central comparisons within the set-theoretic scope are coherent. The reliance on prior work (ALV 2018, AENR 2023) for key equivalences is fine; those are published with independent support.\n\nThe reader's conditional verdict is fair; I might nudge soundness up slightly because the caveats are on the table and the arguments are standard. This is not a breakthrough, but it is the kind of reference that saves people from reinventing folklore.\n\nWho it is for: researchers and graduate students in categorical semantics, type theory, and related areas. I would bring it to a reading group.\n\nRecommendation: yes, send it to peer review. It deserves a serious referee; the referee should ask for proof details in the sketched places and check the diagrams, but the contribution is solid and useful.\n\nBest,","headline":"A solid, genuinely useful 2-categorical map of semantic frameworks; central claim holds up in the declared set-theoretic scope, and the paper deserves peer review.","tokens_in":23897,"tokens_out":3361,"would_cite":true,"duration_ms":31553,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["18C10","18C35","18D30","18N10"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper claims that comprehension categories — categories of contexts with a fibration of types and a comprehension operation — form a unified 2-categorical home in which almost all established categorical models of dependently-sorted…","keywords":["dependent type theory","comprehension categories","display map categories","categories with families","contextual categories","natural models","2-categories","categorical semantics"],"falsifier":"Reprove Theorems 1.16 and 2.22 in univalent foundations with univalent categories: if the displayed isomorphisms do not remain isomorphisms, or even equivalent 2-categories, then the paper's central organizing claim is foundation-dependent rather than fully categorical.","tokens_in":22830,"feed_emoji":"🧩","tokens_out":14757,"duration_ms":130610,"temperature":0.7,"pith_summary":"This paper is a map of the many categorical structures used to model algebraic theories whose sorts depend on previous sorts. It argues that most of these structures are not independent inventions but variants of a single object, the comprehension category, and it proves the translations between them. Concretely, it shows that display map categories, structured display map categories, clans, finite-limit categories, categories with attributes, categories with families, natural models, and contextual categories all embed as sub-2-categories — usually full — of the 2-category of comprehension categories. The differences between the models reduce to conditions on the fibration of types and on the comprehension functor. A sympathetic reader should care because the paper replaces scattered and partly folkloric comparisons with one reference framework and explicit equivalence, isomorphism, and adjunction results.","feed_headline":"One framework unifies nearly all dependently-sorted models","feed_subtitle":"Display map categories, clans, CwFs, natural models, and contextual categories all become sub-2-categories of it.","key_machinery":"The central object is the comprehension category, a category $C$ of contexts together with a fibration $p: T \\to C$ of types and a comprehension functor $\\chi: T \\to C^{\\to}$ that sends each type to its 'context extension' projection, lying strictly over the codomain functor and cartesian with respect to pullbacks. The paper arranges these into a 2-category with pseudo maps, which preserve context extension only up to isomorphism, plus variants with strict maps and transformations as 2-cells. The entire classification is driven by two families of conditions: conditions on the fibration (split, discrete) and conditions on the comprehension functor (full, subcategory inclusion, replete, composition-closed, trivial, contextual). The 'contextual slice' construction, which turns a comprehension category into one whose objects are finite sequences of types, relates contextual and non-contextual models. It is this parameterized structure, rather than any single theorem, that carries the argument.","core_discovery":"The central discovery is that the loose family of categorical models for dependent sorts can be organized around comprehension categories without forcing a single model on anyone. Working with the 2-category of comprehension categories and pseudo maps, the paper establishes a web of exact comparisons: display map categories appear as the sub-2-category of replete subcategorical comprehension categories, structured display map categories as the strict-map sub-2-category of subcategorical ones, clans as rooted replete composition-closed ones, finite-limit categories as rooted trivial ones, categories with attributes as discrete comprehension categories, categories with families as full split comprehension categories, and contextual categories as discrete contextual ones. Alongside these embeddings there are adjunctions such as fullification, repletion, composition closure, and the contextual-core construction. The paper is careful to separate strict maps, pseudo maps, and transformations, and it documents cases, such as structured display map categories, where pseudo and strict behaviour genuinely diverge.","pith_inferences":["Our inference: the 2-categorical embeddings imply that any 2-categorical limit, colimit, or adjunction computed in the ambient 2-category of comprehension categories restricts to the embedded models where it exists; the paper does not spell out this transfer principle, but it follows directly from the embeddings being 2-functors.","Our inference: a newly proposed semantic framework for dependent sorts can be classified by checking whether its category of models is 2-equivalent to a full sub-2-category of comprehension categories satisfying a combination of the listed conditions; this gives a cheap test for whether the framework is genuinely new or a repackaging of an existing one.","Our inference: the paper's set-theoretic strict-equality caveat suggests that, in univalent foundations, the printed isomorphisms such as $\\mathrm{sDMC} \\cong \\mathrm{CompCat}^{\\mathrm{str2}}_{\\mathrm{sub}}$ are likely to become equivalences or biequivalences rather than literal isomorphisms; re-proving the diagrams there would clarify which of the comparisons are structural and which are artifact"],"forward_implications":["Because display map categories are exactly the replete subcategorical comprehension categories, any construction or result for comprehension categories in that sub-2-category applies verbatim to display map categories.","Categories with attributes, categories with families, and natural models form a chain of 2-equivalences, so the choice among them is a matter of presentation, not mathematical content.","For contextual categories, pseudo maps and strict maps agree up to equivalence, so the 2-categorical and 1-categorical perspectives coincide for this class of models.","The adjunctions between comprehension categories and their subclasses — repletion, fullification, composition closure, and contextual core — give canonical ways to move from a coarser model to a finer one and back, which is exactly what a unified semantics of dependent type theory needs."],"supporting_citations":[{"why":"Introduces comprehension categories as a common generalisation of earlier models; the paper takes this object as its unifying language.","marker":"[Jac93]"},{"why":"Supplies the definitions of display map categories and structured display map categories used in Section 3.","marker":"[Tay99]"},{"why":"Provides the original display-map stability framework that the display map category comparison is built on.","marker":"[HP89]"},{"why":"Introduces contextual categories and categories with attributes, the primitive-types models compared in Section 4.","marker":"[Car78]"},{"why":"Introduces categories with families, whose comparison with categories with attributes and comprehension categories is Proposition 4.1.","marker":"[Dyb96]"},{"why":"Introduces natural models and their equivalence to categories with families, used in Proposition 4.3.","marker":"[Awo18]"},{"why":"Gives the earlier 1-categorical comparison of categories with attributes, contextual categories, and display map categories that the present paper extends to 2-categories.","marker":"[Bla91]"},{"why":"Provides a related 2-categorical treatment of context comprehension with lax maps, which the paper relates through Proposition 3.8.","marker":"[CE24]"}],"fun_headline_variants":["Comprehension categories unify nearly all dependent-type semantics","One 2-category hosts almost all dependently-sorted algebraic theories","The 2-category of comprehension categories subsumes nearly all models","A unifying 2-category for dependently-sorted algebraic theories"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The comparisons assume a mathematical world in which you can ask whether two objects of a category are literally equal, not merely isomorphic; in foundations where that question is not available, some of the stated isomorphisms and adjunctions must be weakened to equivalences.","fun_headline_variants_meta":{"raw":{"variants":["Comprehension categories unify nearly all dependent-type semantics","One 2-category hosts almost all dependently-sorted algebraic theories","The 2-category of comprehension categories subsumes nearly all models","A unifying 2-category for dependently-sorted algebraic theories"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000322,"raw_usage":{"total_tokens":1767,"prompt_tokens":855,"completion_tokens":912,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":471,"completion_tokens_details":{"reasoning_tokens":837}},"tokens_in":471,"tokens_out":912,"duration_ms":9797,"temperature":1.0,"reasoning_tokens":837,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T23:44:23.092161+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Reprove Theorems 1.16 and 2.22 in univalent foundations with univalent categories: if the displayed isomorphisms do not remain isomorphisms, or even equivalent 2-categories, then the paper's central organizing claim is foundation-dependent rather than fully categorical.","supporting_citations":[],"review_version":1}