Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Linearly Distributive Fox Theorem

Rose Kudzman-Blais

TL;DR

This work extends Fox’s theorem from cartesian categories to the realm of linearly distributive categories by introducing medial linearly distributive categories (MLDCs) and the medial rule, which interplays with the two monoidal structures via duoidal coherence. It develops the machinery of symmetric MLDCs, medial linear functors, and medial bimonoids to construct a right adjoint B[-] from the 2-category of symmetric MLDCs to cartesian-linearly distributive categories (CLDCs), establishing inc ⊣ B[-]. The main result, the Linearly Distributive Fox Theorem, characterizes CLDCs as symmetric MLDCs whose objects have coherent medial bimonoid structure, mirroring the classical Fox adjunction in a richer, two-monoidal setting. The framework leverages duoidal category theory to unify LDCs with duoidal interchanges, yielding a duoidal variant of Fox’s theorem and providing a robust categorical semantics for linear logic enriched with the medial rule.

Abstract

Linearly distributive categories (LDC), introduced by Cockett and Seely to model multiplicative linear logic, are categories equipped with two monoidal structures that interact via linear distributivities. A seminal result in monoidal category theory is the Fox theorem, which characterizes cartesian categories as symmetric monoidal categories whose objects are equipped with canonical comonoid structures. The aim of this work is to extend the Fox theorem to LDCs and characterize the subclass of cartesian linearly distributive categories (CLDC). To do so, we introduce medial linearly distributive categories (MLDC), medial linear functors, and medial linear transformations. The former are LDCs which respect the logical medial rule, appearing frequently in deep inference, or alternatively are the appropriate structure at the intersection of LDCs and duoidal categories.

Linearly Distributive Fox Theorem

TL;DR

This work extends Fox’s theorem from cartesian categories to the realm of linearly distributive categories by introducing medial linearly distributive categories (MLDCs) and the medial rule, which interplays with the two monoidal structures via duoidal coherence. It develops the machinery of symmetric MLDCs, medial linear functors, and medial bimonoids to construct a right adjoint B[-] from the 2-category of symmetric MLDCs to cartesian-linearly distributive categories (CLDCs), establishing inc ⊣ B[-]. The main result, the Linearly Distributive Fox Theorem, characterizes CLDCs as symmetric MLDCs whose objects have coherent medial bimonoid structure, mirroring the classical Fox adjunction in a richer, two-monoidal setting. The framework leverages duoidal category theory to unify LDCs with duoidal interchanges, yielding a duoidal variant of Fox’s theorem and providing a robust categorical semantics for linear logic enriched with the medial rule.

Abstract

Linearly distributive categories (LDC), introduced by Cockett and Seely to model multiplicative linear logic, are categories equipped with two monoidal structures that interact via linear distributivities. A seminal result in monoidal category theory is the Fox theorem, which characterizes cartesian categories as symmetric monoidal categories whose objects are equipped with canonical comonoid structures. The aim of this work is to extend the Fox theorem to LDCs and characterize the subclass of cartesian linearly distributive categories (CLDC). To do so, we introduce medial linearly distributive categories (MLDC), medial linear functors, and medial linear transformations. The former are LDCs which respect the logical medial rule, appearing frequently in deep inference, or alternatively are the appropriate structure at the intersection of LDCs and duoidal categories.

Paper Structure

This paper contains 25 sections, 59 theorems, 175 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Fox Theorem
  3. Monoidal Categories
  4. Comonoids
  5. Linearly Distributive Categories
  6. Definition, Mix and Examples
  7. Linear Functors and Transformations
  8. Cartesian Linearly Distributive Categories
  9. Duoidal Categories
  10. Definition, Symmetry and Examples
  11. Duoidal Functors and Transformations
  12. Cartesian and Cocartesian Duoidal Categories
  13. Medial Linearly Distributive Categories
  14. Medial Rule and Main Definition
  15. Symmetry
  16. ...and 10 more sections

Key Result

lemma 1

Given a cartesian category $(\cX, \times, \bone)$, every object $A$ in has a canonical unique cocommutative $\times$-comonoid structure and every arrow $f\,\colon A\rightarrow B$ in is a comonoid morphism with respect to these structures.

Figures (5)

  • Figure 1: Proof that $(\bot, \Delta_\bot, m)$ is a cocommutative $\otimes$-comonoid in Proposition \ref{['prop:alternative_SMLDC']}
  • Figure 2: Proof of the first equality in Proposition \ref{['prop:interaction_canonical_flip_medial_maps_linear_dist']}
  • Figure 3: Proof of the first diagram in Proposition \ref{['prop:interchange_canonicalflip_mix']}, where (smc) denotes the diagram holds in any SMC
  • Figure 4: Proof that $\partial^R$ is the inverse of $\delta^L$ in Proposition \ref{['prop:isomix_MLDC']}
  • Figure 5: Proof of the first equality in Proposition \ref{['prop:interaction_canonical_flip_medial_linear_functor']}

Theorems & Definitions (118)

  • remark 1
  • definition 1
  • lemma 1
  • lemma 2
  • lemma 3
  • theorem 1
  • corollary 1
  • corollary 2
  • definition 2
  • definition 3
  • ...and 108 more