Pith. sign in

REVIEW 2 major objections 6 minor 110 references

Logical Aspects of Virtual Double Categories

T0 review · 2 major / 6 minor · reviewed 2026-08-10 · deepseek-v4-flash

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

Pith's one-line read The paper's central theorem makes a cartesian fibration model regular logic exactly when its bilateral virtual double category is a cartesian equipment.

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

arxiv 2501.17869 v2 pith:2XY5VGLD submitted 2025-01-15 math.CT

Hayato Nasu This is my paper · ORCID
classification math.CT MSC 18N1003G3018A05
keywords virtualdoublecategoriesregularlogiccartesianfibrationselementaryexistentialFrobeniusequipmentscategoricaltypetheoryBeck-Chevalleycondition
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

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

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

Reading between the lines

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

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

Formalized claims in Lean

  1. Claim #1: 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 bilate

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

2 major / 6 minor

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.

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 (2)
  1. [2.3.3, Proposition 2.3.34] 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.
  2. [2.3.3, Proposition 2.3.36 and Corollary 2.3.37] 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.
minor comments (6)
  1. [2.3.1, proofs of Propositions 2.3.7 and 2.3.10] 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.
  2. [2.3.1, Lemma 2.3.9 and Section 2.5.1] 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".
  3. [2.3.3, proof of Lemma 2.3.35] 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.
  4. [1.4, Proposition 1.4.3 and Remark 1.4.4] 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.
  5. [2.4.2, Theorem 2.4.8] 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.
  6. [2.3.3, Proposition 2.3.28] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the central equivalence and the image characterization are proved from the stated definitions; the n-ary omission in Proposition 2.3.34 is a proof gap, not a circular reduction.

full rationale

The paper's derivation chain is not circular. The main equivalence (Theorem 2.3.14, restated as Theorem 2.3.17) is proved by unpacking the construction in Definition 2.3.1 rather than by assuming it: if p is elementary existential, Lemmas 2.3.6 and 2.3.9 construct units and positive-length composites in /BU il(p), and Propositions 2.3.7 and 2.3.10 verify compatibility with the cartesian structure; conversely, the proof of Theorem 2.3.17 recovers the bifibration, Beck-Chevalley, and Frobenius structure from the equipment structure of /BU il(p) using the independently proved Lemmas 1.2.22-1.2.24. The image characterization (Corollary 2.3.37) does rely on Proposition 2.3.34, whose proof contains an explicit omitted case: "We will only show this in the case of n = 2, and the general case is similar." This is a genuine missing coherence check for the n-ary globular cells, but it is not circular: the claimed bijection for general n must be verified rather than being built into the definitions. The self-citations to [HN23] (for example, Proposition 2.3.30) are disclosed and concern prior joint results; the Sandwich Lemma is restated and proved in Lemma 1.2.12, and the compact-closed facts are external to the target equivalence. No fitted parameter is renamed as a prediction, and no known result is merely repackaged as a new one. The shortfalls in the manuscript are therefore proof gaps and not circularity.

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

No free parameters are fitted to data. The proofs rely on standard 2-category theory and on previously established results, including several from the author's own prior work. No new entities such as particles or dimensions are introduced; the /BU il construction is a mathematical construction, not an invented entity.

assumptions (4)
  • standard math Axiom of choice: any fibration admits an equivalent cloven fibration.
    Used in Section 2.2 to identify fibrations with indexed categories.
  • standard math Strictification theorem: any pseudo-double category is equivalent to a strict double category [GP99, §7.5].
    Invoked in Remark 1.2.1 to justify informal n-ary composition notation.
  • domain assumption The 2-categories involved have strict finite products and the inclusion 2-functors are local inclusions and isofibrations (Lemma 2.3.16).
    Needed for the pullback square characterization in Theorem 2.3.17; the paper does not verify this in detail.
  • standard math Standard definitions and results on fibrations, virtual double categories, and equipments from [CS10, Shu08, Ale18].
    Preliminaries in Chapter 1 are taken as background.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Logical Aspects of Virtual Double Categories." pith.science (2026). https://pith.science/paper/2XY5VGLD

@misc{pith2026250117869,
  author       = {Pith},
  title        = {Pith review of: Logical Aspects of Virtual Double Categories},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2XY5VGLD}},
  note         = {Machine review of arXiv:2501.17869}
}
read the original abstract

