A system of natural deduction for categories

We will present a system of natural deduction for categories, i.e., a system that includes discharge rules, and whose semantics (via a kind of Curry-Howard isomorphism) interprets terms as objects, morphisms, functors and natural transformations, plus the usual points and functions. The main novelty of that system is that it has discharge rules for forming functors and natural transformations — actually protofunctors and protonatural transformations, entities that behave only syntactically like functors and natural transformations.

The system is expressive enough to let us represent as relatively short terms things like the Yoneda Lemma and the fact that a category of the form Set^{C} has exponentials and a subobject classifier; the categorical constructions that prove those things can be read from the trees that deduce those terms, and it is easy to draw side to side to them other trees that show how each term would be written in the usual notation.

Usually we would choose “x” as the default name for a variable ranging over X, “y” for a variable ranging over Y, etc; we will allow “composite variable names”, so “(a, b)” will be our default name for a variable ranging over A × B, c → d our default name for one ranging over D^{C}, etc. We call this notation the notation of typical points, and the idea is that the name of a variable is the “name of the typical point” of the space in which that variable can take values. Generally — but now always — we will want to attributed related values to variables with related named — for example a being the first coordinate of (a, b).

The symbol E is used to mean “the space of”, in the sense of “the set of all possible values for”: we have x ∈ X, and X is considered as the “space of ‘x’s”: X = E_{x}. Following this idea, E_{(a,b)} = E_{a} × E_{b}, E_{c→d} = (E_{d})^{(E_{c})}, etc. In this way the uppercase letters become free for other uses, and we use fewer symbols. Obviously E_{x}, E_{a}, … can be seen as variables ranging over the class of all sets, whose values bear some relation with the values of x, a, … — namely that x ∈ E_{x}, a ∈ E_{a}, etc.

This notation for variables was chosen to make it convenient to “read aloud” construction trees. For example,

\begin{aligned}\begin{matrix}[a]^{1} & b \\ (a, b) \end{matrix} & (a, b) → c \\ & c \end{aligned} ; a → c ; 1

can be read aloud as: “from a value for a and a value for b we have a natural way to choose a value for (a, b)”... — note that currently we are only talking in terms of “\underline{a} value”, not of “\underline{the} value”; also, we will often say just “an a”, “a b”, etc, instead of the longer “a value for a”, etc. — ...“and given an (a, b) and a function (a, b) → c we have a natural choice for a c. So, the tree over the bar marked with the ‘1’ can be seen as an operation that from an a, a b and an (a, b) → c builds a c; for each b and (a, b) → c fixed this gives a function that takes an a and returns a c, that is, an a → c. So the big tree, with the top a “discharged”, denotes a natural way to build an a → c from a b and an (a, b) → c.”

The tree above is a “natural construction” for a → c from a b and an (a, b) → c; the formal definition is that a natural construction for β from α_{1}, …, α_{n} in a certain system is a tree with β in its root where only members of the list α_{1}, …, α_{n} can appear as “leaves” (i.e., as undischarged hypotheses), and where each bar is an application of a rule of the system.

Generally the list α_{1}, …, α_{n} and the rules of the system will be clear from the context, and then we say that a β has natural constructions if there is a natural construction for β from α_{1}, …, α_{n} in that system, and we say that β is well-defined (in symbols: wd(β)) if it has natural constructions and furthermore all its natural constructions give the same result, using the semantical interpretation of the rules and the values for α_{1}, …, α_{n}. The result of a natural construction for β is called a “natural value” for β; if β and γ are well-defined and have related names then their natural values will be related.

After introducing just a few other auxiliary symbols we will be ready to show a sample construction in the system of natural deduction for categories (“system NDC”, from now on). Just like a x → y is a function from E_{x} to E_{y}, an a → b is a morphism from O_{a} to O_{b}; if we have an O_{a} instead of an E_{a} it would generally make no sense to speak of “an a”. Cat_{a} is the category where O_{a} lives; on the presence of an a → b we must have Cat_{a} = Cat_{b}. An o_{A} is an object of the category A; a m_{A} is a morphism of the category A. A×B is the product of the categories A and B; an object of A×B is written like O[(a; b)] and corresponds to a pair (O_{a}, O_{b}). A ⇒ B is a category of functors; an o[A ⇒ B] is a functor from A to B, and a m[A ⇒ B] is a natural transformation between two such functors.

