The familial nature of enrichment over virtual double categories

Soichiro Fujii; Stephen Lack

The familial nature of enrichment over virtual double categories

T0 review · 0 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read The enrichment 2-functor from virtual double categories to 2-categories is familial: a parametric right 2-adjoint preserving bicategorical pullbacks and fibrations.

desk verdict Solid paper proving Enr: VDBL → 2-CAT is familial; the main theorem is sound and the one omitted proof (Theorem 3.1) is not load-bearing. read the letter →

arxiv 2507.05529 v1 pith:U3AXKDDV submitted 2025-07-07 math.CT

Soichiro Fujii , Stephen Lack This is my paper

classification math.CT MSC 18D2018D6018N1018B1018D6518D7018M65

keywords enrichedcategoriesvirtualdoublefamilial2-functorsparametricright2-adjointspolynomialdiscreteopfibrationsfamiliesconstructioncategoryofelements

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

Enriched category theory is usually set over monoidal categories, and later bicategories, but both settings leave out examples and, as the paper shows, the enrichment 2-functor for bicategories is not a parametric right 2-adjoint. The paper's central claim is that moving the base of enrichment to virtual double categories repairs this: the 2-functor $\mathrm{Enr}\colon\mathbf{VDBL}\to\mathbf{2\text{-}CAT}$, sending a virtual double category $\mathbb{A}$ to the 2-category of $\mathbb{A}$-categories, is familial. Familial is a strengthening of "parametric right 2-adjoint" that guarantees preservation of bicategorical pullbacks and classes of fibrations; roughly, the 2-functor behaves like a families construction. The proof decomposes Enr into three steps — matrices, horizontal monads, and extraction of the 2-category — each either polynomial or a right 2-adjoint, and familial 2-functors compose. A reader should care because this gives enrichment a single formal property that holds for a very general class of bases and fails just outside it.

What carries the argument

The load-bearing mechanism is a discrete opfibration of virtual double categories, a map along which objects, vertical morphisms, and multicells lift uniquely. Proposition 5.5 shows any such map $P\colon\mathbb{X}\to\mathbb{Y}$ is powerful: the pullback 2-functor $P^*\colon\mathbf{VDBL}/\mathbb{Y}\to\mathbf{VDBL}/\mathbb{X}$ has a right 2-adjoint $Q_P$, which the proof constructs explicitly from fibre data. Applied to the forgetful map $P_{\mathrm{hc}}\colon(\mathrm{Set}_*)_{\mathrm{hc}}\to\mathrm{Set}_{\mathrm{hc}}$, powerfulness yields the polynomial 2-functor $\mathbb{Mat}\colon\mathbf{VDBL}\to\mathbf{VDBL}$, whose value at $\mathbb{A}$ is the virtual double category of families and matrices in $\mathbb{A}$. The decomposition $\mathrm{Enr}=V\circ\mathbb{Mod}\circ\mathbb{Mat}$ expresses that an $\mathbb{A}$-category is exactly a horizontal monad (a monad structure on an endomorphism) in the matrix virtual double category, with $V$ extracting the resulting 2-category; a parallel route using $Q\colon\mathbb{Span}_*\to\mathbb{Span}$ produces the polynomial families 2-functor $\mathbb{Fam}$ and its left adjoint $\mathbb{Elt}$.

What would settle it