This thesis deals with two main topics: virtual double categories as semantics environments for predicate logic, and a syntactic presentation of virtual double categories as a type theory. One significant principle of categorical logic is bringing together the semantics and the syntax of logical systems in a common categorical framework. This thesis is intended to propose a double-categorical method for categorical logic in line with this principle. On the semantic side, we investigate virtual double categories as a model of predicate logic and illustrate that this framework subsumes the existing frameworks properly. On the syntactic side, we develop a type theory called FVDblTT that is designed as an internal language for virtual double categories.

Figures

Figures reproduced from arXiv: 2501.17869 by the authors.

Figure 1
Figure 1. The relationship among the structures quantifier ∃, and the conjunction ∧, the category in question should be a regular category. The exis￾tential quantifier is then interpreted using the factorization system consisting of regular epimorphisms and monomorphisms. Various classes of categories and their corresponding logical systems have been studied, from categories with finite products to regular categories and beyo… view at source ↗
Figure 1
Figure 1. A virtual cell in Prof and a proterm that corresponds to it. Corresponding to these four kinds of entities, FVDblTT has four kinds of core judgments: types, terms, protypes, and proterms ( [PITH_FULL_IMAGE:figures/full_fig_p076_1.png] view at source ↗
Figure 2
Figure 2. Judgments of FVDblTT. Fibrationality is satisfied in most virtual double categories for our purposes and is conceptually a natural assumption since it represents the possibility of instantiating functors S and T in a profunctor α(−, •). Furthermore, the fibrationality reflects how we practically reason about cells in the virtual double categories for formal category theory. For instance, a virtual cell in Prof is de… view at source ↗
Figures from the paper (7 more)
Figure 4
Figure 4. Figure 4: Pointwise Kan extensions A pointwise left Kan extension l(y) of s(x) along a fully faithful functor t(x) admits an isomorphism l(t(x)) ∼≡ s(x). Proof. (Contexts are omitted.) l(t(x ′ ))9K z ∼≡ (t(x)9J (t(x ′ ))) ⊲x:I (s(x)9K z) (Lan) ∼≡ (x 9I x ′ ) ⊲x:I (s(x)9K z) (FF−…
Figure 3
Figure 3. Figure 3: Fully faithfulness A term y : J ⊢ l(y) : K is a pointwise left Kan extension of x : I ⊢ s(x) : K along x : I ⊢ t(x) : J if it comes with the following protype isomorphism. y : J # z : K ⊢ Lan : l(y)9K z ∼≡ (t(x)9J y) ⊲x:I (s(x)9K z) [PITH_FULL_IMAGE:figures/full_fig_p…
Figure 6
Figure 6. Figure 6: Judgments in FVDblTT Types, contexts, terms, and term substitutions are the same as those in the algebraic theory as in [Cro94, Jac99]. This fragment of the type theory serves as the theory of categories and functors. As usual, substitution of terms for variables in te…
Figure 7
Figure 7. Figure 7: The rules for types, contexts, and terms ` # ´ ⊢ ¸ protype ` # ´ ⊢ ˛ protype ` # ´ ⊢ ¸ ∧ ˛ protype ` # ´ ⊢ ⊤ protype ` | · proctx `0 # . . . # `n | A proctx `n # ´ ⊢ ¸ protype `0 # . . . # `n # ´ | A, a : ¸ proctx ` # ´ ⊢ ¸ protype ` ′ ⊢ S0 ≡ S1 / ` ´′ ⊢ T0 ≡ T1 / ´ ` …
Figure 8
Figure 8. Figure 8: The rules for protypes, procontexts, and proterms Signatures. In algebraic theories, one often starts with a signature that specifies the sorts and operations of the theory. We present the notion of a signature for FVDblTT as follows. Definition 3.2.1. A signature Σ fo…
Figure 9
Figure 9. Figure 9: The rules for the signature Substitution. The substitution of terms for variables in terms, protypes, and proterms is defined inductively as follows. xi [S/´] ≡ si (i = 1, . . . , n, S = (s1, . . . ,sn)) f (s1, . . . ,sn)[S/´] ≡ f (s1[S/´], . . . ,sn[S/´]) hs,ti[S/´] ≡…
Figure 10
Figure 10. Figure 10: Translation of protype isomorphisms Lemma 3.5.13. The assignment (Σ,PI,E) 7→ Ufd(Σ,PI,E) induces a functor Ufd: Speci ∼≡ Speci. y Proof sketch. For a morphism of specifications Φ: (Σ,E) (Σ′ ,E ′ ), the assignment Ufd(Φ) sends the transformation symbols ’m and m to ’Φ(…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

110 extracted references · 71 canonical work pages

  1. [1]

    Cartesian Double Categories with an Emphasis on Characterizing Spans

    Evangelia Aleiferi. Cartesian Double Categories with an Emphasis on Characterizing Spans . PhD thesis, Dalhousie University, September 2018. https://arxiv.org/abs/1809.06940

    arXiv 2018

  2. [2]

    The formal theory of relative monads

    Nathanael Arkor and Dylan McDermott. The formal theory of relative monads. Journal of Pure and Applied Algebra , 228(9):107676, September 2024. https://arxiv.org/abs/2302.14014

    work page arXiv 2024

  3. [3]

    The nerve theorem for relative monads

    Nathanael Arkor and Dylan McDermott. The nerve theorem for relative monads, 2024. https://arxiv.org/abs/2404.01281

    work page Pith review arXiv 2024

  4. [4]

    Bicategorical type theory: Semantics and syntax

    Benedikt Ahrens, Paige Randall North, and Niels van der Weide . Bicategorical type theory: Semantics and syntax. Math. Structures Comput. Sci. , 33(10):868--912, 2023

    2023

  5. [5]

    tangle, 2022

    Nathanael Arkor. tangle, 2022. https://github.com/varkor/tangle

    2022

  6. [6]

    Diagrammatic Algebra of First Order Logic , January 2024

    Filippo Bonchi, Di Giorgio, Alessandro , Nathan Haydon, and Pawel Sobocinski. Diagrammatic Algebra of First Order Logic , January 2024. arXiv:2401.07055

    arXiv 2024

  7. [7]

    Exact categories

    Michael Barr, Pierre A Grillet, and Donovan H Osdol. Exact categories . Lecture Notes in Mathematics. Springer, Berlin, Heidelberg, 1971

    1971

  8. [8]

    Functorial Semantics for Relational Theories , November 2017

    Filippo Bonchi, Dusko Pavlovic, and Pawel Sobocinski. Functorial Semantics for Relational Theories , November 2017. https://arxiv.org/abs/1711.08699

    arXiv 2017

Show all 110 references
  1. [9]

    On Doctrines and Cartesian Bicategories

    Filippo Bonchi, Alessio Santamaria, Jens Seeber, and Pawe Soboci\' n ski. On Doctrines and Cartesian Bicategories . In Fabio Gadducci and Alexandra Silva, editors, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021) , volume 211 of Leibniz International Pr...

    2021

  2. [10]

    Introduction

    Marta Bunge. Introduction. a personal tribute to peter freyd and bill lawvere. Tbilisi Mathematical Journal , 10:i -- x, 2017

    2017

  3. [11]

    T -cat\'egories (cat\'egories dans un triple)

    Albert Burroni. T -cat\'egories (cat\'egories dans un triple). Cahiers Topologie G\'eom. Diff\'erentielle , 12:215--321, 1971

    1971

  4. [12]

    Generalised algebraic theories and contextual categories

    John Cartmell. Generalised algebraic theories and contextual categories. Ann. Pure Appl. Logic , 32(3):209--243, 1986

    1986

  5. [13]

    The Biequivalence of Locally Cartesian Closed Categories and Martin-L \"of Type Theories

    Pierre Clairambault and Peter Dybjer. The Biequivalence of Locally Cartesian Closed Categories and Martin-L \"of Type Theories . Mathematical Structures in Computer Science , 24(6):e240606, December 2014

    2014

  6. [14]

    M. S. Calenko, V. B. Gisin, and D. A. Raikov. Ordered categories with involution. Dissertationes Math. (Rozprawy Mat.) , 227:111, 1984

    1984

  7. [15]

    Bicategories of spans and relations

    Aurelio Carboni, Stefano Kasangian, and Ross Street. Bicategories of spans and relations. J. Pure Appl. Algebra , 33(3):259--267, 1984

    1984

  8. [16]

    Carboni, G

    A. Carboni, G. M. Kelly, and R. J. Wood. A 2 -categorical approach to change of base and geometric morphisms. I . volume 32, pages 47--95. 1991. International Category Theory Meeting (Bangor, 1989 and Cambridge, 1990)

    1991

  9. [17]

    Carboni, G

    A. Carboni, G. M. Kelly, R. F. C. Walters, and R. J. Wood. Cartesian bicategories II . Theory Appl. Categ. , 19:93--124, 2007

    2007

  10. [18]

    Roy L. Crole. Categories for Types . Cambridge University Press, 1994

    1994

  11. [19]

    G. S. H. Cruttwell and Michael A. Shulman. A unified framework for generalized multicategories. Theory Appl. Categ. , 24:No. 21, 580--655, 2010

    2010

  12. [20]

    Carboni and R

    A. Carboni and R. F. C. Walters. Cartesian bicategories. I . J. Pure Appl. Algebra , 49(1-2):11--32, 1987

    1987

  13. [21]

    Quotients and extensionality in relational doctrines

    Francesco Dagnino and Fabio Pasquali. Quotients and extensionality in relational doctrines. In 8th I nternational C onference on F ormal S tructures for C omputation and D eduction , volume 260 of LIPIcs. Leibniz Int. Proc. Inform. , pages Art. No. 25, 23. Schloss Dagstuhl. Le...

    2023

  14. [22]

    Cauchy-completions and the rule of unique choice in relational doctrines, 2024

    Francesco Dagnino and Fabio Pasquali. Cauchy-completions and the rule of unique choice in relational doctrines, 2024. https://arxiv.org/abs/2402.19266

    2024 arXiv

  15. [23]

    The Relational Quotient Completion , December 2024

    Francesco Dagnino and Fabio Pasquali. The Relational Quotient Completion , December 2024. https://arxiv.org/abs/2412.11295

    2024 arXiv

  16. [24]

    R. J. Macg . Dawson, R. Par \'e , and D. A. Pronk. Paths in double categories. Theory and Applications of Categories , 16:No. 18, 460--521, 2006

    2006

  17. [25]

    Elementary fibrations of enriched groupoids

    Jacopo Emmenegger, Fabio Pasquali, and Giuseppe Rosolini. Elementary fibrations of enriched groupoids. Math. Structures Comput. Sci. , 31(9):958--978, 2021

    2021

  18. [26]

    A characterisation of elementary fibrations

    Jacopo Emmenegger, Fabio Pasquali, and Giuseppe Rosolini. A characterisation of elementary fibrations. Ann. Pure Appl. Logic , 173(6):Paper No. 103103, 29, 2022

    2022

  19. [27]

    P. J. Freyd and G. M. Kelly. Categories of continuous functors. I . J. Pure Appl. Algebra , 2:169--191, 1972

    1972

  20. [28]

    Freyd and Andre Scedrov

    Peter J. Freyd and Andre Scedrov. Categories, allegories , volume 39 of North-Holland Mathematical Library . North-Holland Publishing Co., Amsterdam, 1990

    1990

  21. [29]

    Enriched -categories via non-symmetric -operads

    David Gepner and Rune Haugseng. Enriched -categories via non-symmetric -operads. Advances in Mathematics , 279:575--716, July 2015

    2015

  22. [30]

    Limits in double categories

    Marco Grandis and Robert Par \'e . Limits in double categories. G \'e om. Diff. Cat \'e g , 40:162--220, January 1999

    1999

  23. [31]

    Adjoint for double categories

    Marco Grandis and Robert Par\'e. Adjoint for double categories. Cahiers de Topologie et G \'e om \'e trie Diff \'e rentielle Cat \'e goriques , 45(3):193--240, 2004

    2004

  24. [32]

    John W. Gray. Formal Category Theory : Adjointness for 2- Categories , volume 391 of Lecture Notes in Mathematics . Springer Berlin Heidelberg, Berlin, Heidelberg, 1974

    1974

  25. [33]

    Higher Dimensional Categories -- From Double to Multiple Categories

    Marco Grandis. Higher Dimensional Categories -- From Double to Multiple Categories . World Scientific Publishing Co. Pte. Ltd., Hackensack, NJ, 2020

    2020

  26. [34]

    Categories fibrees et descente

    Alexander Grothendieck. Categories fibrees et descente. In Rev \^e tements Etales et Groupe Fondamental , pages 145--194, Berlin, Heidelberg, 1971. Springer Berlin Heidelberg

    1971

  27. [35]

    Fibrations, Logical Predicates and Indeterminates

    Claudio Hermida. Fibrations, Logical Predicates and Indeterminates . PhD thesis, University of Edinburgh, 1993

    1993

  28. [36]

    On fibred adjunctions and completeness for fibred categories

    Claudio Hermida. On fibred adjunctions and completeness for fibred categories. In Recent trends in data type specification ( C aldes de M alavella, 1992) , volume 785 of Lecture Notes in Comput. Sci. , pages 235--251. Springer, Berlin, 1994

    1992

  29. [37]

    Some properties of Fib as a fibred 2 -category

    Claudio Hermida. Some properties of Fib as a fibred 2 -category. J. Pure Appl. Algebra , 134(1):83--109, 1999

    1999

  30. [38]

    Representable multicategories

    Claudio Hermida. Representable multicategories. Adv. Math. , 151(2):164--225, 2000

    2000

  31. [39]

    Factorization systems and fibrations: Toward a fibred birkhoff variety theorem

    Jesse Hughes and Bart Jacobs. Factorization systems and fibrations: Toward a fibred birkhoff variety theorem. Electronic Notes in Theoretical Computer Science , 69:156--182, 2003. CTCS'02, Category Theory and Computer Science

    2003

  32. [40]

    Double categories of relations relative to factorisation systems, October 2023

    Keisuke Hoshino and Hayato Nasu. Double categories of relations relative to factorisation systems, October 2023. arXiv:2310.19428

    2023 arXiv

  33. [41]

    S. N. Hosseini, A. R. Shir Ali Nasab, W. Tholen, and L. Yeganeh. Quotients of span categories that are allegories and the representation of regular categories. Appl. Categ. Structures , 30(6):1177--1201, 2022

    2022

  34. [42]

    The groupoid interpretation of type theory

    Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. In Twenty-five years of constructive type theory ( V enice, 1995) , volume 36 of Oxford Logic Guides , pages 83--111. Oxford Univ. Press, New York, 1998

    1995

  35. [43]

    Categorical logic and type theory , volume 141 of Studies in Logic and the Foundations of Mathematics

    Bart Jacobs. Categorical logic and type theory , volume 141 of Studies in Logic and the Foundations of Mathematics . North-Holland Publishing Co., Amsterdam, 1999

    1999

  36. [44]

    Johnstone

    Peter T. Johnstone. Sketches of an Elephant : A Topos Theory Compendium : Volume 1 . Oxford Logic Guides . Oxford University Press, Oxford, New York, September 2002

    2002

  37. [45]

    Johnstone

    Peter T. Johnstone. Sketches of an Elephant : A Topos Theory Compendium : Volume 2 . Oxford Logic Guides . Oxford University Press, Oxford, New York, September 2002

    2002

  38. [46]

    Johnstone and Robert Par\'e, editors

    Peter T. Johnstone and Robert Par\'e, editors. Indexed categories and their applications , volume 661 of Lecture Notes in Mathematics . Springer-Verlag, Berlin-New York, 1978

    1978

  39. [47]

    Categories of relations and functional relations

    Romaine Jayewardene and Oswald Wyler. Categories of relations and functional relations. volume 8, pages 279--305. 2000. Papers in honour of Bernhard Banaschewski (Cape Town, 1996)

    2000

  40. [48]

    Relations in categories with pullbacks

    Yasuo Kawahara. Relations in categories with pullbacks. Mem. Fac. Sci. Kyushu Univ. Ser. A , 27:149--173, 1973

    1973

  41. [49]

    G. M. Kelly. A note on relations relative to a factorization system. In Category theory ( C omo, 1990) , volume 1488 of Lecture Notes in Math. , pages 249--261. Springer, Berlin, 1991

    1990

  42. [50]

    G. M. Kelly. Basic concepts of enriched category theory. Reprints in Theory and Applications of Categories , (10):vi+137, 2005

    2005

  43. [51]

    Relations in categories

    Aaron Klein. Relations in categories. Illinois J. Math. , 14:536--550, 1970

    1970

  44. [52]

    Augmented virtual double categories

    Seerp Roald Koudenburg. Augmented virtual double categories. Theory and Applications of Categories , 35:Paper No. 10, 261--325, 2020

    2020

  45. [53]

    Formal category theory in augmented virtual double categories

    Seerp Roald Koudenburg. Formal category theory in augmented virtual double categories. Theory and Applications of Categories , 41:Paper No. 10, 288--413, 2024

    2024

  46. [54]

    Kock and G

    A. Kock and G. E. Reyes. Doctrines in categorical logic. In Handbook of mathematical logic , volume 90 of Stud. Logic Found. Math. , pages 283--313. North-Holland, Amsterdam, 1977

    1977

  47. [55]

    J. Lambek. Diagram chasing in ordered categories with involution. volume 143, pages 293--307. 1999. Special volume on the occasion of the 60th birthday of Professor Michael Barr (Montreal, QC, 1997)

    1999

  48. [56]

    Double Categories of Relations

    Michael Lambert. Double Categories of Relations . Theory and Applications of Categories , 38(33):1249--1283, November 2022

    2022

  49. [57]

    William Lawvere

    F. William Lawvere. Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences of the United States of America , 50:869--872, 1963

    1963

  50. [58]

    William Lawvere

    F. William Lawvere. Adjointness in foundations. Dialectica , 23(3/4):281--296, 1969

    1969

  51. [59]

    William Lawvere

    F. William Lawvere. Equality in hyperdoctrines and comprehension schema as an adjoint functor. In Alex Heller, editor, Proceedings of Symposia in Pure Mathematics , volume 17, pages 1--14. American Mathematical Society, Providence, Rhode Island, 1970

    1970

  52. [60]

    William Lawvere

    F. William Lawvere. Metric spaces, generalized logic, and closed categories. Rendiconti del Seminario Matematico e Fisico di Milano , 43(1):135--166, December 1973

    1973

  53. [61]

    Fibrations of Predicates and Bicategories of Relations

    Finn Lawler. Fibrations of Predicates and Bicategories of Relations . PhD thesis, Trinity College, Dublin, 2015. PhD thesis, available at https://arxiv.org/abs/1502.08017

    2015 arXiv

  54. [62]

    Generalized enrichment of categories

    Tom Leinster. Generalized enrichment of categories. volume 168, pages 391--406. 2002. Category theory 1999 (Coimbra)

    2002

  55. [63]

    Higher Operads, Higher Categories , volume 298 of London Mathematical Society Lecture Note Series

    Tom Leinster. Higher Operads, Higher Categories , volume 298 of London Mathematical Society Lecture Note Series . Cambridge University Press, Cambridge, 2004

    2004

  56. [64]

    Licata and Robert Harper

    Daniel R. Licata and Robert Harper. 2- Dimensional Directed Type Theory . Electronic Notes in Theoretical Computer Science , 276:263--289, September 2011

    2011

  57. [65]

    FORMAL CATEGORY THEORY

    Ivan Di Liberti, Simon Henry, Mike Liebermann, and Fosco Loregian. FORMAL CATEGORY THEORY . course notes, https://ncatlab.org/nlab/files/DLHLL-FormalCategoryTheory.pdf (accessed 2024-09-25), 2017

    2024

  58. [66]

    Laretto, F

    A. Laretto, F. Loregian, and N. Veltri. Directed equality with dinaturality, 2024. https://arxiv.org/abs/2409.10237

    2024

  59. [67]

    ( Co )End Calculus , volume 468 of London Mathematical Society Lecture Note Series

    Fosco Loregian. ( Co )End Calculus , volume 468 of London Mathematical Society Lecture Note Series . Cambridge University Press, Cambridge, 2021

    2021

  60. [68]

    Categorical notions of fibration

    Fosco Loregian and Emily Riehl. Categorical notions of fibration. Expo. Math. , 38(4):496--514, 2020

    2020

  61. [69]

    Lambek and P

    J. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic , volume 7 of Cambridge Studies in Advanced Mathematics . Cambridge University Press, Cambridge, 1986

    1986

  62. [70]

    Stephen Lack, R. F. C. Walters, and R. J. Wood. Bicategories of spans as C artesian bicategories. Theory Appl. Categ. , 24:No. 1, 1--24, 2010

    2010

  63. [71]

    Exact completions and toposes

    Matias Menni. Exact completions and toposes . PhD thesis, University of Edinburgh, 2000

    2000

  64. [72]

    Relations in categories, 2000

    Stefan Milius. Relations in categories, 2000. master's thesis, available at https://www8.cs.fau.de/ext/milius/thesis/thesis_a4.pdf

    2000

  65. [73]

    G.P. Monro. Quasitopoi, logic and heyting-valued models. Journal of Pure and Applied Algebra , 42(2):141--164, 1986

    1986

  66. [74]

    Triposes, exact completions, and H ilbert's -operator

    Maria Emilia Maietti, Fabio Pasquali, and Giuseppe Rosolini. Triposes, exact completions, and H ilbert's -operator. Tbilisi Math. J. , 10(3):141--166, 2017

    2017

  67. [75]

    Elementary quotient completion

    Maria Emilia Maietti and Giuseppe Rosolini. Elementary quotient completion. Theory Appl. Categ. , 27:No. 17, 445--463, 2013

    2013

  68. [76]

    Quotient completion for the foundation of constructive mathematics

    Maria Emilia Maietti and Giuseppe Rosolini. Quotient completion for the foundation of constructive mathematics. Log. Univers. , 7(3):371--402, 2013

    2013

  69. [77]

    Comprehension and quotient structures in the language of 2-categories

    Paul-Andr\'e Melli\`es and Nicolas Rolland. Comprehension and quotient structures in the language of 2-categories. In 5th I nternational C onference on F ormal S tructures for C omputation and D eduction , volume 167 of LIPIcs. Leibniz Int. Proc. Inform. , pages Art. No. 6, 18...

    2020

  70. [78]

    String diagrams for double categories and equipments, 2018

    David Jaz Myers. String diagrams for double categories and equipments, 2018. https://arxiv.org/abs/1612.02762

    2018 arXiv

  71. [79]

    An internal logic of virtual double categories, 2024

    Hayato Nasu. An internal logic of virtual double categories, 2024. https://arxiv.org/abs/2410.06792

    2024 arXiv

  72. [80]

    New and Daniel R

    Max S. New and Daniel R. Licata. A Formal Logic for Formal Category Theory . In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures , volume 13992, pages 113--134. Springer Nature Switzerland, Cham, 2023

    2023

  73. [81]

    Towards a directed homotopy type theory

    Paige Randall North. Towards a directed homotopy type theory. In Proceedings of the Thirty-Fifth Conference on the Mathematical Foundations of Programming Semantics , volume 347 of Electron. Notes Theor . Comput . Sci . , pages 223--239. Elsevier Sci. B. V., Amsterdam, 2019

    2019

  74. [82]

    First order theories as double lawvere theories

    Robert Par\'e. First order theories as double lawvere theories. Conference talk at CT2009 in Cape Town, 2009. https://www.mscs.dal.ca/ pare/CapeTown2009.pdf

    2009

  75. [83]

    Morphisms of rings

    Robert Par\' e . Morphisms of rings. In Joachim L ambek: the interplay of mathematics, logic, and linguistics , volume 20 of Outst. Contrib. Log. , pages 271--298. Springer, Cham, 2021

    2021

  76. [84]

    Products in double categories, revisited, 2024

    Evan Patterson. Products in double categories, revisited, 2024. https://arxiv.org/abs/2401.08990

    2024

  77. [85]

    Transposing cartesian and other structure in double categories, 2024, 2404.08835

    Evan Patterson. Transposing cartesian and other structure in double categories, 2024, 2404.08835

    2024 arXiv

  78. [86]

    Du sko Pavlovi\'c. Maps. I . R elative to a factorisation system. J. Pure Appl. Algebra , 99(1):9--34, 1995

    1995

  79. [87]

    Du sko Pavlovi\'c. Maps. II . C hasing diagrams in categorical proof theory. J. IGPL , 4(2):159--194, 1996

    1996

  80. [88]

    Andrew M. Pitts. Categorical logic. In Handbook of logic in computer science, V ol. 5 , volume 5 of Handb. Log. Comput. Sci. , pages 39--128. Oxford Univ. Press, New York, 2000

    2000

  81. [89]

    Palmgren and S

    E. Palmgren and S. J. Vickers. Partial horn logic and C artesian categories. Ann. Pure Appl. Logic , 145(3):314--353, 2007

    2007

  82. [90]

    Formal category theory in -equipments i, 2024

    Jaco Ruit. Formal category theory in -equipments i, 2024. https://arxiv.org/abs/2308.03583

    2024

  83. [91]

    Kan extensions and the calculus of modules for --categories

    Emily Riehl and Dominic Verity. Kan extensions and the calculus of modules for --categories. Algebraic & Geometric Topology , 17(1):189--271, January 2017

    2017

  84. [92]

    Elements of - Category Theory

    Emily Riehl and Dominic Verity. Elements of - Category Theory . Cambridge Studies in Advanced Mathematics . Cambridge University Press, Cambridge, 2022

    2022

  85. [93]

    Robert A. G. Seely. Hyperdoctrines, natural deduction and the B eck condition. Z. Math. Logik Grundlag. Math. , 29(6):505--542, 1983

    1983

  86. [94]

    R. A. G. Seely. Locally cartesian closed categories and type theory. Mathematical Proceedings of the Cambridge Philosophical Society , 95(1):33--48, January 1984

    1984

  87. [95]

    Selinger

    P. Selinger. A survey of graphical languages for monoidal categories. In New structures for physics , volume 813 of Lecture Notes in Phys. , pages 289--355. Springer, Heidelberg, 2011

    2011

  88. [96]

    Framed bicategories and monoidal fibrations

    Michael Shulman. Framed bicategories and monoidal fibrations. Theory Appl. Categ. , 20:No. 18, 650--738, 2008

    2008

  89. [97]

    Compact closed bicategories

    Michael Stay. Compact closed bicategories. Theory Appl. Categ. , 31:Paper No. 26, 755--798, 2016

    2016

  90. [98]

    Streicher

    T. Streicher. A model of type theory in simplicial sets: a brief introduction to V oevodsky's homotopy type theory. J. Appl. Log. , 12(1):45--49, 2014

    2014

  91. [99]

    Fibered categories a la jean benabou, 2023

    Thomas Streicher. Fibered categories a la jean benabou, 2023. https://arxiv.org/abs/1801.02927

    2023 arXiv

  92. [100]

    La teoria delle relazioni nello studio di categorie regolari e di categorie esatte

    Rosanna Succi-Cruciani . La teoria delle relazioni nello studio di categorie regolari e di categorie esatte. Riv. Mat. Univ. Parma (4) , 1:143--158, 1975

    1975

  93. [101]

    Yoneda structures on 2-categories

    Ross Street and Robert Walters. Yoneda structures on 2-categories. Journal of Algebra , 50(2):350--379, 1978

    1978

  94. [102]

    On the calculus of relations

    Alfred Tarski. On the calculus of relations. J. Symbolic Logic , 6:73--89, 1941

    1941

  95. [103]

    Recursive Domains, Indexed Category Theory and Polymorphism

    Paul Taylor. Recursive Domains, Indexed Category Theory and Polymorphism . PhD thesis, University of Cambridge, 1983

    1983

  96. [104]

    Practical foundations of mathematics , volume 59 of Cambridge Studies in Advanced Mathematics

    Paul Taylor. Practical foundations of mathematics , volume 59 of Cambridge Studies in Advanced Mathematics . Cambridge University Press, Cambridge, 1999

    1999

  97. [105]

    cartesian bicategory

    Todd Trimble and other nLab authors . cartesian bicategory. https://ncatlab.org/nlab/show/cartesian+bicategory, 2009. Revision 27 https://ncatlab.org/nlab/revision/cartesian+bicategory/27, Last visited on 2025-01-28

    2009

  98. [106]

    The existential completion

    Davide Trotta. The existential completion. Theory Appl. Categ. , 35:No. 43, 1576--1607, 2020

    2020

  99. [107]

    Enriched categories, internal categories and change of base

    Dominic Verity. Enriched categories, internal categories and change of base. Repr. Theory Appl. Categ. , (20):1--266, 2011

    2011

  100. [108]

    R. J. Wood. Abstract proarrows. I . Cahiers de Topologie et G \'e om \'e trie Diff \'e rentielle , 23(3):279--290, 1982

    1982

  101. [109]

    R. J. Wood. Proarrows II . Cahiers de Topologie et G \'e om \'e trie Diff \'e rentielle Cat \'e goriques , 26(2):135--168, 1985

    1985

  102. [110]

    R. F. C. Walters and R. J. Wood. Frobenius objects in C artesian bicategories. Theory Appl. Categ. , 20:No. 3, 25--47, 2008

    2008

Pith tools

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