Attributed C-sets in CatColab

Several levels in CatColab

• double theories, which are double categories, possibly with extra structure
  • called “logic” in the tool
• A theory has models
  • the main thing that you are editing in the tool
  • a model is a structure-preserving lax functor from the theory into the double category called $\mathbb{Set}$ or $\mathbb{Span}$
• A model can have instances
  • not implemented yet
  • in ACSets.jl: they are in the form of interlinked columnar tables
  • model vs. instances:
    • models are categorical structures, consists of objects and morphisms, possibly with functorial operations acting on them
    • instances are set-theoretical structures, consists of elements, possibly with functional operations acting on them

Here are a few examples. The “trivial,” but important and motivating, example is when the double theory is the point (the terminal double category). Then a model is a category, say $\mathsf{C}$, and an instance of that model is a copresheaf on $\mathsf{C}$, i.e., a functor $\mathsf{C} \to \mathsf{Set}$. So that how $\mathsf{C}$-sets fit in.
There is a double theory whose models are multicategories, i.e., typed operads. An instance is then a functor into the multicategory of sets and functions of several variables, i.e., an algebra of the operad.

• related:
  • theory, model
  • mentioned: ascet