Inspect the composite (5.2) for $P=P_{\mathrm{hc}}$ or $P=Q$: it asserts that the canonical map from hom-categories in the slice over $\mathbb{Y}$ to hom-categories over $\mathbb{X}$ is an isomorphism of categories. A concrete test is to take a small virtual double category with one nontrivial multicell as the domain and verify the counit composite is bijective on objects and fully faithful; any failure at even one multicell boundary would refute Proposition 5.5 and hence the paper's route to Theorem 7.10.

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is Theorem 7.10: the 2-functor $\mathrm{Enr}\colon\mathbf{VDBL}\to\mathbf{2\text{-}CAT}$ is familial. The route is a factorization $\mathrm{Enr}=V\circ\mathbb{Mod}\circ\mathbb{Mat}$, where $\mathbb{Mat}$ is a polynomial 2-functor induced by the discrete opfibration $P_{\mathrm{hc}}\colon(\mathrm{Set}_*)_{\mathrm{hc}}\to\mathrm{Set}_{\mathrm{hc}}$, and both $\mathbb{Mod}$ and $V$ are right 2-adjoints. The enabling result is Proposition 5.5: every discrete opfibration between virtual double categories is powerful, so pullback along it has an explicitly constructed right 2-adjoint $Q_P$. This makes the polynomial presentation possible and also yields the families 2-functor $\mathbb{Fam}$, built from the analogous universal discrete opfibration $Q\colon\mathbb{Span}_*\to\mathbb{Span}$. Along the way the paper gives an explicit left adjoint $\mathbb{L}$ for $\mathrm{Enr}_1$, shows the profunctor virtual double category $\mathbb{A}\text{-}\mathbb{Prof}$ is familial, and derives a formal pullback construction of $\mathbb{A}$-categories from families.

Load-bearing premise

The paper's main theorem rests on Proposition 5.5, the claim that every fibration-like map (a discrete opfibration) between virtual double categories is powerful, meaning pullback along it has a right adjoint built by an explicit construction. If that construction is flawed for the two specific maps used — pointed sets over sets and pointed spans over spans — then the matrix and families 2-functors need not be polynomial, and the main theorem would not follow by this route.

Editorial extensions

If this is right

$\mathrm{Enr}\colon\mathbf{VDBL}\to\mathbf{2\text{-}CAT}$ is a parametric right 2-adjoint, so the slice functor $\mathrm{Enr}_1$ has an explicit left adjoint $\mathbb{L}$; every 2-category over $\mathrm{Set}$ freely generates a virtual double category of enrichment.
Since familial 2-functors preserve bicategorical pullbacks and classes of fibrations, the 2-category of categories enriched over a virtual double category inherits these limit and fibration properties.
The factorization $\mathrm{Enr}=V\circ\mathbb{Mod}\circ\mathbb{Mat}$ identifies $\mathbb{A}$-categories with horizontal monads in $\mathbb{A}$-matrices, so the profunctor construction $\mathbb{A}\text{-}\mathbb{Prof}$ is itself familial.
The families 2-functor $\mathbb{Fam}$ is familial, and the pullback description in Theorem 8.5 gives a formal construction of $\mathbb{A}$-categories from $\mathbb{Fam}(\mathbb{A})$ and internal categories in $\mathrm{Set}$.
Enrichment over pseudo double categories is also familial, because the left adjoint $\mathbb{L}$ factors through representable virtual double categories (Remark 3.2).

Reading between the lines

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

The failure over bicategories (Remark 3.3) suggests that the parametric-right-adjoint property is not intrinsic to enrichment; it is created by the virtual double category structure, so the boundary between good and bad behaviour is sharp.
The explicit $Q_P$ construction offers a template: any universal discrete opfibration in a pullback-rich 2-category should induce a familial families 2-functor, a pattern the authors indicate can be pushed to general T-categories.
One testable consequence not developed in the paper is computational: because $\mathbb{Mat}$ and $\mathbb{Fam}$ are polynomial, concrete descriptions of $\mathbb{A}\text{-}\mathbb{Prof}$ and $\mathbb{A}$-$\mathrm{Cat}$ could be extracted from the pullback formulas for explicit bases such as spans or sets.

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.

Desk Editor's Note

read the letter

The real result here is the one advertised: Enr: VDBL → 2-CAT is familial, not just a parametric right 2-adjoint, and the proof is sound. The reader's conditional verdict is fair, but the condition is minor. Theorem 3.1's proof is omitted, but the authors explicitly say it can be obtained by combining later results, and it is not used in the proof of Theorem 7.10. I would not hold the paper hostage to that omission.

