Pith. sign in

REVIEW 2 major objections 5 minor 1 cited by

The Relational Quotient Completion

T0 review · 2 major / 5 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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…

desk verdict 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. read the letter →

arxiv 2412.11295 v1 pith:BA7X3QE3 submitted 2024-12-15 math.CT cs.LOmath.LO

Francesco Dagnino , Fabio Pasquali This is my paper · ORCID
classification math.CTcs.LOmath.LO MSC 18B1018C2018D0503G30
keywords calculusofrelationsrelationaldoctrinequotientcompletionextensionalequalityprojectivecover2-monadquantitativemonadalgebras
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 5 minor

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.

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 (2)
  1. [Section 6, before Theorem 6.11] 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.
  2. [Section 6, Example 6.14] 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.
minor comments (5)
  1. [Throughout] 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.
  2. [Section 7, after Theorem 7.20] 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.
  3. [Section 4, Example 4.6] 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.
  4. [Lemma 3.12 and Theorem 3.15] 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.
  5. [Section 2, Definition 2.1] 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.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the main theorems are proved from the definitions; the only dependency worth noting is a companion-paper result for Eilenberg-Moore doctrines, which is a verification matter rather than a circular reduction.

full rationale

The derivation chain is self-contained for the central results. Proposition 2.4 is proved directly from the relational-doctrine axioms: totality of alpha gives d_X <= alpha;alpha^bot, monotonicity of converse and functionality of beta give alpha^bot;beta <= beta^bot;beta <= d_Y, hence beta <= alpha, and symmetrically alpha <= beta. This discreteness is used in Proposition 4.2, in quotient uniqueness arguments, and in Theorem 6.7, but always as a proved lemma, not as an imported assumption. The quotient completion (Section 3) and extensional collapse (Section 4) are free constructions: their universal properties are established via explicit 2-adjunctions (Theorems 3.15, 3.19, 4.7, 5.1) and monadicity (3.21, 4.8, 5.2), rather than by fitting parameters to the examples they are supposed to explain. Theorem 6.7 and Corollary 6.8 characterize the essential image of the extensional quotient completion by projective covers; the reverse direction constructs a pseudoinverse explicitly using projectivity, fullness of the inclusion, and quotient universal properties, so the characterization is not a restatement of the definition. Theorem 6.11 is an application of Corollary 6.8: it verifies that free algebras form a projective cover and that the counit components are quotient arrows, using Proposition 6.10. The only external dependency is the companion paper [46] for the technical fact that Eilenberg-Moore relational doctrines are extensional and have quotients; this is a separate, checkable proof rather than an equation that reduces the theorem to its own conclusion, so it is a verification risk, not circularity. No fitted inputs are renamed as predictions, and no uniqueness theorem is imported from the authors' prior work to force the construction.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

Pure category theory paper; no numeric parameters fitted to data. The content rests on the definition of relational doctrine, standard 2-categorical machinery, and in some examples the axiom of choice. No empirical entities are postulated; the new structures are mathematical definitions, not entities requiring independent evidence.

assumptions (5)
  • standard math Standard 2-category theory background: lax 2-adjunctions, 2-monads, lax idempotent monads, idempotent monads, Eilenberg-Moore objects.
    Used throughout Sections 3, 5, 6; cited to [25,28,29,30] without proof.
  • domain assumption Definition 2.1: a relational doctrine is a functor R:(C×C)^op→Pos with identity, composition and converse satisfying stated lax naturality axioms and equations.
    This is the new primitive notion of the paper; it is not derived from prior notions and the whole theory rests on its adequacy.
  • domain assumption The quotient arrow notion (Definition 3.2) requires uniqueness of the mediating arrow; the paper assumes this universal property is well-defined in arbitrary relational doctrines.
    Part of the definition; if uniqueness failed, the completions would not be universal.
  • domain assumption In Section 6, the theory assumes existence of chosen quotient arrows and, in Theorem 6.13, that every R-surjective arrow splits.
    Explicit assumptions used to prove projective cover characterizations and the algebras application.
  • domain assumption The Axiom of Choice is invoked in several examples (4.5(1), 6.2(1,2), 6.14) to provide sections of surjections.
    The authors flag these uses; not needed for the general universal constructions but needed for the concrete metric and topological examples.

how reviews work

0 comments
Cite this review

Pith. "Pith review of The Relational Quotient Completion." pith.science (2026). https://pith.science/paper/BA7X3QE3

