Contents

category theory

# Contents

## Idea

So-called Trimble rewiring refers to a certain type of transformation on graphs which were introduced in Trimble’s thesis, intended to refine Kelly-Mac Lane graphs or classical proof nets in multiplicative linear logic so as to capture properties of the monoidal unit in symmetric closed monoidal categories. These unit-extended proof nets may be interpreted as morphisms in free symmetric monoidal closed categories, and it turns out that two unit-extended proof nets are interpretable as the same morphism if and only if they are “rewiring equivalent”.

Rewirings can be organized into a confluent and strongly normalizing rewrite system, where a rewrite called “directed rewiring”. The normal forms of graphs can then be used to state a full coherence theorem, extending the coherence theorem of Kelly and Mac Lane for symmetric monoidal closed categories.

The concept of rewiring equivalence extends to weakly distributive categories and $\ast$-autonomous categories as well, and likewise is used to give coherence theorems for these structures.

## Definition

(For now this is just the very rough idea. More details to come.)

Recall from proof net the notion of (cut-free) proof structure and the notion of (cut-free) proof net (a proof structure of the form $S(\pi)$ where $\pi$ is a sequent proof).

###### Definition

A unit-extended proof structure of type $\Delta \to B$ is a proof structure of type $\Delta \to B$ equipped with a function $u: Unit^-(\Delta^-, B^+) \to Subform(\Delta^-, B^+)$ from the set of negatively signed subformula occurrences of $I$ to the set of subformulas of $\Delta$ and $B$.

We draw such a unit-extended proof structure as a graph: the graph of the proof structure together with an edge from each occurrence $R$ of $I^-$ to $u(R)$. We think of this unit edge as connoting a subterm of the form $r t$, where $r$ is a variable term of type $I$ (a “scalar”), and $t$ is a term of type $u(R)$.

Let $UStruct(\Delta, B)$ denote the set of unit-extended proof structures of type $\Delta \to B$, and let $Proof(\Delta, B)$ denote the set of sequent proofs of the sequent $\Delta \vdash B$. We define a relation from $Proof(\Delta, B)$ to $UStruct(\Delta, B)$, i.e., a function

$Proof(\Delta, B) \to P(UStruct(\Delta, B))$

by induction along the sequent proof, as follows. (Details to be filled in. The most important sequent rule to consider is

$\Gamma(\frac\pi: \Delta, \Sigma \vdash A}\Delta, I, \Sigma \vdash A}\; unit_{-}$

where a related unit-extended proof net is obtained from a proof net for $\pi$ by introducing a fresh unit edge from the occurrence of $I^-$ introduced in the last step to any subformula of $\Delta, \Sigma \vdash A$. The other rules are straightforward.)

###### Definition

A unit-extended proof net is a proof structure that is related to some sequent deduction.

Theorem on graphical criterion for a unit-extended proof structure to be a unit-extended proof net, similar to the criterion of Danos-Regnier.

###### Definition

Two unit-extended proof nets $\gamma, \gamma'$ of type $\Delta \to B$ are rewiring-equivalent if there is a sequence of unit-extended proof nets $\gamma = \gamma_0, \gamma_1, \ldots, \gamma_n = \gamma'$ of type $\Delta \to B$ such that each successive pair of graphs $\gamma_i, \gamma_{i+1}$ differ only by a single unit edge $u(R)$.

Theorem that two sequent proofs $\pi, \pi'$ produce the same morphism in the free smc category $V[T]$ iff any two of their unit-extended proof nets $\gamma, \gamma'$ are rewiring-equivalent.

Notion of directed rewiring…

• Todd Trimble, Linear logic, bimodules, and full coherence for autonomous categories. PhD thesis, Rutgers University, 1994