What is genuinely new: the familiality theorem itself, the constructions of 𝕄𝕒𝕥, 𝔽𝕒𝕞, and 𝔼𝕝𝕥 for virtual double categories, the universal discrete opfibration in VDBL, and the negative results for bicategorical and monoidal enrichment. The decomposition Enr = V ∘ 𝕄𝕠𝕕 ∘ 𝕄𝕒𝕥 is clean and does real work: 𝕄𝕒𝕥 is shown to be polynomial via Proposition 5.5, hence familial, while 𝕄𝕠𝕕 and V are right adjoints. The paper is careful with size and with the distinction between representable discrete opfibrations and the stronger Burroni–Leinster notion.

The softest spot is Proposition 5.5. The explicit construction of Q_P is detailed, and the claimed isomorphism (5.2) is credible — the inverse sends a morphism K to its componentwise actions on fibers, with uniqueness coming from the discrete opfibration conditions. But the verification is compressed into the phrase 'straightforward to check', and this is the load-bearing step for 𝕄𝕒𝕥 being polynomial. I could not find a flaw, and the stress-test note independently could not either. So this is the place a referee should look carefully, but I do not treat it as a known defect.

Other omissions are minor: Theorem 3.1's proof is absent, and there are a handful of 'evident' verifications in Sections 6–8. None of these affect Theorem 7.10. The citation pattern is appropriate: [FL24] is where the motivating question comes from, and the in-preparation papers [FL25a, FL25b] are flagged as such. The paper is not circular and introduces no ungrounded entities.

Who is this for: anyone in enriched category theory, generalized multicategories, or formal category theory. It strengthens the case that virtual double categories are the right setting for enrichment, and the new 𝔽𝕒𝕞/𝔼𝕝𝕥 constructions should be useful. A serious referee should engage. The paper deserves peer review, and if Proposition 5.5 checks out under scrutiny — which I expect — the main theorem will stand.

Referee Report

0 major / 5 minor

Summary. The paper studies the 2-functor Enr : VDBL → 2-CAT that sends a virtual double category to its 2-category of enriched categories. The central theorem (Theorem 7.10) states that Enr is familial, hence a parametric right 2-adjoint, and consequently preserves bicategorical pullbacks and various classes of fibrations. The proof decomposes Enr as V ∘ 𝕄𝕠𝕕 ∘ 𝕄𝕒𝕥, where 𝕄𝕒𝕥 is a polynomial 2-functor induced by the forgetful discrete opfibration (Set*)hc → Sethc, and 𝕄𝕠𝕕 and V are right 2-adjoints relating virtual double categories, unital virtual double categories, and 2-categories. The paper also constructs a families 2-functor 𝔽𝕒𝕞 : VDBL → VDBL and an associated elements 2-functor 𝔼𝕝𝕥, and shows that the discrete opfibration Phc is obtained as a pullback of the universal one Q : 𝕊𝕡𝕒𝕟∗ → 𝕊𝕡𝕒𝕟.

Significance. If the main results hold, the paper gives a satisfying formal framework for enrichment over virtual double categories, strengthening the earlier results for bicategories and providing a clean factorisation of Enr into a polynomial 2-functor and right adjoints. The explicit construction of the right adjoint Q_P in Proposition 5.5 and the detailed description of the families construction are valuable contributions that will likely be useful beyond the paper's immediate setting. The negative results of Section 3 (non-parametric-right-adjointness for bicategories and monoidal categories) are also informative. The paper is largely self-contained and builds on standard references, with the main proofs spelled out in considerable detail.

minor comments (5)