@misc{pith2026241211295,
  author       = {Pith},
  title        = {Pith review of: The Relational Quotient Completion},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/BA7X3QE3}},
  note         = {Machine review of arXiv:2412.11295}
}
read the original abstract

Taking a quotient roughly means changing the notion of equality on a given object, set or type. In a quantitative setting, equality naturally generalises to a distance, measuring how much elements are similar instead of just stating their equivalence. Hence, quotients can be understood quantitatively as a change of distance. In this paper, we show how, combining Lawvere's doctrines and the calculus of relations, one can unify quantitative and usual quotients in a common picture. More in detail, we introduce relational doctrines as a functorial description of (the core of) the calculus of relations. Then, we define quotients and a universal construction adding them to any relational doctrine, generalising the quotient completion of existential elementary doctrine and also recovering many quantitative examples. This construction deals with an intensional notion of quotient and breaks extensional equality of morphisms. Then, we describe another construction forcing extensionality, showing how it abstracts several notions of separation in metric and topological structures. Combining these two constructions, we get the extensional quotient completion, whose essential image is characterized through the notion of projective cover. As an application, we show that, under suitable conditions, relational doctrines of algebras arise as the extensional quotient completion of free algebras. Finally, we compare relational doctrines to other categorical structures where one can model the calculus of relations.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Logical Aspects of Virtual Double Categories

    math.CT 2025-01 conditional novelty 6.0 of 10

    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.

Reference graph

Works this paper leans on

57 extracted references · 41 canonical work pages · cited by 1 Pith paper

  1. [46]

    Dagnino, F

    F. Dagnino, F. Pasquali, Cauchy-completions and the rule of uniq ue choice in relational doctrines CoRR abs/2402.19266 (2024). arXiv:2402.19266, doi:10.48550/ARXIV.2402.19266. URL https://doi.org/10.48550/arXiv.2402.19266

    arXiv doi:10.48550/arxiv.2402.19266 2024

  2. [32]

    E. M. Vitale, On the characterization of monadic categories ove r set, Cahiers de Topologie et G´ eom´ etrie Diff´ erentielle Cat´ egoriques 35(4) (1994) 351–358. URL http://eudml.org/doc/91556

    work page 1994

  3. [1]

    Barthe, V

    G. Barthe, V. Capretta, O. Pons, Setoids in type theory, Journal of Functional Programming 13 (2) (2003) 261–293. doi:10.1017/S0956796802004501

    work page doi:10.1017/s0956796802004501 2003

  4. [2]

    Hofmann, Extensional constructs in intensional type theor y, CPHC/BCS Distinguished Dissertations, Springer-Verlag London Lt d., London, 1997

    M. Hofmann, Extensional constructs in intensional type theor y, CPHC/BCS Distinguished Dissertations, Springer-Verlag London Lt d., London, 1997

    work page 1997

  5. [3]

    Carboni, R

    A. Carboni, R. Celia Magno, The free exact category on a left exa ct one, Journal of the Australian Mathematical Society. Series A. Pu re Mathematics and Statistics 33 (1982) 295 – 301

    work page 1982

  6. [4]

    Carboni, E

    A. Carboni, E. Vitale, Regular and exact completions, Journal of Pure and Applied Algebra 125 (1998) 79–117

    work page 1998

  7. [5]

    Maietti, G

    M. Maietti, G. Rosolini, Quotient completion for the foundation of c onstructive mathematics, Logica Universalis 7 (3) (2013) 371–402. doi:10.1007/s11787-013-0080-2 . URL https://doi.org/10.1007/s11787-013-0080-2

    doi:10.1007/s11787-013-0080-2 2013

  8. [6]

    M. E. Maietti, G. Rosolini, Elementary quotient completion, Theory and Applications of Categories 27 (17) (2013) 445–463

    work page 2013

