Central category

Syntax

C ::= ...as before...
| central

Type system

C M : T in val

C M : T in central

C D : C' in val

C D : C' in central

Equations

The equations for central are the same as those for val, except that the following are not valid:

D (fn C P {M}) = fn C P {D M} (bv D bv P = Ø)
D (M1,...,Mn) = (D M1,...,D Mn)

Syntactic categories

We can construct the category central as for val. Because there are fewer axioms for central than for val, central is not a cartesian closed category. It is, however, symmetric monoidal, and has closed structure given by an adjunction (natural in X and Z):

val[X, Y Z] central[X Y, Z]

Graphical presentation

The graphical presentation of central is the same as for val, except that we lose some of the axioms on graphs. The symmetric monoidal axioms are still true, hence any graph isomorphic terms are still equal. We also still have beta- and eta-convertability.

There is no natural diagonal:

nor a natural terminal:

Currying is not natural wrt central morphisms:

Currying is natural wrt val morphisms:

=

Previous | Next