[Section 3 (Theorem 3.1)] The proof of Theorem 3.1 is omitted with the explanation that the adjunction can be obtained from later results; since the existence of the left adjoint is indeed subsumed by Theorem 7.10, this is not a gap in the main theorem, but the explicit description of 𝕃F should either be proved or accompanied by a precise reference to where the details appear.
[Section 5 (Proposition 5.5 and Eq. (5.2))] The verification that the composite (5.2) is an isomorphism of categories is compressed into 'straightforward to check'; spelling out the inverse bijection from a morphism K : P^*B → A over X to the induced map B → Q_P A over Y would make the load-bearing step of the paper easier to verify.
[Section 7.3 (Theorem 7.10)] The identification of V∘𝕄𝕠𝕕∘𝕄𝕒𝕥 with Enr is asserted with a reference to [CS10, Example 6.4] and the adjunction 𝕍 ⊣ V is said to be 'straightforward'; a short explicit check of the correspondence between 𝔸-natural transformations and cells of the form (7.4) would strengthen the final step.
[Section 8 (Proposition 8.6)] The notation in the proof of Proposition 8.6, in particular '𝔼𝕝𝕥𝕏. P^P' in diagram (8.6), is difficult to parse; please clarify the notation and the composition of 2-functors involved.
[Section 6 (Remark 6.1)] The assertion that the composite (−)he∘(−)vert is 1he×(−) and that its right adjoint is exponentiation by 1he is stated without proof; a brief justification or reference would be helpful.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found: the familiality proof is self-contained, and the only self-citations are motivational or ancillary.

full rationale

The central claim, Theorem 7.10, is derived from the factorization Enr = V ∘ 𝕄𝕠𝕕 ∘ 𝕄𝕒𝕥 displayed in (1.4). Each factor is established independently: 𝕄𝕒𝕥 is polynomial via the discrete opfibration Phc, whose powerfulness is proved by an explicit construction in Proposition 5.5, with Q_P built and the isomorphism (5.2) asserted directly rather than imported from the conclusion; 𝕄𝕠𝕕 and V are right adjoints constructed in Section 7 with explicit unit/counit data (Inc, Und, 𝕍, V) and triangle identities checked in Propositions 7.5–7.6 and via [CS10, Proposition 6.1]. Familiality then follows by the closure of familial 2-functors under composition, which is cited from [Web07] and Proposition 4.7. The proof does not define the conclusion into the premises: Q_P is constructed, not assumed; Enr is not assumed familial; and the composite factorization is verified rather than stipulated. The self-citation [FL24] appears only as motivation for the question, and the forward references [FL25a] and [FL25b] are not load-bearing. The omitted proof in Theorem 3.1 ('We omit the details as one can also obtain the 2-adjunction ... by combining the results proved in what follows') is a genuine proof-completeness gap, and the key assertion in Proposition 5.5 that (5.2) is an isomorphism is left as 'straightforward', but neither is a circular step nor is Theorem 3.1 used in the proof of Theorem 7.10. Therefore no derivation step reduces by construction to its own inputs.

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

No invented entities in the sense of ungrounded postulates. The new mathematical constructions (𝕄𝕒𝕥, 𝔽𝕒𝕞, 𝔼𝕝𝕥, 𝕃) are explicitly defined and are the paper's results, not hidden inputs. They have independent evidence in the form of explicit definitions, proofs of their universal properties, and comparison to known constructions in representable cases (Remarks 8.7, 8.8).

assumptions (5)

standard math Two Grothendieck universes U1 ∈ U2; small/large sets and categories are defined accordingly.
Stated in the Convention on size at the end of Section 1; standard in category theory.
domain assumption VDBL has a terminal object and pullbacks, so polynomial 2-functors and slices VDBL/Y are available.
Used throughout Sections 4-8; the paper treats pullbacks and slices in VDBL as standard (e.g., in the definition of 𝕄𝕒𝕥 and 𝔽𝕒𝕞).
standard math Weber's results on parametric right 2-adjoints, familial 2-functors, and polynomials: Proposition 4.7 (polynomial 2-functor from a powerful representable discrete opfibration is familial) and closure/composition properties.
Invoked as black boxes in the proofs of Theorem 6.2, 7.7, 7.10, and 8.1. These are from Weber (2007, 2015).
standard math Identification of virtual double categories with T-categories for the free category monad T on Gph (Burroni, Leinster).
Used in Remarks 2.2 and 5.2 to interpret discrete opfibrations as pullbacks in Gph; the paper cites Burroni (1971) and Leinster (2004).
standard math The 2-adjunctions (−)vert ⊣ (−)hc and the CS10 results on 𝕄𝕠𝕕 and V (e.g., that the composite V ∘ 𝔼𝕟𝕣 is isomorphic to Enr).
Used to construct the factorization (1.4) and Theorem 7.10; these are prior results by Cruttwell-Shulman and Leinster, or proved in the paper with standard verifications.

