CatColab

Depending on your needs, you can access different types of documentation:

• General Users: Use the guides for fundamentals and general usage.
• Software Developers: Access the Developer docs for API information and the GitHub repository for source code.
• Mathematical Research: Consult the Mathematical docs and the Bibliography of suggested reading for formal references.

The catcolab-document-methods package provides TypeScript-compatible methods for operating on document data. Because the core document type definitions are exported from a Rust crate, they only contain data structures. This package provides the functional logic to manipulate those structures in a TypeScript environment.

Key characteristics:

• Environment Agnostic: Unlike the frontend package, this package has no dependencies on UI libraries. It can be used in any JavaScript environment, including headless environments (e.g., Node.js, server-side scripts, or CLI tools).
• Dependency: It extends the types defined in catcolab-document-types.

CatColab uses two primary deployment environments. The frontend is hosted on Netlify, while the backend runs on separate AWS EC2 instances.

• Production (catcolab): Runs the latest tagged release. Frontend at catcolab.org, backend at backend.catcolab.org.
• Staging (catcolab-next): Runs the main branch. Frontend at next.catcolab.org, backend at backend-next.catcolab.org.

Note on PR Previews: Netlify preview links only contain frontend changes and connect to the staging backend (backend-next.catcolab.org). Previews may be unreliable if the Pull Request includes backend changes.

A modal double theory extends simple double theories by incorporating modalities (like list modalities) using monads.

• Simple Case: A modal double theory is a monad $(\dbl{T}, T)$ in the 2-category of strict almost representable VDCs ($\arVDCstrict$), where $\dbl{T}$ is a virtual equipment. A model is a strict morphism of monads $M: (\dbl{T}, T) \to (\SSet, S)$.
• General Case (Mode Theory): A mode theory is a strict monoidal category $\cat{M}$. A modal double theory with mode theory $\cat{M}$ is a 2-functor $\cal{T}: \mathbf{B}(\cat{M}) \to \arVDCstrict$ from the delooping of $\cat{M}$ to the 2-category of strict almost representable VDCs, such that $\cal{T}(*)$ is a virtual equipment. A model is a 2-natural transformation between the theory $\cal{T}$ and a target 2-functor $\cal{S}$.

DoubleTT is a type theory designed for specifying models of double theories within CatColab. It combines standard dependent type theory (such as dependent records) with specialized rules for double-categorical models, including type constructors for object and morphism types.

Its primary purpose is to enable the composition of models using the variable sharing paradigm (formalized by the category-theoretic concept of colimit). This allows users to compose models by identifying their objects.

An ontology log, or olog, is a semi-formal representation of knowledge or a viewpoint. It uses a diagrammatic language consisting of:

• Types: Represented as boxes.
• Aspects: Represented as arrows connecting types.

Ologs are considered semi-formal because while the types and aspects provide a formal structure, they are typically labeled with natural language. This allows an arrow to be read from left to right as a grammatical sentence. Ologs serve as a lightweight stepping stone toward more precise models, such as database schemas.

To describe ODE systems outside the polynomial class (e.g., using exponential or sine functions), you can use a cartesian double theory based on a Lawvere theory $\mathcal{T}$:

1. Embed the Lawvere theory: Include $\mathcal{T}$ in the tight category of the double theory via an object $\text{Term}$.
2. Define State: Include an object $\text{State}$ and an arrow $\text{State} \to \text{Term}$.
3. Define Contributions: Include a proarrow $\text{Contrib}: \text{Term} \mathrel{\mkern-3mu\vdash} \text{State}$.

An f.f.g. model consists of finite sets of state variables and exogenous variables (generators of type $\text{Term}$), an embedding of state variables into terms, and contributions $c: \text{Contrib}(v, x)$ interpreted as $\dot x \mathrel{+\mkern-3mu=} k_c \cdot v$, where $v$ is a term from the Lawvere theory.

Symmetric monoidal categories are modeled as the modal double theory of generalized monoidal categories using the symmetric variant of the list double monad, $T = \text{List}_{\text{bij}}$.

In the internal language, the symmetry isomorphism $\sigma_{X,Y}: X \otimes Y \to Y \otimes X$ is constructed by:

1. Forming a list with the swapped elements: $\Gamma \mid [x,y]: [X,Y] \vdash_{\text{List}{\text{bij}} \text{Hom}{\mathcal{X}}} [y,x]: [Y,X]$ using the swap permutation $\sigma: [2] \xrightarrow{\cong} [2]$.
2. Applying the cell $\text{Hom}{\otimes}$ induced by the tensor $\otimes: \text{List}{\text{bij}} \mathcal{X} \to \mathcal{X}$.

This results in the term: $\Gamma \mid (x,y): X \otimes Y \vdash_{\text{Hom}_{\mathcal{X}}} (y,x): Y \otimes X$.

In CatColab, a model using the informal logic contains no formal structured content. It only supports the rich text allowed in any standard model notebook.

When you create a new model, it is assigned to the informal logic by default. This allows for immediate typing and note-taking, but if you need to add structured content (such as formal mathematical models or specific data structures), you must switch the model to a different, non-trivial logic.