Layered Monoidal Theories II: Fibrational Semantics

Abstract

Layered monoidal theories provide a categorical framework for studying scientific theories at different levels of abstraction, via string diagrammatic algebra. We introduce models for three closely related classes of layered monoidal theories: fibrational, opfibrational and deflational theories. We prove soundness and completeness of these theories for the respective models. Our work reveals connections between layered monoidal theories and well-known categorical structures such as Grothendieck fibrations and displayed categories.

Figures (9)

• Figure 1: Left: A typical term in a layered theory. Right: An equation for the functor boundary.
• Figure 2: Rules for generating the basic terms of a layered signature
• Figure 3: 1-equations defining monoidal functors inside the fibres
• Figure 4: The structural 2-equations. Here $\mathsf{id}_T$ and $\mathsf{id}_S$ are the identity terms on the types $T$ and $S$, while $\mathsf{id}_{\varepsilon}$ is the identity term on $\varepsilon : \varepsilon$ obtained by the rule \ref{['term:ext-unit']}.
• Figure 5: Rules for generating the opfibrational terms

Theorems & Definitions (129)

• Definition 2.1: Opcartesian map
• Remark 2.2: Weakly opcartesian map
• Definition 2.3: Opfibration
• Remark 2.4: Preopfibration
• Proposition 2.5
• Remark 2.6
• Definition 2.7: Fibration
• Example 2.8: Family fibration
• Definition 2.9: Morphism of (op)fibrations
• Proposition 2.10