how reviews work

0 comments

Cite this review

Pith. "Pith review of The familial nature of enrichment over virtual double categories." pith.science (2026). https://pith.science/paper/U3AXKDDV

@misc{pith2026250705529,
  author       = {Pith},
  title        = {Pith review of: The familial nature of enrichment over virtual double categories},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/U3AXKDDV}},
  note         = {Machine review of arXiv:2507.05529}
}

read the original abstract

Originally enriched categories were defined over a monoidal category, but it was gradually realized that important examples can only be included when one enriches over more general structures such as bicategories and virtual double categories. We show that, as well as allowing more examples, working over virtual double categories also gives better formal properties. We study the 2-functor sending a virtual double category to the 2-category of categories enriched over it. We show that this is a parametric right 2-adjoint, and in fact is familial. We also show how a ``families construction'' for virtual double categories can be used to give a formal construction of the 2-category of categories enriched over a virtual double category.

Discussion (0). Sign in 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

Exponentiable virtual double categories and presheaves for double categories
math.CT 2025-08 conditional novelty 7.0 of 10

Every pseudo double category is exponentiable, and the virtual double category of lax functors Lax(A,B) is isomorphic to the virtual double category Mod(B^A) of monads and modules.

Reference graph

Works this paper leans on

26 extracted references · 25 canonical work pages · cited by 1 Pith paper

[1]

The nerve theorem for relative monads

Nathanael Arkor and Dylan McDermott. The nerve theorem for relative monads. Theory Appl. Categ. , 43:Paper No. 13, 403--454, 2025

work page 2025
[2]

Betti, A

R. Betti, A. Carboni, R. Street, and R. Walters. Variation through enrichment. J. Pure Appl. Algebra , 29:109--127, 1983

work page 1983
[3]

A unified approach to the construction of categories of games

Nathan James Bowler. A unified approach to the construction of categories of games . PhD thesis, University of Cambridge, 2011

work page 2011
[4]

T -cat \'e gories (cat \'e gories dans un triple)

Albert Burroni. T -cat \'e gories (cat \'e gories dans un triple). Cah. Topologie G \'e om. Diff \'e r. Cat \'e goriques , 12:215--321, 1971

work page 1971
[5]

Restriction categories as enriched categories

Robin Cockett and Richard Garner. Restriction categories as enriched categories. Theor. Comput. Sci. , 523:37--55, 2014

work page 2014
[6]

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

work page 2010
[7]

The oplax limit of an enriched category

Soichiro Fujii and Stephen Lack. The oplax limit of an enriched category. Theory Appl. Categ. , 40:Paper No. 14, 390--412, 2024

work page 2024
[8]

A G iraud-- C onduch\'e condition for generalized multicategories, 2025

Soichiro Fujii and Stephen Lack. A G iraud-- C onduch\'e condition for generalized multicategories, 2025. in preparation

work page 2025

Show all 26 references

[9]

Nerves of generalized multicategories, 2025

Soichiro Fujii and Stephen Lack. Nerves of generalized multicategories, 2025. in preparation

2025
[10]

Pasting diagrams in n -categories with applications to coherence theorems and categories of paths

Michael Johnson. Pasting diagrams in n -categories with applications to coherence theorems and categories of paths . PhD thesis, University of Sydney, 1987

1987
[11]

Double categories of profunctors

Yuto Kawase. Double categories of profunctors. arXiv:2504.11099v3, 2025

2025 arXiv
[12]

Formal category theory in augmented virtual double categories

Seerp Roald Koudenburg. Formal category theory in augmented virtual double categories. Theory Appl. Categ. , 41:288--413, 2024

2024
[13]