A functor is denoted by its action on names of objects, and its action on “unnamed” arrows (i.e., undecorated arrows — a →^{f} b is not undecorated) is inferred from its action on objects. For example, a ⇒ a^{F} takes O_{a} to O_{a^{F}}, O_{a′} to O_{a′}^{F}, a′ → a′′ to a′^{F} → a′′^{F}, and so on.

An “unnamed” natural transformation from a ⇒ a^{F} to a ⇒ a^{G} is written as a →^{•} (a^{F} → a^{G}); if all its image morphisms are isos, monics or epis we may include that information in the name of the natural transformation by replacing the ‘→’ by ‘↔’, ‘↪’ or ‘↠’ respectively.

The table below shows the main rules of system NDC. The full system is much larger than that, and most rules have restrictions — in Fmorf, for example, we must have Cat_{a′} = Cat_{a}.

{a → b \atop O[a]} src  {a → b \atop O[b]} tgt  {O[a] \atop a → a} id  \begin{matrix}a → b & b → c \\ a → c \end{matrix}

\begin{matrix}O[a] & a ⇒ a^{F} \\ O[a^{F}] \end{matrix} Fobj  \begin{matrix}a′ → a′′ & a ⇒ a^{F} \\ a′^{F} → a′′^{F} \end{matrix} Fmorf

2001nd-abs (typeset 2001jun27 06:49) edrx@mat.puc-rio.br

\begin{aligned}O[a] & a →^{•} (a^{F} → a^{G}) \\ & a^{F} → a^{G} \end{aligned} NTobj

\begin{matrix}[O[a]]^{1} & … \\ a^{F} → a^{G} \end{matrix} ; a →^{•} (a^{F} → a^{G}) 1 NTdisch  \begin{matrix}[a′ → a′′]^{1} & … \\ a′^{F} → a′′^{F} \end{matrix} ; a ⇒ a^{F} ; 1 Fdisch

The discharging rules Fdisch and NTdisch form protofunctors and proto-NTs instead of functors and NTs; a protofunctor is an operation that behaves syntactically like a functor, and, likewise, a proto-NT behaves syntactically like a natural transformation. A protofunctor that respects identities and composition of morphisms is a functor; a proto-NT T : F → G that obeys the “square condition” for any arrow f : A → B (namely: T_{B} ∘ F (f) = G(f) ∘ T_{A}) is a natural transformation. Using ‘wd’ these conditions can be written as:

∀O_{a} wd(a^{F} → a^{F})
∀O_{a}, O_{b}, O_{c}, (a → b), (b → c) wd(a^{F} → c^{F})
∀O_{a}, O_{b}, (a → b) wd(a^{F} → b^{G})

Note that these conditions must be checked in the semantics.

A simple example of system NDC at work: here’s how to “Curry” the identity functor (a; b) ⇒ (a; b).

\begin{matrix}\begin{matrix}\begin{matrix}[a′ → a′′]^{2} & {[O[b]]^{1} \atop b → b} \\ (a′; b) → (a′′; b) \end{matrix} ; b →^{•} ((a′; b) → (a′′; b)) & 1 \\ (b ⇒ (a′; b)) → (b ⇒ (a′′; b)) \end{matrix} & ren \\ a ⇒ (b ⇒ (a; b)) \end{matrix} ; 2

From the object of ‘b’s in B build the identity arrow b → b; with the morphisms a′ → a′′ of A and b → b build the morphism (a′; b) → (a′′; b) of the product category A × B. Now regard what is above the bar marked ‘1’ as an operation that takes an arbitrary object O[b] of B and produces a morphism (a′; b) → (a′′; b); this is what a natural transformation b →^{•} ((a′; b) → (a′′; b)) would do, so we can discharge the O[b] and form a (proto-)natural transformation. Apply a renaming rule and that becomes a morphism between the objects O[b ⇒ (a′; b)] and O[b ⇒ (a′′; b)] in A ⇒ A × B, a category of functors. So we’ve got an operation that behaves syntactically as a functor a ⇒ (b ⇒ (a; b)), as it takes a generic morphism of A, a′ → a′′, and returns a morphism with the right name; discharge the a′ → a′′ and form a (proto-)functor.

Other examples: the Yoneda lemma corresponds to the term (a; b ⇒ b^{F}) →^{•} (a^{F} ↔ (b →^{•} ((a → b) → b^{F}))), but explaining it would require a few more definitons. The terms for the exponentials and the classifier in a Set^{C} would require even more definitions.

Eduardo Ochs Departamento de Matemática, PUC-Rio

http://www.mat.puc-rio.br/~edrx/math.html
edrx@mat.puc-rio.br