{"id":"10c402b7-ac18-4f85-9771-9dc80e2e4ee4","arxiv_id":"2412.11295","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A new categorical framework, relational doctrines, yields universal quotient and extensionality completions that unify exact completion, setoids, and quantitative metric quotients.","lead":"The paper introduces relational doctrines, a categorical framework for the calculus of relations, and builds universal constructions that add quotients and extensional equality. It shows these constructions unify classical quotient completions with quantitative versions over metric spaces and matrices, and characterize the resulting doctrines through projective covers.","discovery_kind":"unification","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified: Proposition 2.4 is correctly proved, and the projective-cover characterization (Corollary 6.8) is internally coherent; the main residual risk is lack of formal verification, not a specific flaw.","rationale":"I examined the paper in good faith, focusing on the central claim that the essential image of the extensional quotient completion is characterized by projective covers, and on the reader's flagged weakest assumption, Proposition 2.4. The proof of Proposition 2.4 is a short, valid derivation from the relational doctrine axioms; I verified each inequality and found no missing hypothesis. The uses of this proposition in Proposition 4.2, in quotient uniqueness, and in Theorem 6.7 are legitimate and do not make the framework fragile in the way the reader suggested. I also traced the main steps of Theorem 6.7 and Corollary 6.8: the forward direction uses the pseudo-inverse to transfer projectivity from (S)eq via Corollary 6.4, and the reverse direction constructs a pseudoinverse using chosen quotient presentations and the fullness of \\hat{F}; the argument is standard and internally consistent. Similarly, the 2-monadicity results are supported by explicit KZ identities and reflection adjunctions, and the examples are coherent. The paper is not machine-checked and has frequent typos, and Theorem 6.11 depends on an external result in [46] about the algebra doctrine having quotients; these are legitimate reasons for a conditional verdict, but they are not a specific load-bearing flaw that I can point to inside the argument. Therefore I find no significant objection, and the reader's conditional verdict can remain unchanged without altering its basis.","tokens_in":50941,"tokens_out":30171,"duration_ms":279631,"concrete_test":"Formalize Definition 2.1 and Propositions 2.4, 4.2, and Corollary 6.8 in a proof assistant such as Lean's mathlib or Coq's UniMath, and independently re-derive the construction of the pseudoinverse G in Theorem 6.7; if all definitions and proofs check without additional axioms, the central claim stands, while any failure would pinpoint the exact unsupported step.","verdict_should_be":"UNCHANGED","load_bearing_attack":"After checking the argument, I do not find a load-bearing correctness gap. The reader's candidate weakest assumption, Proposition 2.4, is valid: the proof uses totality of α to get β = d_X;β ≤ α;α^⊥;β, uses α≤β to get α^⊥≤β^⊥, and uses functionality of β to get α^⊥;β≤β^⊥;β≤d_Y, hence β≤α; the reverse inequality is symmetric. This discreteness is applied in Proposition 4.2, in quotient uniqueness, and in Theorem 6.7; none of these uses introduces a hidden axiom or a circular step. The essential-image characterization in Theorem 6.7/Corollary 6.8 is a standard enough-projectives argument: the forward direction constructs an inverse from chosen quotient presentations, and the backward direction shows the image objects are projective via Corollary 6.4. The 2-monadicity claims are supported by the stated KZ conditions and the 2-adjunction lemmas. The main residual risks are that the proofs are long, unformalized, and contain many typos, and that Theorem 6.11 relies on the cited companion paper [46] for the claim that the algebra doctrine RT is extensional and has quotients. These are verification risks rather than identified contradictions.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces relational doctrines as a functorial, variable-free description of a core fragment of the calculus of relations: a functor R:(C×C)^op→Pos equipped with relational identities, composition, and converse satisfying the usual unit/associativity/involution axioms. On this basis it defines R-equivalence relations, quotient arrows, effective descent quotients, extensional equality, and two free constructions: the intensional quotient completion (R)q and the extensional collapse (R)e, whose composite is the extensional quotient completion (R)eq. The main theorems assert 2-adjointness and 2-monadicity for these constructions (Theorems 3.15, 3.21, 4.7, 5.2), characterize the essential image of the extensional quotient completion through projective covers (Theorem 6.7 and Corollary 6.8), and apply this to show that, under suitable hypotheses, relational doctrines of algebras for a monad arise as the extensional quotient completion of their restriction to free algebras (Theorems 6.11 and 6.13). Section 7 compares relational doctrines with ordered categories with involution and with existential elementary doctrines.","tokens_in":51160,"tokens_out":15573,"duration_ms":150869,"significance":"If the results are correct, this is a valuable unifying framework: it subsumes the elementary quotient completion of Maietti and Rosolini, it supplies quantitative examples such as metric spaces and semi-normed vector spaces, and it gives a clean categorical account of when quotients and extensionality are 'property-like' structures via lax idempotent 2-monads. The constructions are natural and the proofs are largely detailed and definition-driven; the projective-cover characterization is a conceptually satisfying analogue of the exact-completion story. The skeptical concern about Proposition 2.4 does not, on my reading, land: the proof is correct, and the discreteness of functional-total relations is used legitimately in Proposition 4.2, in quotient uniqueness, and in Theorem 6.7. The main residual risks are (i) the paper is not fully self-contained for a load-bearing fact about Eilenberg-Moore doctrines, and (ii) one comparison example contains an unjustified preservation claim. Neither issue points to an internal inconsistency in the central construction, but both need attention before publication.","major_comments":[{"comment":"The sentence 'One can prove that RT is extensional and has quotients (see [46])' delegates a load-bearing fact for Theorem 6.11 and for the 'main result' paragraph that follows it. Since the rest of the paper proves its central claims from Definition 2.1, please add a proof, or at least a precise statement with a numbered theorem from [46], and clarify the status of [46] if it is a companion preprint. This is a self-containedness issue rather than a criticism of the cited result, but it is load-bearing for the algebra-doctrine application.","section":"Section 6, before Theorem 6.11"},{"comment":"The proof that the forgetful functor U:C^T→C extends to a 1-arrow JSpn_U in EQRD says that U, 'being a right adjoint, preserves coequalizers of equivalence relations.' Right adjoints preserve limits, not colimits, and this preservation is not automatic for monadic forgetful functors. Since the example is the advertised recovery of Vitale's result in [32], this needs a proof or an explicit appeal to a theorem with the right hypotheses. The issue does not affect Theorems 6.11 or 6.13 themselves, but it does affect a claim presented as a consequence.","section":"Section 6, Example 6.14"}],"minor_comments":[{"comment":"The manuscript contains many typographical errors and malformed phrases, including 'Furthremore', '2-mondic', 'relaitonal identity', 'saty', 'efective', 'descente', 'sujective', 'well-defind', 'costruction', 'doctirne', and 'Furthre'. A systematic proofreading pass is needed before publication; I do not list every instance.","section":"Throughout"},{"comment":"The assertion that the 2-monads Tq, Te, and Teq restrict to the cartesian modular doctrines and that the completions coincide with the elementary quotient completion is stated without proof. Please add a proof or a precise reference to a theorem in the existing literature.","section":"Section 7, after Theorem 7.20"},{"comment":"The claim that applying the extensional collapse to QTRel gives exactly the category of equilogical spaces is stated without argument. A short proof or a precise citation would make the example self-contained.","section":"Section 4, Example 4.6"},{"comment":"The symbol Q is used both for the quotient-completion 2-functor and for the chosen reflection left adjoint (S)q→S. Renaming one of these would considerably improve readability.","section":"Lemma 3.12 and Theorem 3.15"},{"comment":"The phrase 'all relational operations are lax natural transformations' is informal: the intended inequalities are clear from the displayed axioms, but a sentence saying in exactly which sense the identity and composition are lax (and the converse is strict) would help the reader.","section":"Section 2, Definition 2.1"}],"recommendation":"major_revision","confidential_remarks":"The paper is a substantial extension of the authors' FSCD 2023 paper. My main concerns are the self-containedness of Theorem 6.11 via [46] and the unjustified preservation claim in Example 6.14. If the authors add the missing proof or make the dependence on [46] precise, and correct or carefully rephrase Example 6.14, I would be happy to recommend acceptance. The editor may also wish to verify the publication status of [46] and the amount of overlap with [34]."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The short version: this is a real and substantial paper. It introduces relational doctrines as a variable-free model of the calculus of relations, then builds the intensional quotient completion, the extensional collapse, and the extensional quotient completion, proving 2-monadicity and a projective-cover characterization. The metric, matrix, and seminormed examples are not decoration—they show the framework does something the older doctrine-based quotient completions cannot. The comparison with ordered categories with involution and with existential elementary doctrines is also well done and gives the paper useful context.\n\nI checked the candidate weak point the reader flagged, Proposition 2.4, and it is fine. The discreteness of functional-and-total relations follows from the axioms as written; the uses in Proposition 4.2 and in quotient uniqueness are legitimate. The projective-cover characterization in Theorem 6.7/Corollary 6.8 is a standard enough-projectives argument and appears internally coherent. The stress-test note is right: I do not see a load-bearing gap.\n\nThe soft spots are real but proportionate. The proofs are long, entirely unformalized, and the text is full of typos and abbreviated steps; a referee will need patience. Theorem 6.11 relies on the companion paper [46] for the claim that the algebra doctrine RT is extensional and has quotients, and that is the one place where the present paper is not self-contained. The authors also honestly list the absence of a syntax and the incomplete comparison with linear doctrines as open limitations. The self-citation to their FSCD 2023 paper is appropriate—this is explicitly the extended version, and the new material is genuinely new.\n\nWho should read this: categorical logicians and people who work on quotient completions, setoids, exact completion, and quantitative semantics. It deserves a serious referee and, assuming the referee checks the reliance on [46] and tolerates the typos, it should appear in a good journal.\n\nMy recommendation: send it to review. It is not desk-reject material, and the central claims are credible enough to justify referee time.","headline":"A solid, genuinely new categorical-logic paper: the constructions and main theorems hold up, and the main risks are proof-length and typo-level, not load-bearing correctness.","tokens_in":51723,"tokens_out":1510,"would_cite":true,"duration_ms":18291,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["18B10","18C20","18D05","03G30"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper claims that quotients, classical or metric, are instances of one universal construction—the extensional quotient completion—whose outputs are exactly the extensional relational doctrines with quotients and enough projective…","keywords":["calculus of relations","relational doctrine","quotient completion","extensional equality","projective cover","2-monad","quantitative equality","monad algebras"],"falsifier":"Look for a pair of distinct functional and total relations in a concrete relational doctrine such as $\\mathcal{V}$-$\\mathbf{Rel}$ with $\\mathcal{V}$ the quantale $[0,\\infty]$ under the reverse order; Proposition 2.4 predicts no such pair exists, and exhibiting one would break the identification of $R$-equality with graph equality on which the extensional collapse and Corollary 6.8 rest.","tokens_in":50692,"feed_emoji":"📏","tokens_out":13619,"duration_ms":116918,"temperature":0.7,"pith_summary":"Taking a quotient means changing the notion of equality on an object, and in quantitative settings equality becomes a distance; this paper gives a single categorical framework in which both kinds of quotient are the same operation. It introduces relational doctrines, a functorial version of the calculus of relations, and builds two universal completions on them: an intensional quotient completion that freely adds quotients, and an extensional collapse that forces relationally indistinguishable arrows to be equal. Their composite, the extensional quotient completion, is the paper's central object: Corollary 6.8 characterizes its essential image as exactly the extensional relational doctrines with quotients that admit a projective cover, and Theorem 6.11 shows that doctrines of algebras for quotient-preserving monads arise as such completions of free algebras. If the paper is right, the standard quotient-completion technology transfers to quantitative examples—pseudometric spaces, seminormed vector spaces, bisimulations—where the usual doctrine-based approach fails.","feed_headline":"One construction makes metric and classical quotients the same","feed_subtitle":"It covers pseudometric spaces, bisimulations, and monad algebras from one principle.","key_machinery":"The carrying object is a relational doctrine: a functor $R:(\\mathcal{C}\\times\\mathcal{C})^{\\mathrm{op}}\\to \\mathbf{Pos}$ equipped with an identity relation $d_X$, relational composition $;$, and converse $(-)^{\\perp}$ satisfying the laws of the calculus of relations, whose arrows $f$ are represented by graphs $\\Gamma_f=R_{f,\\mathrm{id}_Y}(d_Y)$. The argument runs through two named constructions. The intensional quotient completion $(R)_q$ has as objects pairs $\\langle X,\\rho\\rangle$ with $\\rho$ an $R$-equivalence relation and as relations the descent data $\\alpha$ with $\\rho^{\\perp};\\alpha;\\sigma\\leq \\alpha$, making every object $\\langle X,\\rho\\rangle$ a quotient of $\\langle X,d_X\\rangle$. The extensional collapse $(R)_e$ instead quotients the base category by $R$-equality $f\\approx g$, defined by $\\Gamma_f=\\Gamma_g$. Their composite $(R)_{eq}$ is the extensional quotient completion; its essential image is characterized by $R$-projective objects, those $P$ for which every arrow $P\\to Y$ lifts through every quotient arrow $q:X\\to Y$, and by projective covers, full subcategories from which every object is reached by a quotient arrow.","core_discovery":"The central claim is that quotients in a relational doctrine are nothing but a change of the identity relation, and that two universal constructions compose to make this precise. First, the intensional quotient completion $(R)_q$ freely adds an effective descent quotient to every $R$-equivalence relation, generalizing the elementary quotient completion and producing, for example, the category of $\\mathcal{V}$-metric spaces from $\\mathcal{V}$-relations and semi-normed vector spaces from the vector-space doctrine. Second, the extensional collapse $(R)_e$ divides out $R$-equality—two parallel arrows are identified exactly when their relational graphs are equal—which abstracts separation in metric and topological settings. The composite $(R)_{eq}$ is the extensional quotient completion, and the paper's main structural results are that it is a lax idempotent 2-monadic construction, that an extensional relational doctrine with quotients is equivalent to $(I^\\star_G R)_{eq}$ for a full subcategory $G$ if and only if $G$ is an $R$-projective cover, and that for a quotient-preserving monad the doctrine of algebras is the extensional quotient completion of its restriction to free algebras.","pith_inferences":["The projective-cover description suggests a general recipe for recognizing completions in other doctrines: whenever a base category is generated by a class of projective objects under a monad-preserved quotient operation, the associated algebra doctrine should be a completion of the free-algebra subcategory; this is testable for comonads and for lax extensions that do not preserve quotients.","Reading the extensional collapse as point-free separation, the construction offers a uniform 'Hausdorffization' across pseudometric spaces, seminormed spaces, and topological spaces; one could apply the same collapse to other concrete categories whose forgetful functor defines a relational doctrine.","The authors flag the rule of unique choice and Cauchy completeness as future work; a quantitative version of the rule would make the projective-cover theorem interact with completeness, potentially yielding a quantitative counterpart of the tripos-to-topos construction."],"forward_implications":["The classical setoid construction and the exact completion of a weakly lex category are recovered as instances of the extensional quotient completion applied to set-theoretic relations and to span doctrines.","Quantitative quotients become first-class: quotient completion of $\\mathcal{V}$-relations yields $\\mathcal{V}$-metric spaces, and the vector-space doctrine yields semi-normed vector spaces, with the extensional collapse turning pseudometrics into metrics.","For any quotient-preserving monad on an extensional relational doctrine with quotients and a projective cover, the doctrine of algebras is the extensional quotient completion of the restriction to free algebras.","Having quotients and being extensional are properties, not structures: the associated 2-monads are lax idempotent, so any compatible algebra structure is essentially unique.","Relational doctrines with a projective cover are exactly, up to equivalence, the essential image of the extensional quotient completion."],"supporting_citations":[{"why":"This pair defines the elementary quotient completion that the intensional quotient completion generalizes and is compared with throughout the paper.","marker":"[5, 6]"},{"why":"The exact completion of a weakly lex category supplies the classical projective-cover characterization that Theorem 6.7 extends to relational doctrines.","marker":"[3, 4]"},{"why":"This reference introduces metric spaces as generalized equality and supplies the motivating quantitative example of pseudometrics.","marker":"[7]"},{"why":"This work explains why ordinary predicate-logic doctrines fail to capture quantitative equality, motivating the move to relational doctrines.","marker":"[16]"},{"why":"These are the classical sources for the calculus of relations whose core operations relational doctrines axiomatize.","marker":"[17, 18, 19]"},{"why":"This result characterizes monadic categories over sets via free algebras and is the direct precedent for Theorem 6.11.","marker":"[32]"},{"why":"Ordered categories with involution are the comparison class for Section 7.1 and the rule of unique choice.","marker":"[33]"},{"why":"Allegories supply the modular law and its regular-logic proof used in Theorem 7.20.","marker":"[49]"}],"fun_headline_variants":["Quotients unified via relational doctrines","Metric and set quotients now one construction","One construction to unify every quotient","Relational doctrines make quotients universal","Extensional quotient completion: the key"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is Proposition 2.4: in a relational doctrine, two functional and total relations that are ordered are actually equal; this discreteness is what forces $R$-equality of arrows to coincide with equality of graphs and guarantees uniqueness of quotient mediators, so if it failed the extensional collapse and the projective-cover characterization would identify the wrong arrows.","fun_headline_variants_meta":{"raw":{"variants":["Quotients unified via relational doctrines","Metric and set quotients now one construction","One construction to unify every quotient","Relational doctrines make quotients universal","Extensional quotient completion: the key"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000259,"raw_usage":{"total_tokens":1619,"prompt_tokens":1015,"completion_tokens":604,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":631,"completion_tokens_details":{"reasoning_tokens":555}},"tokens_in":631,"tokens_out":604,"duration_ms":5619,"temperature":1.0,"reasoning_tokens":555,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T15:05:07.340152+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Look for a pair of distinct functional and total relations in a concrete relational doctrine such as $\\mathcal{V}$-$\\mathbf{Rel}$ with $\\mathcal{V}$ the quantale $[0,\\infty]$ under the reverse order; Proposition 2.4 predicts no such pair exists, and exhibiting one would break the identification of $R$-equality with graph equality on which the extensional collapse and Corollary 6.8 rest.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"This reference introduces metric spaces as generalized equality and supplies the motivating quantitative example of pseudometrics."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"This result characterizes monadic categories over sets via free algebras and is the direct precedent for Theorem 6.11."},{"cited_title":"Lambek, Diagram chasing in ordered categories with involu- tion, Journal of Pure and Applied Algebra 143 (1) (1999) 293–307","cited_arxiv_id":null,"evidence_quote":"Ordered categories with involution are the comparison class for Section 7.1 and the rule of unique choice."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Allegories supply the modular law and its regular-logic proof used in Theorem 7.20."}],"review_version":1}