Stephen Lack. Icons. Applied Categorical Structures , 18(3):289--307, 2010

2010
[14]

Generalized enrichment of categories

Tom Leinster. Generalized enrichment of categories. J. Pure Appl. Algebra , 168(2-3):391--406, 2002

2002
[15]

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
[16]

Coherent theories as double L awvere theories, 2009

Roberd Par\'e. Coherent theories as double L awvere theories, 2009. International Category Theory Conference (CT 2009)

2009
[17]

Yoneda theory for double categories

Robert Par\' e . Yoneda theory for double categories. Theory Appl. Categ. , 25:No. 17, 436--489, 2011

2011
[18]

Products in double categories, revisited

Evan Patterson. Products in double categories, revisited. arXiv:2401.08990v1, 2024

2024
[19]

Enriched indexed categories

Michael Shulman. Enriched indexed categories. Theory Appl. Categ. , 28:616--695, 2013

2013
[20]

The petit topos of globular sets

Ross Street. The petit topos of globular sets. J. Pure Appl. Algebra , 154(1-3):299--315, 2000

2000
[21]

Enriched categories and cohomology

Ross Street. Enriched categories and cohomology. Repr. Theory Appl. Categ. , (14):1--18, 2005. Reprinted from Quaestiones Math. 6 (1983), no. 1-3, 265--283, with new commentary by the author

1983
[22]

The comprehensive factorization of Burroni 's $ T $ -functors

Walter Tholen and Leila Yeganeh. The comprehensive factorization of Burroni 's $ T $ -functors. Theory Appl. Categ. , 36:206--249, 2021

2021
[23]

R. F. C. Walters. Sheaves and C auchy-complete categories. Cahiers Topologie G\'eom. Diff\'erentielle , 22(3):283--286, 1981. Third Colloquium on Categories, Part IV (Amiens, 1980)

1981
[24]

Familial 2-functors and parametric right adjoints

Mark Weber. Familial 2-functors and parametric right adjoints. Theory Appl. Categ. , 18:No. 22, 665--732, 2007

2007
[25]

Operads as polynomial 2-monads

Mark Weber. Operads as polynomial 2-monads. Theory Appl. Categ. , 30:Paper No. 49, 1659--1712, 2015

2015
[26]

Polynomials in categories with pullbacks

Mark Weber. Polynomials in categories with pullbacks. Theory Appl. Categ. , 30:533--598, 2015

2015

Pith tools

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

[1] [1]

The nerve theorem for relative monads

Nathanael Arkor and Dylan McDermott. The nerve theorem for relative monads. Theory Appl. Categ. , 43:Paper No. 13, 403--454, 2025

work page 2025

[2] [2]

Betti, A

R. Betti, A. Carboni, R. Street, and R. Walters. Variation through enrichment. J. Pure Appl. Algebra , 29:109--127, 1983

work page 1983

[3] [3]

A unified approach to the construction of categories of games

Nathan James Bowler. A unified approach to the construction of categories of games . PhD thesis, University of Cambridge, 2011

work page 2011

[4] [4]

T -cat \'e gories (cat \'e gories dans un triple)

Albert Burroni. T -cat \'e gories (cat \'e gories dans un triple). Cah. Topologie G \'e om. Diff \'e r. Cat \'e goriques , 12:215--321, 1971

work page 1971

[5] [5]

Restriction categories as enriched categories

Robin Cockett and Richard Garner. Restriction categories as enriched categories. Theor. Comput. Sci. , 523:37--55, 2014

work page 2014

[6] [6]

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

work page 2010

[7] [7]

The oplax limit of an enriched category

Soichiro Fujii and Stephen Lack. The oplax limit of an enriched category. Theory Appl. Categ. , 40:Paper No. 14, 390--412, 2024

work page 2024

[8] [8]

A G iraud-- C onduch\'e condition for generalized multicategories, 2025

Soichiro Fujii and Stephen Lack. A G iraud-- C onduch\'e condition for generalized multicategories, 2025. in preparation

work page 2025