{"id":"4892f382-8e14-4281-9866-f5c8a284b35c","arxiv_id":"2501.17869","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Elementary existential fibrations correspond exactly to cartesian equipments obtained via the new /BU il construction, and regular fibrations correspond to those with Beck-Chevalley pullbacks.","lead":"This thesis proposes virtual double categories as a common framework for both the semantics and the syntax of predicate logic, and proves that elementary existential fibrations are exactly the cartesian fibrations whose associated bilateral virtual double category is a cartesian equipment. If correct, it unifies the fibration-based and bicategory-based approaches to regular logic in a single double-categorical setting.","discovery_kind":"unification","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Proposition 2.3.34 only checks binary cells; the n-ary case is deferred to \"similar\" and is load-bearing for the image characterization in Corollary 2.3.37.","rationale":"Reader's weakest_assumption is exactly Proposition 2.3.34, and I agree. The central claim Theorem 2.3.14 itself—that a cartesian fibration is elementary existential iff BUil(p) is a cartesian equipment—is well supported by Lemmas 2.3.6–2.3.12 and the proof of Theorem 2.3.17, modulo the usual sketchiness of long fiber calculations. The point where the argument becomes load-bearing is the converse direction of the image theorem: to know that every Frobenius cartesian equipment is, up to equivalence, of the form BUil(p), one must be able to pass from the unilateral fibration back to the full equipment. Proposition 2.3.34 is the only place this is argued, and its proof is visibly incomplete for n-ary cells. Because Lemma 1.3.8 requires bijectivity on all frames, the missing n-ary case is not a cosmetic omission. The phrase \"the general case is similar\" might be true, but the coherence involved—associativity of the recovered loose composition, compatibility with the previously constructed equivalence—is exactly what needs checking. This does not make me think the theorem is false; it makes me think the thesis is not yet complete at this point. Hence the reader's CONDITIONAL verdict stands unchanged.","tokens_in":66832,"tokens_out":15941,"duration_ms":145068,"concrete_test":"Write out the n=3 case of Proposition 2.3.34 explicitly. For α : I×J → 1, β : J×K → 1, γ : K×L → 1 in a Frobenius cartesian equipment BW, construct the canonical bijection between ternary cells of BUil(uni(BW)) (arrows from ⋀(α[⟨0,1⟩] ∧ β[⟨1,2⟩] ∧ γ[⟨2,3⟩]) to δ[⟨0,3⟩] in the appropriate fiber) and ternary cells of C4CB(BW), and verify it is compatible with the associativity isomorphism (α⊙β)⊙γ ≅ α⊙(β⊙γ). If the two routes through binary composites give different cells, the equivalence in Proposition 2.3.34 fails; if they agree, repeat for general n by induction.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Corollary 2.3.37—that the essential image of /BU il : Fib^{×∧=∃} → Eqp_cart is exactly the Frobenius cartesian equipments—rests on Proposition 2.3.34, which claims BUil(uni(BW)) ≃ BW for every Frobenius cartesian equipment BW. The proof establishes this only for unary and binary cells and then says \"the general case is similar.\" This is not a harmless formality: Lemma 1.3.8 characterizes an equivalence in FVDbl by a bijection on all n-ary globular cells, and the n-ary cells of BUil(uni(BW)) are built from iterated conjunctions of restrictions, whereas the corresponding cells of the recovered double category C4CB(BW) use the composite of n loose arrows via the compact-closed structure. Matching these for all n requires a coherence check that the two binary decompositions of an n-ary composite agree (associativity), and that the canonical correspondence respects restriction along tight arrows. As written, the recovery of BW from uni(BW) is incomplete, so the claimed image characterization is not fully proven. The gap is probably fillable—the binary case strongly suggests the structure is right—but until the n-ary case is written out, the central equivalence is conditional.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The thesis develops a double-categorical framework for predicate logic and a type-theoretic internal language for virtual double categories. Chapter 2 constructs a 2-functor /BUil from cartesian fibrations to cartesian fibrational virtual double categories, proves that elementary existential fibrations are exactly the cartesian fibrations for which /BUil(p) is a cartesian composable FVDC (Theorem 2.3.14, restated as a pullback in Theorem 2.3.17), and proposes to identify the essential image of /BUil on elementary existential fibrations with Frobenius cartesian equipments (Corollary 2.3.37). It also proves that the loose bicategory of a cartesian equipment is a cartesian bicategory (Theorem 2.4.8) and translates comprehension, extensionality, and choice principles into double-categorical terms. Chapter 3 introduces the type theory FVDblTT and states a syntax-semantics biadjunction for cartesian fibrational virtual double categories.","tokens_in":67086,"tokens_out":6982,"duration_ms":65213,"significance":"If the central theorems are fully established, the paper gives a clean double-categorical home for regular logic: equality and existential quantification become units and composition in a cartesian equipment, and the Beck-Chevalley and Frobenius conditions are absorbed into the cartesian structure of a double category. The /BUil construction and the systematic comparison with allegories, cartesian bicategories, and relational doctrines are valuable and well placed in the literature. The author is explicit about provenance: tools from [HN23] are cited, the overlap of Chapter 3 with [Nas24] is disclosed, and the relation to Shulman's /BYr construction and to [Pat24b] is acknowledged. The thesis also contains a large amount of explicit diagrammatic reasoning and a useful overview diagram (Figure 1). The main caveat is that the image characterization in Corollary 2.3.37 rests on an n-ary verification that is not written out.","major_comments":[{"comment":"The proof of Proposition 2.3.34 establishes the equivalence /BUil(uni(/BW)) ≃ /BW only for unary and binary cells and then states \"the general case is similar.\" This is load-bearing for Corollary 2.3.37, since Lemma 1.3.8 requires a bijection on all n-ary globular cells. For n ≥ 3 the top loose arrow of a cell in /BUil(uni(/BW)) is built from iterated binary conjunctions of restrictions, whereas the corresponding cell of /C4CB(/BW) uses the composite of n loose arrows through the compact-closed structure. The missing verification includes an associativity coherence for the two binary decompositions of an n-ary composite and compatibility with restriction along tight arrows. As written, the recovery of /BW from uni(/BW) is incomplete, so the image characterization in Corollary 2.3.37 is not fully proved; the gap appears fillable, but it must be written out.","section":"2.3.3, Proposition 2.3.34"},{"comment":"Proposition 2.3.36 is only a sketch: it says that preservation of the relevant structures \"ensures\" pseudo-naturality. Corollary 2.3.37 then uses this to conclude that /BUil is locally an equivalence with inverse uni. To support the 2-categorical claim, the naturality isomorphisms on 1-cells and the compatibility with 2-cells need to be specified, or the statement should be weakened to an object-level bijection that is not claimed to be 2-natural. This is a second load-bearing point in the image theorem.","section":"2.3.3, Proposition 2.3.36 and Corollary 2.3.37"}],"minor_comments":[{"comment":"Several cross-references appear to be self-referential: the proof of Proposition 2.3.7 says \"Considering Proposition 2.3.7\", the proof of Proposition 2.3.10 says \"we consult Proposition 2.3.10 instead\", and Remark 2.3.20 says \"Owing to Remark 2.3.20\"; these presumably should refer to the corresponding propositions on unital and composable FVDCs in Section 1.4.","section":"2.3.1, proofs of Propositions 2.3.7 and 2.3.10"},{"comment":"There are minor typos: \"prodcut projection\" in the proof of Lemma 2.3.9 should be \"product projection\", and \"follws\" in Definition 2.5.2 should be \"follows\".","section":"2.3.1, Lemma 2.3.9 and Section 2.5.1"},{"comment":"In the proof of Lemma 2.3.35, the assertion that Fib×∧=∃ → BiFib is fully faithful is attributed to \"Lemma 2.3.35\" but should refer to Lemma 2.2.19.","section":"2.3.3, proof of Lemma 2.3.35"},{"comment":"The proof of Proposition 1.4.3 is given only as a sketch; since the paper later uses the biequivalence between composable FVDCs and equipments, a precise pointer to the statement in [Her00] with the required hypotheses would be helpful.","section":"1.4, Proposition 1.4.3 and Remark 1.4.4"},{"comment":"In the proof of Theorem 2.4.8, condition (iii) is justified by saying that the laxity cells are \"confirmed to be the same\" as the cells derived from the universal properties, without displaying the verification; a diagrammatic or equational check should be added or referenced.","section":"2.4.2, Theorem 2.4.8"},{"comment":"The decomposition of the displayed pullback square into six pullback squares is described only in words; listing the actual squares would make the Beck-Chevalley argument easier to check.","section":"2.3.3, Proposition 2.3.28"}],"recommendation":"major_revision","confidential_remarks":"The main technical risk is the n-ary case of Proposition 2.3.34. It is likely fixable, and the paper's scope and contributions are appropriate for the journal, so I would encourage a revision that supplies the missing coherence check and the pseudo-naturality data rather than a rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's the quick take: this is a real contribution to double-categorical logic, not a repackaging. The BUil construction and Theorem 2.3.14 — a cartesian fibration is elementary existential iff its bilateral VDC is a cartesian equipment — is the kind of unifying statement that makes the framework worth taking seriously. The proof is mostly detailed and honest about what it delegates. The comparison sections (allegories, cartesian bicategories, relational doctrines) and the translation of comprehension/extensionality into tabulators/unit-pureness are genuinely useful.\n\nThe soft spot the reader's report flags is real and load-bearing. Proposition 2.3.34 is what gives Corollary 2.3.37, the claim that the essential image of BUil is exactly the Frobenius cartesian equipments. The proof only works the binary-cell case and says the general case is similar. That's not a harmless ellipsis: the n-ary cells of BUil(uni(BW)) are built from iterated conjunctions of restrictions, while the corresponding cells in the recovered double category use the composite of n loose arrows through the compact-closed structure. Matching them for all n requires a coherence check (associativity of the two binary decompositions, compatibility with restriction). The binary case strongly suggests the structure is right, and the gap is probably fillable, but as written the image characterization is conditional. Claim 2.3.18 is also postponed to the end of the theorem, which makes Theorem 2.3.14's proof harder to check than it needs to be. There are also cross-reference slips (Remark 2.3.20 references itself; several proposition references are off by one). These are minor.\n\nTheorem 2.4.8 is honestly flagged as already proved in Pat24b; the alternative proof is fine but not novel. The type theory chapter overlaps heavily with the author's own Nas24 preprint, and the disclosure is explicit, so the self-citation is not a problem; but a referee should check what this chapter adds beyond the preprint.\n\nWho benefits: anyone working in categorical logic, fibred category theory, or double categories. It deserves a serious referee. My recommendation: send it out, but require the n-ary case of Prop 2.3.34 to be written out (or the proof of Cor 2.3.37 adjusted) before acceptance. The central theorem is likely correct; the missing coherence check is the difference between conditional and proven.","headline":"A substantive double-categorical semantics for regular logic with a genuinely load-bearing gap in the image characterization; worth refereeing, but the n-ary cell proof needs to be written out.","tokens_in":67647,"tokens_out":2440,"would_cite":true,"duration_ms":23473,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["18N10","03G30","18A05"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper's central theorem makes a cartesian fibration model regular logic exactly when its bilateral virtual double category is a cartesian equipment.","keywords":["virtual double categories","regular logic","cartesian fibrations","elementary existential fibrations","Frobenius cartesian equipments","categorical logic","type theory","Beck-Chevalley condition"],"falsifier":"Produce a Frobenius cartesian equipment, for example the cartesian equipment of spans or profunctors, and explicitly check triples of loose arrows in $\\mathbb{Bil}(\\mathrm{uni}(\\mathbb{B}))$: if some 3-ary virtual cell fails to correspond uniquely to the composite in $\\mathbb{B}$, then the claimed equivalence of Proposition 2.3.34 fails for that example. The check is a finite string-diagram calculation inside the chosen equipment.","tokens_in":66611,"feed_emoji":"🔗","tokens_out":7234,"duration_ms":77346,"temperature":0.7,"pith_summary":"This thesis argues that virtual double categories are the right common home for the syntax and semantics of predicate logic. Its central claim is that a cartesian fibration interprets regular logic—equality, conjunction, and existential quantification—exactly when the bilateral virtual double category $\\mathbb{Bil}(p)$ built from it is a cartesian composable fibrational virtual double category, i.e., a cartesian equipment. Equality and the existential quantifier are not ad hoc adjunctions imposed on the fibration; they emerge as units and composition of loose arrows in the induced double category. The thesis also characterizes the image of the construction as the Frobenius cartesian equipments and develops a type theory, FVDblTT, as an internal language for virtual double categories. If correct, this unifies fibration-based categorical logic, bicategorical logic, and double-categorical logic in one framework.","feed_headline":"Regular logic is exactly when relations compose in a cartesian equipment","feed_subtitle":"Fibrations for regular logic are exactly those whose induced virtual double category composes its relations.","key_machinery":"The load-bearing construction is the bilateral virtual double category $\\mathbb{Bil}(p)$, together with its one-sided inverse $\\mathrm{uni}(\\mathbb{B})$. A loose arrow $I \\to J$ is an object of the fiber over $I\\times J$, so it is a binary predicate with two distinguished contexts, and an $n$-ary cell is a proof of a Horn consequence. Restrictions are induced by base change, local finite products come from fiberwise finite products, and—when the fibration is elementary existential—the units and composites of loose arrows are produced by the left adjoints $\\sum_{\\langle 0,0\\rangle}$ and $\\sum_{\\langle 0,2\\rangle}$, which are precisely equality and existential quantification. The universal properties of those loose compositions force the Beck-Chevalley and Frobenius conditions; in the converse direction, the sandwich lemma and Beck-Chevalley pullbacks in cartesian equipments reconstruct those conditions from the double category. The Frobenius axiom on a cartesian equipment supplies the self-duality that lets $\\mathrm{uni}(\\mathbb{B})$ recover the whole equipment from only one side of its cells.","core_discovery":"The core claim is Theorem 2.3.14: for a cartesian fibration $p$, the virtual double category $\\mathbb{Bil}(p)$ is a cartesian composable FVDC—equivalently a cartesian equipment—if and only if $p$ is an elementary existential fibration. In $\\mathbb{Bil}(p)$, tight arrows are the arrows of the base category, and loose arrows from $I$ to $J$ are objects of the fiber over $I\\times J$, viewed as bilateral predicates; an $n$-ary cell records a proof of a Horn-style entailment $\\alpha_1,\\dots,\\alpha_n \\vdash \\beta[s,t]$. Reindexing along a pair of tight arrows is restriction of predicates, the unit loose arrow on $I$ is constructed from the left adjoint to reindexing along the diagonal $I\\to I\\times I$, and composability of loose arrows is constructed from left adjoints along product projections. The paper further shows that the essential image of $\\mathbb{Bil}$ on elementary existential fibrations is exactly the Frobenius cartesian equipments, with the unilateral fibration construction $\\mathrm{uni}$ as a two-sided inverse up to equivalence. The result gives a double-categorical reformulation of the classical correspondence between regular logic and fibrations in which relations can be composed.","pith_inferences":["If Theorem 2.3.14 is read as a completeness statement, the same $\\mathbb{Bil}$ construction should classify other logical fragments: restricting which left adjoints exist in the fibration should correspond exactly to restricting which loose composites exist in the virtual double category, yielding a graded ladder from cartesian logic to regular logic.","The characterization of the image as Frobenius cartesian equipments suggests that the Frobenius axiom, rather than a technical convenience, is what makes a category of relations recoverable as an equipment; one could test this by showing that the unilateral fibration of a non-Frobenius cartesian equipment such as the equipment of profunctors provably fails to determine the omitted composition.","FVDblTT could be extended to an internal language for elementary existential fibrations by adding equality and existential constructors corresponding to units and composites of loose arrows, making the syntax-semantics correspondence proof-relevant."],"forward_implications":["A cartesian fibration models regular logic exactly when its induced virtual double category composes its loose arrows, so the passage from virtual to composable models is the logical passage from finite-product logic to regular logic.","The construction reproduces the classical examples: subobject fibrations yield double categories of relations, codomain fibrations yield double categories of spans, and family fibrations yield matrix double categories, with regularity of the base category equivalent to composability.","Frobenius cartesian equipments are exactly the equipments recoverable from their unilateral fibrations, giving a double-categorical analogue of the duality between fibrations and bicategories of relations.","The loose bicategory of every cartesian equipment is a cartesian bicategory, so cartesian equipments generalize cartesian bicategories while retaining tight arrows as genuine functions.","FVDblTT provides a syntax-semantics adjunction for virtual double categories, so proofs in the type theory correspond to cells in the semantics."],"supporting_citations":[{"why":"Supplies the equipment technology of companions, conjoints, prone and supine cells, and the prior construction of framed bicategories from fibrations that $\\mathbb{Bil}$ generalizes.","marker":"[Shu08]"},{"why":"Supplies the sandwich lemma, Beck-Chevalley pullbacks, and double categories of relations used throughout the proof of Theorem 2.3.14 and its corollaries.","marker":"[HN23]"},{"why":"Supplies the characterization of cartesian double categories and cartesian equipments used to identify when $\\mathbb{Bil}(p)$ is a cartesian composable FVDC.","marker":"[Ale18]"},{"why":"Supplies the standard definitions of elementary, existential, and regular fibrations as models of logical fragments, the notions being characterized by the double-categorical conditions.","marker":"[Jac99]"},{"why":"Supplies the functorial choice of pullback squares $\\Phi_=$ and the definition of elementary fibration used in the proof.","marker":"[EPR22]"},{"why":"Supplies the notion of virtual double category, restrictions, and composability of loose arrows, which form the ambient framework of the $\\mathbb{Bil}$ construction.","marker":"[CS10]"},{"why":"Supplies the path double category and composite universal properties for virtual double categories, used in the composability conditions.","marker":"[DPP06]"}],"fun_headline_variants":["Regular logic is exactly composable relations in cartesian equipment","Cartesian equipments characterize regular logic via fibrations","Virtual double categories unify syntax and semantics for logic","Cartesian equipment theorem links regular logic and fibrations"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The recovery theorem assumes that the equivalence between a Frobenius cartesian equipment and its bilateral reconstruction from the unilateral fibration, proved for two-arrow cells, automatically holds for cells of every arity; the paper leaves the general case to 'similar' reasoning.","fun_headline_variants_meta":{"raw":{"variants":["Regular logic is exactly composable relations in cartesian equipment","Cartesian equipments characterize regular logic via fibrations","Virtual double categories unify syntax and semantics for logic","Cartesian equipment theorem links regular logic and fibrations"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00077,"raw_usage":{"total_tokens":3391,"prompt_tokens":908,"completion_tokens":2483,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":524,"completion_tokens_details":{"reasoning_tokens":2431}},"tokens_in":524,"tokens_out":2483,"duration_ms":19309,"temperature":1.0,"reasoning_tokens":2431,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T20:20:18.338718+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Produce a Frobenius cartesian equipment, for example the cartesian equipment of spans or profunctors, and explicitly check triples of loose arrows in $\\mathbb{Bil}(\\mathrm{uni}(\\mathbb{B}))$: if some 3-ary virtual cell fails to correspond uniquely to the composite in $\\mathbb{B}$, then the claimed equivalence of Proposition 2.3.34 fails for that example. The check is a finite string-diagram calculation inside the chosen equipment.","supporting_citations":[],"review_version":1}