Show all 57 references
  1. [7]

    F. W. Lawvere, Metric spaces, generalized logic, and closed cate gories, Rend. Sem. Mat. Fis. Milano 43 (1973) 135–166

    1973

  2. [8]

    Ad´ amek, Varieties of quantitative algebras and their monads , in: C

    J. Ad´ amek, Varieties of quantitative algebras and their monads , in: C. Baier, D. Fisman (Eds.), Proceedings of the 37th Annual ACM/IE EE Symposium on Logic in Computer Science, LICS 2022, ACM, 2022, pp. 9:1–9:10. doi:10.1145/3531130.3532405

    2022

  3. [9]

    Mardare, P

    R. Mardare, P. Panangaden, G. D. Plotkin, Quantitative algebra ic rea- soning, in: M. Grohe, E. Koskinen, N. Shankar (Eds.), Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, ACM, 2016, pp. 700–709. doi:10.1145/2933575.2934518

    2016

  4. [10]

    Mardare, P

    R. Mardare, P. Panangaden, G. D. Plotkin, On the axiomatizabilit y of quantitative algebras, in: Proceedings of the 32nd Annual ACM/IE EE Symposium on Logic in Computer Science, LICS 2017, IEEE Computer Society, 2017, pp. 1–12. doi:10.1109/LICS.2017.8005102. 66

    2017

  5. [11]

    F. W. Lawvere, Adjointness in foundations, Dialectica 23 (1969 ) 281– 296, also available as Repr. Theory Appl. Categ., 16 (2006) 1–16. doi:10.1111/j.1746-8361.1969.tb01194.x

    2006

  6. [12]

    F. W. Lawvere, Equality in hyperdoctrines and comprehension s chema as an adjoint functor, in: A. Heller (Ed.), Proceedings of the New Yo rk Symposium on Application of Categorical Algebra, American Mathe- matical Society, 1970, pp. 1–14

    1970

  7. [13]

    B. P. F. Jacobs, Categorical Logic and Type Theory, Vol. 141 o f Studies in logic and the foundations of mathematics, North-Holland, 2001. URL http://www.elsevierdirect.com/product.jsp?isbn=9780444508539

    2001

  8. [14]

    A. M. Pitts, Categorical logic, in: Handbook of logic in computer s ci- ence, Vol. 5, Vol. 5 of Handbook of Logic in Computer Science, Oxfor d Univ. Press, New York, 2000, pp. 39–128

    2000

  9. [15]

    van Oosten, Realizability: An Introduction to its Categorical Side, Vol

    J. van Oosten, Realizability: An Introduction to its Categorical Side, Vol. 152 of Studies in Logic and the Foundations of Mathematics, Nor th Holland Publishing Company, 2008

    2008

  10. [16]

    Dagnino, F

    F. Dagnino, F. Pasquali, Logical foundations of quantitative eq uality, in: C. Baier, D. Fisman (Eds.), Proceedings of the 37th Annual ACM/IE EE Symposium on Logic in Computer Science, LICS 2022, ACM, 2022, pp. 16:1–16:13. doi:10.1145/3531130.3533337

    2022

  11. [17]

    Andr´ eka, S

    H. Andr´ eka, S. Givant, P. Jipsen, I. N´ emeti, On tarski’s axiomatic foun- dations of the calculus of relations, The Journal of Symbolic Logic 82 (3) (2017) 966–994

    2017

  12. [18]

    C. S. Peirce, The logic of relatives, The Monist 7 (2) (1897) 161– 217

  13. [19]

    Tarski, On the calculus of relations, Journal of Symbolic Logic 6 (3) (1941) 73–89

    A. Tarski, On the calculus of relations, Journal of Symbolic Logic 6 (3) (1941) 73–89. doi:10.2307/2268577

    1941 doi

  14. [20]

    Givant, The calculus of relations as a foundation for mathema tics, Journal of Automated Reasoning 37 (4) (2006) 277–322

    S. Givant, The calculus of relations as a foundation for mathema tics, Journal of Automated Reasoning 37 (4) (2006) 277–322. doi:10.1007/s10817-006-9062-x . URL https://doi.org/10.1007/s10817-006-9062-x 67

    2006 doi

  15. [21]

    Tarski, S

    A. Tarski, S. Givant, A Formalization of Set Theory Without Varia bles, no. v. 41 in A formalization of set theory without variables, American Mathematical Soc., 1988

    1988

  16. [22]

    Dal Lago, F

    U. Dal Lago, F. Gavazzo, A relational theory of effects and co effects, Proceedings of the ACM on Programming Languages 6 (POPL) (2022 ) 1–28. doi:10.1145/3498692

    2022 doi

  17. [23]

    Gavazzo, Quantitative behavioural reasoning for higher-o rder ef- fectful programs: Applicative distances, in: A

    F. Gavazzo, Quantitative behavioural reasoning for higher-o rder ef- fectful programs: Applicative distances, in: A. Dawar, E. Gr¨ ade l (Eds.), Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, ACM, 2018, pp. 452–461. doi:10.1145/32091...

    2018

  18. [24]

    Gavazzo, C

    F. Gavazzo, C. D. Florio, Elements of quantitative rewriting, Pr oceed- ings of the ACM on Programming Languages 7 (POPL) (2023) 1832–

    2023

  19. [25]

    Lack, A 2-Categories Companion, Springer New York, New Yo rk, NY, 2010, pp

    S. Lack, A 2-Categories Companion, Springer New York, New Yo rk, NY, 2010, pp. 105–191. doi:10.1007/978-1-4419-1524-5_4 . URL https://doi.org/10.1007/978-1-4419-1524-5_4

    2010 doi

  20. [26]

    A. Kurz, J. Velebil, Relation lifting, a survey, J. Log. Algebraic Me thods Program. 85 (4) (2016) 475–499. doi:10.1016/j.jlamp.2015.08.002. URL https://doi.org/10.1016/j.jlamp.2015.08.002

    2016 doi

  21. [27]

    Betti, J

    R. Betti, J. Power, On local adjointness of distributive bicateg ories, Bollettino della Unione Matematica Italiana 2 (4) (1988) 931–947

    1988

  22. [28]

    Blackwell, G

    R. Blackwell, G. M. Kelly, J. Power, Two-dimensional monad the- ory, Journal of Pure and Applied Algebra 59 (1) (1989) 1–41. doi:10.1016/0022-4049(89)90160-6

    1989 doi

  23. [29]

    Kock, Monads for which structures are adjoint to units, Journal of Pure and Applied Algebra 104 (1995) 41–59

    A. Kock, Monads for which structures are adjoint to units, Journal of Pure and Applied Algebra 104 (1995) 41–59. doi:10.1016/0022-4049(94)00111-U

    1995 doi

  24. [30]

    G. M. Kelly, S. Lack, On property-like structures, Theory and Applica- tions of Categories 3 (9) (1997) 213–250. 68

    1997

  25. [31]

    Street, The formal theory of monads, Journal of Pure an d Applied Algebra 2 (2) (1972) 149 – 168

    R. Street, The formal theory of monads, Journal of Pure an d Applied Algebra 2 (2) (1972) 149 – 168. doi:10.1016/0022-4049(72)90019-9

    1972 doi

  26. [33]

    Lambek, Diagram chasing in ordered categories with involu- tion, Journal of Pure and Applied Algebra 143 (1) (1999) 293–307

    J. Lambek, Diagram chasing in ordered categories with involu- tion, Journal of Pure and Applied Algebra 143 (1) (1999) 293–307. doi:https://doi.org/10.1016/S0022-4049(98)00115-7

    1999 doi

  27. [34]

    Dagnino, F

    F. Dagnino, F. Pasquali, Quotients and extensionality in relationa l doctrines, in: M. Gaboardi, F. van Raamsdonk (Eds.), 8th Interna - tional Conference on Formal Structures for Computation and De duction, FSCD 2023, Vol. 260 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentru m f¨ ...

    2023 doi

  28. [35]

    Shulman, Framed bicategories and monoidal fibrations, Theo ry and Applications of Categories 20 (18) (2008) 650–738

    M. Shulman, Framed bicategories and monoidal fibrations, Theo ry and Applications of Categories 20 (18) (2008) 650–738

    2008

  29. [36]

    Lambert, Double categories of relations, Theory and Applica tions of Categories 38 (33) (2022) 1249–1283

    M. Lambert, Double categories of relations, Theory and Applica tions of Categories 38 (33) (2022) 1249–1283

    2022

  30. [37]

    Hofmann, G

    D. Hofmann, G. J. Seal, W. Tholen, Monoidal Topology: A Catego rical Approach to Order, Metric, and Topology, Vol. 153, Cambridge Univ er- sity Press, 2014

    2014

  31. [38]

    Laird, G

    J. Laird, G. Manzonetto, G. McCusker, M. Pagani, Weighted re - lational models of typed lambda-calculi, in: Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Sci- ence, LICS 2013, IEEE Computer Society, 2013, pp. 301–310. doi:10.1109/LICS.2013.36

    2013 doi

  32. [39]

    C. L. Ong, Quantitative semantics of the lambda calculus: Some generalisations of the relational model, in: Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Sci- ence, LICS 2017, IEEE Computer Society, 2017, pp. 1–12. doi:10.1109/LICS.2017.8005064. 69

    2017

  33. [40]

    Barr, Relational algebras, in: S

    M. Barr, Relational algebras, in: S. MacLane, H. Applegate, M. Barr, B. Day, E. Dubuc, Phreilambud, A. Pultr, R. Street, M. Tierney, S. Swierczkowski (Eds.), Reports of the Midwest Category Semina r IV, Springer Berlin Heidelberg, Berlin, Heidelberg, 1970, pp. 39–55

    1970

  34. [41]

    Thijs, Simulations and fixpoint semantics, Ph.D

    A. Thijs, Simulations and fixpoint semantics, Ph.D. thesis, Rijksu niver- siteit Groningen (1996)

    1996

  35. [42]

    Scott, A new category? Domains, spaces and equivalence re lations, available at http://www.cs.cmu.edu/Groups/LTC/ (1996)

    D. Scott, A new category? Domains, spaces and equivalence re lations, available at http://www.cs.cmu.edu/Groups/LTC/ (1996)

    1996

  36. [43]

    Bishop, Foundations of Constructive Analysis, McGraw-Hill s eries in higher mathematics, McGraw-Hill, 1967

    E. Bishop, Foundations of Constructive Analysis, McGraw-Hill s eries in higher mathematics, McGraw-Hill, 1967

    1967

  37. [44]

    Bishop, D

    E. Bishop, D. Bridges, Constructive Analysis, Grundlehren der mathe- matischen Wissenschaften, Springer Berlin Heidelberg, 2012

    2012

  38. [45]

    M. E. Maietti, F. Pasquali, G. Rosolini, Quasitoposes as elementary quotient completions (2024). arXiv:2111.15299. URL https://arxiv.org/abs/2111.15299

    2024 arXiv

  39. [47]

    Dagnino, G

    F. Dagnino, G. Rosolini, Doctrines, modalities and comonads, Mat h- ematical Structures in Computer Science 31 (7) (2021) 769–798. doi:10.1017/S0960129521000207. URL https://doi.org/10.1017/S0960129521000207

    2021 doi

  40. [48]

    Carboni, R

    A. Carboni, R. Walters, Cartesian bicategories I, Journal of P ure and Applied Algebra 49 (1-2) (1987) 11–32

    1987

  41. [49]

    P. J. Freyd, A. Scedrov, Categories, allegories, Vol. 39 of Nor th-Holland mathematical library, North-Holland, 1990

    1990

  42. [50]

    Bonchi, A

    F. Bonchi, A. Santamaria, J. Seeber, P. Sobocinski, On doctrin es and cartesian bicategories, in: F. Gadducci, A. Silva (Eds.), 9th Confer ence on Algebra and Coalgebra in Computer Science, CALCO 2021, Vol. 211 70 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik,...

    2021 doi

  43. [51]

    C. J. Cioffo, Biased elementary doctrines and quotient completio ns (2023). arXiv:2304.03066. URL https://arxiv.org/abs/2304.03066

    2023 arXiv

  44. [52]

    M. E. Maietti, F. Pasquali, G. Rosolini, Triposes, exact completions, and Hilbert’s epsilon-operator, Tbilisi Mathematical Journal 10 (3) (2017) 141 – 166. doi:10.1515/tmj-2017-0106. URL https://doi.org/10.1515/tmj-2017-0106

    2017 doi

  45. [53]

    Maietti, G

    M. Maietti, G. Rosolini, Relating quotient completions via categoric al logic., in: D. Probst, P. S. (eds.) (Eds.), Concepts of Proof in Mathe mat- ics, Philosophy, and Computer Science, De Gruyter, 2016, pp. 229 –250

    2016

  46. [54]

    Frey, Triposes, q-toposes and toposes, Annals of Pure and Applied Logic 166 (2) (2015) 232–259

    J. Frey, Triposes, q-toposes and toposes, Annals of Pure and Applied Logic 166 (2) (2015) 232–259. doi:https://doi.org/10.1016/j.apal.2014.10.005. URL https://www.sciencedirect.com/science/article/pii/S0168007214001109

    2015 doi

  47. [55]

    M. E. Maietti, G. Rosolini, Unifying exact completions, Appl. Categ or- ical Struct. 23 (1) (2015) 43–52. doi:10.1007/s10485-013-9360-5 . URL https://doi.org/10.1007/s10485-013-9360-5

    2015 doi

  48. [56]

    Cruttwell, M

    G. Cruttwell, M. Shulman, A unified framework for generalized mu lticat- egories, Theory and Applications of Categories 24 (21) (2010) 580 –655

    2010

  49. [57]

    T. M. Fiore, N. Gambino, J. Kock, Monads in double categories, Journal of Pure and Applied Algebra 215 (6) (2011) 1174–1197. doi:https://doi.org/10.1016/j.jpaa.2010.08.003. 71

    2011 doi

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.