Instances of Models of Double-Categorical Theories

Basic Information

• Paper ID: 2510.08861
• Title: Instances of models of double-categorical theories
• Authors: Kevin Carlson, Evan Patterson (Topos Institute)
• Classification: math.CT (Category Theory)
• Submission Date: October 9, 2025
• Paper Link: https://arxiv.org/abs/2510.08861

Abstract

This paper makes joint contributions to the study of categorical database theory and higher-order morphisms between double categories. The common thread is the concept of instances or right modules, which the authors generalize from functors from ordinary categories to Set to models of (Cartesian) double theories. This provides an instance concept for objects such as categories with monads or (symmetric) multicategories, and in the latter case recovers multifunctors to Set. The authors also prove that instances of models are equivalent to an appropriate notion of discrete opfibrations over that model, which cannot be recovered as representable discrete opfibrations in the model 2-category. Finally, they provide a comprehensive factorization system with these discrete opfibrations as the right class.

Research Background and Motivation

Problem Context

1. Development needs of double category theory: Modern weak double category theory originated from the collaboration of Paré and Grandis, whose "main idea" was to study arrows in pseudo-double categories that are either too lax (such as profunctors, spans, relations) or too strict (such as adjunctions) to admit limits, associating them with more ordinary (horizontal) arrows.
2. Requirements of categorical database theory: Spivak and Kent pioneered categorical database theory, viewing small categories C as ontologies or database schemas, and concrete databases as C-sets. This idea has been extended in applied category theory, including algebraic databases and attributed C-sets.
3. Software application drivers: The CatColab application developed by the authors at Topos Institute is based on Paré's theory of lax double functors to Span, interpreting small double categories as double (Lawvere) theories and structure-preserving lax functors as models of theories.

Core Problems

The traditional instance concept (such as C-sets corresponding to modules I 7→ C) cannot be directly generalized in general double theories. When X is a model of a double theory admitting non-trivial proarrows, although the model 1 is terminal with respect to tight morphisms of the model, it is sufficiently rich to act non-trivially on the left side of the module.

Research Motivation

The need to find the correct instance concept for double theory models such that it can:

1. Generalize the copresheaf concept for ordinary categories
2. Apply to complex structures such as categories with monads and multicategories
3. Recover multifunctors to Set in the multicategory case
4. Provide equivalence with discrete opfibrations

Core Contributions

1. Defined the instance concept for double theory models: Generalized the instance concept from ordinary categories to general double theories, addressing technical difficulties by requiring "I acts trivially on the left."
2. Established presheaf-type representation of instances: Proved that the instance category of any model X is equivalent to the category of functors κ(X) → Set, where κ(X) is the "collage" of X.
3. Established equivalence between instances and discrete opfibrations: The main theorem proves equivalence between instances of a model and discrete opfibrations over that model, generalizing the classical equivalence between copresheaves and discrete opfibrations over categories.
4. Constructed comprehensive factorization systems: Using local representability of the model category, constructed a comprehensive factorization system with discrete opfibrations as the right class.
5. Generalized to the Cartesian case: Extended all results to Cartesian double theories, covering important examples such as Lawvere theories and symmetric multicategories.

Methodology Details

Core Task Definition

The central task of this paper is to define an appropriate instance concept for models X of double theories D such that it satisfies:

• Generalizes the copresheaf concept for ordinary categories
• Is equivalent to the discrete opfibration concept
• Forms a presheaf-type category

Definition of Instances

Preliminary Definition (Definition 2.1)

Let D be a double theory and E be a double category with terminal object I. D has a terminal model I in E. An instance of model X is a module H: I 7→ X satisfying "I acts trivially on the left," meaning all laxators of the following form are identities:

I    I    X(z)
 \   |   /
  \  |  /
   \ | /
I ---+--- X(z)

Simplified Definition (Definition 2.3)

After structural simplification, an instance H consists of:

• For each object d ∈ D, a proarrow Hd: I 7→ Xd
• For each tight morphism f: d → d', a cell Hf
• For each proarrow m: d 7→ d', an action cell Hm

Satisfying functoriality, naturality, associativity, and unitality axioms.

Collage Construction (Construction 2.7)

For a Span-valued model X: D → Span, define its collage κ(X) as a category:

• Objects: For each d ∈ D and x ∈ X(d), obtain an object x
• Morphisms: Generated by tight morphisms and lax morphisms
• Relations: Preserving composition, naturality, etc.

Discrete Opfibrations

Definition (Definition 3.2)

A model morphism p: E → B is a discrete opfibration if for every proarrow m: x 7→ y, the square

⊤(Em) → Ex
  ↓      ↓
⊤(Bm) → Bx

is a pullback.

Main Equivalence Theorem

Theorem 3.7

There exists an equivalence ∇: Dopf(B) ⇄ Inst(B): ∫, where:

• Dopf(B) is the category of discrete opfibrations over B
• Inst(B) is the category of instances of B
• ∫H is called the element model of instance H

Technical Innovations

1. Generalization of the Instance Concept

