## MILL, BMCCs, and dinatural transformations

I’m looking at multiplicative intuitionistic linear logic (MILL) right now and figuring out how it’s related to braided monoidal closed categories (BMCCs).

The top and bottom lines in the inference rules of MILL are functors that you get from the definition of BMCCs, so they exist in every BMCC. Given a braided monoidal category **C**, the turnstile symbol

is the external hom functor (that is, is the set of morphisms from to ). Inference rules are natural or dinatural transformations.

Let be a category; then a natural transformation between two functors

can be seen as a functor from the category (), where is the category with two objects labelled and and one nontrivial arrow between them, labelled

For every morphism in we get a commuting square in :

that maps to a commuting square in

In other words, it assigns to each object x in **C** a morphism α_x in **D** such that the square above commutes.

Now consider the case where we want a natural transformation α between two functors

op F,G:C×C->D.

Given f:x->y, g:s->t, we get a commuting cube in (**A** × **C**^op × **C**) that maps to a commuting cube in **D**.

G(1_t,f) Gtx -------------------> Gty 7| 7| / | / | α_tx / |G(g,1_x) α_ty / | / | / | G(g,1_y) / | / | / V G(1_s,f) / V / Gsx -------------- /---> Gsy / 7 / 7 / / / / / / / / / / F(1_t,f) / / α_sy Ftx -------------------> Fty / | / | / | / | / F(g,1_x) | / α_sx | F(g,1_y) | / | / | / | / V/ F(1_s,f) V/ Fsx -------------------> Fsy

This is bigger, but still straightforward.

To get a dinatural transformation, we set g:=f and then choose a specific route around the cube so that both of the indices are the same on α.

....................... Gyy .. 7| . . / | . . α_yy / | . . / | G(f,1_y) . . / | . . G(1_x,f) / V . Gxx -------------- /---> Gxy . 7 / . . / / . . / / . . / F(1_y,f) / . Fyx -------------------> Fyy . | / . . | / . . F(f,1_x) | / α_xx . . | / . . | / . . V/ .. Fxx .......................

In other words, a dinatural transformation α: F -> G assigns to each object x a morphism α_xx such that the diagram above commutes.

Dinatural transformations come up when you’re considering two of MILL’s inference rules, namely

x ⊢ y y ⊢ z ------- (Identity) and --------------- (Cut) x ⊢ x x ⊢ z

These two have the same symbol appearing on both sides of the turnstile, x in the Identity rule and y in the Cut rule. Setting

Fxy = * ∈Set,

where * is the one-element set, and

Gxy = x ⊢ y ∈Set,

the Identity rule specifies that given f:x->y we have that f o 1_x = 1_y o f:

.......................y ⊢ y .. 7| . . / | . . α_yy / | . . / | 1_y o f . . / | . . f o 1_x / V . x ⊢ x ------------- /--> x ⊢ y . 7 / . . / / . . / / . . / 1 / . * ---------------------> * . | / . . | / . . 1 | / α_xx . . | / . . | / . . V/ .. * ........................

where

α_xx:* -> x ⊢ x * |-> 1_x

picks out the identity morphism on x.

In the Cut rule, we let j:x->s, k:t->z, and f:s->t,

F(t,s) = (x ⊢ s, t ⊢ z) j f k F(1,f) = (x ---> s ---> t, t ---> z) j f k F(f,1) = (x ---> s, s ---> t ---> z) G(s,t) = x ⊢ z

and consider the diagram for a morphism f:s->t in C.

.......................x ⊢ z .. 7| . . / | . . composition / | . . / | 1 . . / | . . 1 / V . x ⊢ z ------------- /--> x ⊢ z . 7 / . . / / . . / / . . / F(f,1) / . (x ⊢ s, t ⊢ z) -------> (x ⊢ s, s ⊢ z) | / . . | / . . | / composition . . F(1,f) | / . . | / . . V/ .. (x ⊢ t, t ⊢ z) .................

which says that composition of morphisms is associative.

leave a comment