The "left trivial action" condition cleverly resolves technical difficulties in defining instances in general double theories, avoiding problems with direct generalization in cases with non-trivial proarrows.

2. Innovation in Collage Construction

The κ construction provides a systematic method for "flattening" double category structures into ordinary categories, enabling the use of classical presheaf theory.

3. Generalization of Discrete Opfibration Concept

Generalizes the classical discrete opfibration concept to double theory models, requiring pullback conditions at each proarrow.

4. Comprehensive Factorization Systems

The factorization system constructed using local representability provides a powerful tool for studying model morphisms.

Experimental Setup

Theoretical Verification

This paper is primarily pure mathematical theory work, verified through:

Key Example Verification

1. Instances of categories: Verifies recovery of classical C-sets in the terminal double theory case
2. Instances of monads: Proves that instances of categories with monad T: X → X are X-sets H with natural transformation Hη: H → H∘T
3. Instances of multicategories: Recovers multifunctors M → Set in the Cartesian case

Construction Verification

Through detailed diagram chasing and axiom verification:

• Functoriality of κ construction
• Mutual inverse property of equivalences ∇ and ∫
• Orthogonality of factorization systems

Experimental Results

Main Results

Proposition 2.8

For models X: D → Span of simple double theories, the instance category Inst(X) is equivalent to the functor category Cat(κX, Set).

Theorem 3.7 (Main Theorem)

For a fixed model B of simple double theory D, there exists an equivalence ∇: Dopf(B) ⇄ Inst(B): ∫ between the category of discrete opfibrations over B and the category of instances of B.

Proposition A.2

The model category Lax(D, Span) of simple double theories is locally representable.

Generalization Results

Theorem 4.5

For Cartesian double theories, the equivalence restricts to an equivalence between Cartesian instances and Cartesian discrete opfibrations.

Corollary 4.6

Cartesian model categories admit an orthogonal factorization system with discrete opfibrations as the right class.

Application Results

The applicability of the theory is verified through concrete examples:

• Multicategory instances recover multifunctors M → Set
• Algebraic profunctors as instances of modal theories
• Unified treatment of symmetric and co-Cartesian multicategories

Related Work

Foundations of Double Category Theory

• Weak double category theory by Paré and Grandis
• Yoneda theory and module concepts for double categories by Paré
• Generalized multicategory virtual equipments by Cruttwell and Shulman

Categorical Database Theory

• Pioneering work by Spivak and Kent
• Attributed C-sets by Patterson et al.
• Algebraic databases by Schultz et al.

Opfibration Theory

• Comprehensive factorization systems by Street and Walters
• Initial functors in ∞-cosmoi by Riehl and Verity
• General theory of representable discrete opfibrations in 2-categories

Conclusions and Discussion

Main Conclusions

1. Successfully generalized the instance concept to general double theory models
2. Established fundamental equivalence between instances and discrete opfibrations
3. Provided a comprehensive framework for studying double theory model morphisms
4. Provided theoretical foundations for applied software such as CatColab

Limitations

1. The κ construction is neither full nor faithful nor conservative, limiting its utility in studying properties of Lax(D, Span)
2. The instance category does not depend on almost all data of the model
3. Currently focuses mainly on Span-valued models; other cases require further research

Future Directions

1. Modal theories: The paper previews modal virtual double theories as a more convenient foundation for encoding non-simple double Lawvere theories
2. Virtual equipments: Consider extending the theory to virtual equipment settings
3. Higher-order structures: Study higher-order double category structures and their instance theories

In-Depth Evaluation

Strengths

1. Strong theoretical innovation: Successfully resolves technical difficulties in defining instances for double theory models
2. Complete structure: Forms a complete theoretical system from definitions through main equivalence theorems to application examples
3. Technical depth: Involves multiple deep techniques including double category theory, opfibration theory, and local representability
4. Practical value: Provides solid theoretical foundations for categorical database theory and formal modeling software

Weaknesses

1. High technical threshold: Requires deep background in category theory, limiting the audience
2. Limitations of κ construction: Acknowledges that κ is neither full nor faithful, which may impact certain applications
3. Relatively few examples: While key examples are provided, more concrete application scenarios could be demonstrated

Impact

1. Theoretical contribution: Opens new directions for cross-disciplinary research between double category theory and categorical database theory
2. Practical value: Directly supports development of scientific modeling software such as CatColab
3. Reproducibility: Mathematical proofs are detailed and theoretical results are verifiable

Applicable Scenarios

1. Formal scientific modeling software development
2. Research in categorical database theory
3. Further development of double category theory
4. Applications of generalized multicategories and operads theory

References

This paper cites 51 important references, covering:

• Foundational literature in double category theory (Grandis & Paré, Verity, etc.)
• Categorical database theory (Spivak & Kent, etc.)
• Locally representable category theory (Adámek & Rosický, etc.)
• Opfibration and factorization system theory (Street & Walters, etc.)

This paper is an important theoretical contribution at the intersection of double category theory and categorical database theory, providing new perspectives and tools for understanding and applying double theory models. Its technical depth and theoretical completeness make it an important reference in this field.