From 314d624bf6f7f9114d34f23d29af3e7dc02b2b34 Mon Sep 17 00:00:00 2001 From: Mike Shulman Date: Tue, 7 Jun 2016 13:00:25 -0700 Subject: [PATCH] Remove canonical/atomic; can consider adding it back later --- canonical.tex | 642 +++++++++++++++++++++++++++++++++++++++++++++++ catlog.tex | 676 ++------------------------------------------------ 2 files changed, 662 insertions(+), 656 deletions(-) create mode 100644 canonical.tex diff --git a/canonical.tex b/canonical.tex new file mode 100644 index 0000000..75cfa84 --- /dev/null +++ b/canonical.tex @@ -0,0 +1,642 @@ +\chapter{Computation and Canonicity} +\label{cha:canonical} + +[TODO: Is this chapter a good idea at all?] + +As observed in \cref{rmk:beta-reduction}, the $\beta$-reduction rule can be seen as a ``directed simplification'': clearly $M$ is simpler than $\pi_1(\pair M N)$. +Put differently, the derivation leading to the term $\pi_1(\pair M N)$ is ``redundant'' since it represents a morphism that already had a representative, namely $M$. +In this chapter we study theories that (at least partially) prevent such redundancy from occurring, eliminating (or reducing) the need for the equivalence relations $\equiv$ in presenting free categories. + +The idea is to prevent application of elimination rules (such as $\pi_1$) to terms resulting from introduction rules (such as $\pair M N$). +We do, of course, have to be able to apply elimination rules to some terms, in order to derive, say, $x:A\times B \types \pi_1(x):A$. +To distinguish between the ``terms that can be eliminated'' and those that can't, we replace the single judgment $x:A\types M:B$ with two: +\begin{mathpar} + x:A \types M\atom B\and + x:A \types M\can B. +\end{mathpar} +We read $M\atom B$ as ``$M$ is an \textbf{atomic} term of type $B$'' and $M\can B$ as ``$M$ is a \textbf{canonical} term of type $B$''. +Intuitively, the canonical terms are a subset of the ordinary ones with the property of being ``canonical representatives'' of a morphism in a free category. +If we succeed at proving an initiality theorem without needing to impose any equivalence relation on terms, then it will follow that in fact, every $\equiv$-equivalence class of ordinary terms has \emph{exactly one} representative that is ``canonical'' in the current sense. +Moreover, by translating the theories with $\equiv$ into the theories without $\equiv$ we obtain a ``reduction'' operation that computes the canonical form of any term. + + +\section{Categories with products} +\label{sec:atomcan-catprod} + +We consider first the case of categories with products only. +We assert the same natural deduction rules as before, but now with annotations describing which terms are canonical and which are atomic. +\begin{mathpar} + \inferrule{\types X\type}{x:X\types x\atom X}\;\idfunc\and + \inferrule{f\in \cG(A,B) \\ x:X\types M\can A}{x:X\types f(M)\atom B}\;fI\and + \inferrule{\types X\type}{x:X\types \ttt\can \unit}\;\unit I\and + \inferrule{x:X\types M\atom B\times C}{x:X \types \pi_1(M)\atom B}\;\timesE1\and + \inferrule{x:X\types M\atom B\times C}{x:X \types \pi_2(M)\atom C}\;\timesE2\and + \inferrule{x:X\types M\can B \\ x:X\types N\can C}{x:X\types \pair MN\can B\times C}\;\timesI +\end{mathpar} +Note particularly that in the $\timesE$ rules, $M$ must be atomic; whereas in the $\timesI$ rule, $\pair MN$ is only canonical; thus $\pi_1(\pair MN)$ cannot be formed. +We allow $M$ and $N$ in the $\timesI$ rule to also be canonical, so that we can form iterated pairs such as $\pair M{\pair NP}$; while similarly we say that $\pi_1(M)$ and $\pi_2(M)$ are again atomic, so that we can form iterated projections such as $\pi_1(\pi_2(M))$. +All variables are atomic, so that we can form $x:A\times B \types \pi_1(x):A$. + +Of course, this division into atomic and canonical is an artifact of the syntax; it has no natural counterpart in category theory. +Thus, to extract a description of a free category with products, we need some way to combine the two kinds of terms to describe one kind of morphism. +It turns out that the best way to do this is to assert that any atomic term \emph{belonging to a base type} (i.e.\ an object of \cG) is also canonical: +\begin{mathpar} + \inferrule{B\in\cG \\ x:A \types M\atom B}{x:A\types M\can B}\;\atomcan +\end{mathpar} +and then regard the canonical terms as the morphisms. +This completes the definition of our \textbf{unary canonical/atomic calculus for categories with products}. + +At this point it is a little difficult to explain why we regard a term of the form $f(M)$ to be atomic but allow the argument $M$ to be canonical. +It doesn't make much difference what choice we make regarding this rule in our current very simple theory, since both $M$ and $f(M)$ always belong to a base type, and for base types there is no difference between atomic and canonical terms (the only way to make a canonical term of a base type is to apply $\atomcan$). +So we just ask the reader to take our word for it that this choice is the best one; it will make more sense later [TODO]. + +The restriction $B\in\cG$ in $\atomcan$ is what removes the redundancy expressed by the \emph{other} generator of $\equiv$, namely the $\eta$-conversion $\pair{\pi_1(M)}{\pi_2(M)}\equiv M$. +However, it deals with it in a surprising way: it is the seemingly ``more complicated'' term $\pair{\pi_1(M)}{\pi_2(M)}$ that we regard as canonical! +For example, when $x=M$ we have the following derivation in our new system: +\begin{mathpar} + \inferrule*[Right=\timesI]{ + \inferrule*[Right=\atomcan]{ + \inferrule*[Right=\timesE]{\inferrule*{ }{x:A\times B\types x\atom A\times B}}{x:A\times B \types \pi_1(x)\atom A} + }{x:A\times B \types \pi_1(x)\can A} \\ + \inferrule*[Right=\atomcan]{ + \inferrule*[Right=\timesE]{\inferrule*{ }{x:A\times B\types x\atom A\times B}}{x:A\times B \types \pi_2(x)\atom B} + }{x:A\times B \types \pi_2(x)\can B} + }{ + x:A\times B \types \pair{\pi_1(x)}{\pi_2(x)}\can A\times B + } +\end{mathpar} +but while we have $x:A\times B\types x\atom A\times B$, we cannot apply $\atomcan$ to deduce $x:A\times B\types x\can A\times B$ since $A\times B$ is not a base type. +Put differently, when transforming an arbitrary term into a canonical one, we regard the $\beta$-conversion as a reduction, but the $\eta$-conversion as an \emph{expansion}. + +There are various reasons for this choice, foremost among which is that it works well. +Philosophically, it can be justified by saying that the type $A\times B$ is supposed to be a ``type whose elements are pairs'', and therefore the \emph{canonical form} of any element of it (even a variable) should \emph{be a pair}. +A category theorist can gain some intuition for it by thinking of $\beta$-reduction as analogous to the multiplication transformation $T^2\to T$ of a monad, while the $\eta$-expansion is analogous to the unit transformation $\mathsf{Id}\to T$. +In an example such as the free monoid monad, the multiplication ``simplifies'' a list $((a,b),(),(c,d,e))$ by removing redundant parentheses to get $(a,b,c,d,e)$, while the unit makes an element $a$ into a list $(a)$ by \emph{adding} parentheses. +Na\"ively one might say that $(a)$ is more complicated than $a$, but it has the virtue of being in the same ``canonical form'' as every other list. + +\begin{rmk} + Recall that we generally want to regard terms as simply a different syntactic representation of derivations, with a parse tree that inverts the derivation tree. + This is almost true for our current system: the only rule that breaks it is $\atomcan$, which uses the same term $M$ to represent two different derivations (one of $M\atom B$, and one of $M\can B$ obtained by following the former with $\atomcan$). + However, this can be regarded as simply a convenient abuse of notation: since otherwise the syntaxes producing atomic and canonical terms are disjoint, if when parsing $M\can B$ we see that $M$ looks like an atomic term, it must be that it was deduced from $\atomcan$ and so we can insert an appropriate node into the tree. +\end{rmk} + +The central lemma that justifies this theory is, as usual, the admissibility of cut/substitution. + +\begin{lem}\label{thm:catprod-atomcan-subadm} + The following two cut rules are admissible in the unary canonical/atomic calculus for categories with products. + \begin{enumerate} + \item If $x:A\types M\can B$ and $y:B\types N\atom C$ are derivable, then either $x:A\types P\atom C$ or $x:A\types P\can C$ is derivable for some $P$.\label{item:catprod-atomcan-subadm-1} + \item If $x:A\types M\can B$ and $y:B\types N\can C$ are derivable, then $x:A\types P\can C$ is derivable for some $P$.\label{item:catprod-atomcan-subadm-2} + \end{enumerate} +\end{lem} +For purposes of composition in a free category with products, we are mainly interested in~\ref{item:catprod-atomcan-subadm-2}. +However, for the induction to go through we must also prove~\ref{item:catprod-atomcan-subadm-1} by a simultaneous induction on derivations of both. +\begin{proof} + Here are the inductive cases for the derivation of $y:B\types N\atom C$: + \begin{itemize} + \item If it ends with $\idfunc$, then $B=C$ and $N=y$, whence $x:A\types M\can B$ is our desired result. + \item If it ends with $fI$ for some $f\in\cG(D,C)$, then $N=f(N')$ and $y:B\types N'\can D$. + Thus, by the inductive hypothesis of~\ref{item:catprod-atomcan-subadm-2}, we have $x:A\types P'\can D$. + Applying $fI$ again, we have $x:A\types f(P')\atom C$. + \item If it ends with $\timesE1$, then we have $N=\pi_1(N')$ and $y:B\types N'\atom C\times D$. + Thus, inductively we have $x:A\types P'\can C\times D$. + This is where the interesting thing happens: since $P'$ is canonical rather than atomic, we can't apply $\timesE1$ directly to obtain $\pi_1(P')$. + Instead we observe that \emph{any canonical term of $C\times D$ must be of the form $\pair PQ$}, simply because the only rule that builds canonical terms of a product type is $\timesI$. + Thus, we must have $P'=\pair PQ$ where $x:A\types P\can C$ and $x:A\types Q\can D$. + But $x:A\types P\can C$ is exactly what we wanted. + (Of course, the case of $\timesE2$ is symmetric.) + \end{itemize} + And here are the inductive cases for the derivation of $y:B\types N\can C$: + \begin{itemize} + \item If it ends with $\unit I$, then $C=\unit$ and so $x:A\types \ttt\can \unit$. + \item If it ends with $\timesI$, then $N=\pair{N_1}{N_2}$ with $y:B\types N_1\can C_1$ and $y:B\types N_2\can C_2$. + Thus, inductively we have $x:A\types P_1:C_1$ and $x:A\types P_2:C_2$, whence $x:A\types \pair{P_1}{P_2}\can C$. + \item If it ends with $\atomcan$, then we have $y:B\types N\atom C$, and hence by the inductive hypothesis of~\ref{item:catprod-atomcan-subadm-1} we have either $x:A\types P\atom C$ or $x:A\types P\can C$. + In the second case we are done. + In the first case, since we already applied $\atomcan$ at type $C$, $C$ must be a base type, so we can apply $\atomcan$ again to conclude $x:A\types P\can C$.\qedhere + \end{itemize} +\end{proof} + +Like \cref{thm:category-cutadm,thm:catprod-subadm}, the proof of \cref{thm:catprod-atomcan-subadm} defines a ``substitution'' operation (well, technically, two operations) on terms, which we write as $N\hsub{M/y}$. +However, compared to ordinary substitution, this operation is more powerful: it also performs ``$\beta$-simplification'' as it goes. +For instance, we have +\[ \pi_1(y)\hsub{\pair M N/y} = M \] +whereas ordinary substitution would give $\pi_1(\pair M N)$. +In type-theoretic lingo, this ``reducing substitution'' is called \textbf{hereditary substitution}. +Its recursive defining clauses are +\begin{align*} + y\hsub{M/y} &= M\\ + f(N)\hsub{M/y} &= f(N\hsub{M/y})\\ + \ttt\hsub{M/y} &= \ttt\\ + \pi_1(N)\hsub{M/y} &= P \qquad\text{where }N\hsub{M/y}=\pair P Q\\ + \pi_2(N)\hsub{M/y} &= Q \qquad\text{where }N\hsub{M/y}=\pair P Q\\ + \pair P Q \hsub{M/y} &= \pair{P\hsub{M/y}}{Q\hsub{M/y}}. +\end{align*} + +In particular, hereditary substitution implies that the usual natural deduction rules are also \emph{admissible} for canonical terms. +For instance, given a canonical term $x:X \types M\can A\times B$, we can construct a canonical term $x:X\types M' \can A$, even though $\pi_1$ cannot be applied directly to canonical terms; we can take $M' = \pi_1(y)\hsub{M/y}$. +(It may be tempting to write this as ``$\pi_1(M)$'', but that would probably be confusing since it hides the fact that a meta-operation on syntax is occurring, as we can't directly apply $\pi_1$ to $M$.) + +This gives our promised way to ``reduce'' terms in the type theory from \cref{sec:beta-eta}. +Like we did in \cref{sec:category-cutadm} for the cut-ful type theory of \cref{sec:category-cutful}, since all the rules of \cref{sec:beta-eta} are admissible in our canonical/atomic calculus, we can interpret any derivation --- and hence any term --- in that type theory into our current one. +With projections defined in terms of hereditary substitution as in the previous paragraph, the net effect of this is to automatically reduce all applications of a projection to a pair. + +Now recall that in ordinary natural deduction, we don't need to (and, indeed, can't) prove that identity rule $A\types A$ is also admissible; hence we assume the ``use a variable'' rule $x:A\types x:A$. +However, in the canonical/atomic calculus, we have only assumed that variables are \emph{atomic}; thus we need to also prove that there are \emph{canonical} identities. + +\begin{lem}\label{thm:catprod-atomcan-idadm} + If $\types A\type$ is derivable, then there is a term $\hid{A}(x)$ such that $x:A \types \hid{A}(x)\can A$. +\end{lem} +\begin{proof} + We induct on the derivation of $\types A\type$. + \begin{itemize} + \item If $A\in\cG$ is a base type, then we can apply $\atomcan$ to derive $x:A \types x\can A$. + \item If $A=\unit$, then $x:\unit \types \ttt\can \unit$. + \item If $A=A_1\times A_2$, then by induction we have $y:A_1 \types \hid{A_1}(y)\can A_1$ and $z:A_2 \types \hid{A_2}(z)\can A_2$. + Thus, $x:A \types \hid{A_1}(y)\hsub{\pi_1(x)/y}\can A_1$ and $x:A \types \hid{A_2}(z)\hsub{\pi_2(x)/z}\can A_2$, so we have + \[ x:A \types \pair{\hid{A_1}(y)\hsub{\pi_1(x)/y}}{\hid{A_2}(z)\hsub{\pi_2(x)/z}} \can A.\qedhere\] + \end{itemize} +\end{proof} + +As a recursively defined operation, the clauses of $\hid{A}$ are thus +\begin{align*} + \hid{A}(x) &= x \qquad\text{if }{A\in\cG}\\ + \hid{\unit}(x) &= \ttt\\ + \hid{A\times B}(x) &= \pair{\hid{A}(y)\hsub{\pi_1(x)/y}}{\hid{B}(z)\hsub{\pi_2(x)/z}}. +\end{align*} +Note that the hereditary substitution in the last clause is not doing any $\beta$-reduction, since the identity terms being substituted into are built only out of variables and pairs. +For instance, we have +\[ \hid{A\times (B\times C)}(x) = \pair{\pi_1(x)}{\pair{\pi_1(\pi_2(x))}{\pi_2(\pi_2(x))}} \] + +\begin{lem}\label{thm:atomcan-catprod-subassoc} + Hereditary substitution and identities form a category: + \begin{align*} + P\hsub{N/z}\hsub{M/y} &= P\hsub{N\hsub{M/y}/z}\\ + \hid{A}(y)\hsub{M/y} &= M\\ + N\hsub{\hid{A}(x)/y} &= N[x/y]. + \end{align*} +\end{lem} +\begin{proof} + Left to the reader as \cref{ex:atomcan-catprod-subassoc}. +\end{proof} + +\begin{thm}\label{thm:atomcan-catprod-initial} + For any directed graph \cG, the free category with finite products generated by \cG can be described by the unary canonical/atomic calculus for categories with products under \cG, without any quotienting: its objects are the types $A$ such that $\types A\type$ is derivable, and its morphisms $A\to B$ are the terms $M$ such that $x:A \types M\can B$ is derivable. +\end{thm} +\begin{proof} + \cref{thm:atomcan-catprod-subassoc} gives us a category, which we denote $\F\bPrCat\cG$. + The interesting thing is the proof that $\F\bPrCat\cG$ has finite products. + The product of $A$ and $B$ is, of course, supposesd to be $A\times B$, with projections + \begin{align*} + z:A\times B &\types \pi_1(w)\hsub{z/w}\can A\\ + z:A\times B &\types \pi_2(w)\hsub{z/w}\can B + \end{align*} + (We can't write $\pi_1(z)$ because $A$ may not be a base type.) + Now given any morphisms $x:X \types M\can A$ and $x:X \types N\can B$, we can certainly form $x:X \types \pair M N \can A\times B$, and its composite with $\pi_1$ is + \[ \pi_1(w)\hsub{z/w}\hsub{\pair M N/z} = \pi_1(w)\hsub{z\hsub{\pair M N/z}/w} = \pi_1(w)\hsub{\pair M N/w} = M \] + using the associativity of hereditary substitution and the definition of hereditary substitution on $\pi_1$. + Of course, the case of $\pi_2$ is similar. + In the other direction, given any morphism $x:X \types P\can A\times B$, as observed in the proof of \cref{thm:catprod-atomcan-subadm} $P$ must be a pair $\pair M N$ where $x:X\types M\can A$ and $x:X\types N\can B$, and for the same reasons $M$ and $N$ are the composites of $P$ with $\pi_1$ and $\pi_2$ respectively. + Thus, $A\times B$ has the universal property of a product with respect to \emph{syntactic equality} of terms/derivations. + + Now if \cM is a category with finite products and $P:\cG\to\cM$ a graph morphism, we extend $P$ to $\F\bPrCat\cG$ just as before by recursion on derivations. + We have to define $P$ on both atomic and canonical terms for the recursion to go through (since the atomic and canonical terms are defined by mutual induction); since there is no separation between ``atomic and canonical morphisms'' in \cM we just send both kinds of term to ordinary morphisms in \cM. + As usual, the defining clauses in this recursion are forced by functoriality and product-preservation, and we can then prove by induction on derivations that the resulting operation actually is a functor. +\end{proof} + + +\subsection*{Exercises} + +\begin{ex}\label{ex:atomcan-catprod-subassoc} + Prove \cref{thm:atomcan-catprod-subassoc} (hereditary substitution is associative). +\end{ex} + +\begin{ex}\label{ex:atomcan-catfib} + Formulate a canonical/atomic calculus for fibrations of categories and prove its initiality theorem. + Then do the same for fibrations of categories with products, as in \cref{ex:catprod-fib}. +\end{ex} + + +\section{Categories with coproducts} +\label{sec:atomcan-catcoprod} + +Now we consider a canonical/atomic calculus for categories with coproducts. +In general, objects with left (``mapping out'') universal properties are trickier to deal with in natural deduction systems, because our terms only appear on the \emph{right} of the $\types$. +We begin by rewriting the theory of \cref{sec:catcoprod} with atomic and canonical annotations; see \cref{fig:catcoprod-atomcan}. +\begin{figure} + \centering + \begin{mathpar} + \inferrule{\types X\type}{x:X\types x\atom X}\;\idfunc\and + \inferrule{f\in \cG(A,B) \\ x:X\types M\can A}{x:X\types f(M)\atom B}\;fI\and + \inferrule{x:X \types M\atom \zero \\ \types C\type}{x:X \types \abort(M)\can C}\;\zeroE\\ + \inferrule{x:X\types M\can A}{x:X\types \inl(M)\can A + B}\;\plusI1\and + \inferrule{x:X\types N\can B}{X\types \inr(N)\can A + B}\;\plusI2\and + \inferrule{u:A\types P\can C \\ v:B\types Q\can C \\ x:X\types M\atom A + B}{x:X\types \case(M,u.P,v.Q)\can C}\;\plusE\and + \inferrule{B\in\cG\\ x:A \types M\atom B}{x:A\types M\can B}\;\atomcan + \end{mathpar} + \caption{Unary canonical/atomic calculus for categories with coproducts} + \label{fig:catcoprod-atomcan} +\end{figure} +The principle is the same: we prevent ourselves from eliminating on the results of introduction rules by requiring elimination rules to act only on atomic terms. +The only perhaps surprising thing is that the ``branches'' $P,Q$ of $\case$, and the $\case$ term itself, are canonical, though the ``branch term'' $M$ must be atomic. + +The proof of admissibility of (hereditary) substitution for this theory is more complicated because of the presence of the rules $\zeroE$ and $\plusE$. +In \cref{sec:atomcan-catprod} we could see by inspection that canonical terms of a certain type must have a certain form, but $\zeroE$ and $\plusE$ can produce canonical terms of any type at all. + +\begin{thm}\label{thm:atomcan-catcoprod-subadm} + The following rules are admissible in the unary canonical/atomic calculus for categories with coproducts under \cG: + \begin{enumerate} + \item Hereditary substitution into atomic terms: if $x:A\types M\can B$ and $y:B\types N\atom C$ are derivable, then either $x:A\types P\atom C$ or $x:A\types P\can C$ is derivable for some $P$.\label{item:catcoprod-atomcan-subadm-1} + \item Hereditary substitution into canonical terms: if $x:A\types M\can B$ and $y:B\types N\can C$ are derivable, then $x:A\types P\can C$ is derivable for some $P$.\label{item:catcoprod-atomcan-subadm-2} + \end{enumerate} +\end{thm} +\begin{proof} + By mutual induction. + We outline the cases for each statement as follows. + \begin{enumerate} + \item A derivation of $y:B\types N\atom C$ can only end with $\idfunc$ and $fI$. + Both cases are just like those in \cref{thm:catprod-atomcan-subadm}; + recall that the second case uses the inductive hypothesis of~\ref{item:catcoprod-atomcan-subadm-2}. + \item A derivation of $y:B\types N\can C$ can end with $\atomcan$, $\plusI1$, $\plusI2$, $\zeroE$, or $\plusE$. + \begin{itemize} + \item If it ends with $\atomcan$, we apply the inductive hypothesis of~\ref{item:catcoprod-atomcan-subadm-1}. + \item If $N=\inl(N')$ with $y:B\types N'\can C_1$, then by the inductive hypothesis $x:A\types N'\hsub{M/y}\can C_1$ and so $x:A\types \inl(N'\hsub{M/y})\can C$. + The case of $\inr$ is dual. + \item If $N=\case(N',u.P,v.Q)$ with $y:B\types N'\atom D+E$ and $u:D\types P\can C$ and $v:E\types Q\can C$, then since the only rule that can produce an atomic term of type $D+E$ is $\idfunc$, we must have $B=D+E$ and $N'=y$. + % In a more general case, we would inspect the last rule in the derivation; the other ways to produce an atomic term could then be substituted by the inductive hypothesis of~\ref{item:catcoprod-atomcan-subadm-1} to give an atomic $N'\hsub{M/y}\atom D+E$ that we can apply $\case$ to directly. + Now we do a secondary inner induction on the derivation of $x:A\types M\can B$, which can likewise end with $\plusI1$, $\plusI2$, or $\zeroE$ or $\plusE$. + \begin{itemize} + \item If $M=\inl(M')$, then by the inductive hypothesis we have $x:A\types P\hsub{M'/u}\can C$. + \item Dually, if $M=\inr(M')$, we have $x:A\types Q\hsub{M'/v}\can C$. + \item If $M=\abort(M')$, then $x:A\types \abort(M')\can C$. + \item If $M=\case(M',w.S,z.T)$ with $x:A\types M'\atom F+G$ and $w:F\types S\can D+E$ and $z:G\types T\can D+E$, then + by the inner inductive hypothesis we have $w:F\types S'\can C$ and $z:G\types T'\can C$. + Thus, applying $\plusE$ we have $x:A\types \case(M',w.S',z.T')\can C$. + \end{itemize} + \item The case when $N=\abort(N')$ with $y:B\types N'\atom\zero$ is similar, but simpler. + We must have $B=\zero$ and $N'=y$, and we induct on the derivation of $x:A\types M\can B$, which must end with $\zeroE$ or $\plusE$. + \begin{itemize} + \item If $M=\abort(M')$, then $x:A\types \abort(M')\can C$. + \item If $M=\case(M',w.S,z.T)$ with $x:A\types M'\atom F+G$ and $w:F\types S\can \zero$ and $z:G\types T\can \zero$, then + by the inner inductive hypothesis we have $w:F\types S'\can C$ and $z:G\types T'\can C$, whence $x:A \types \case(M',w.S',z.T')\can C$.\qedhere + \end{itemize} + \end{itemize} + \end{enumerate} +\end{proof} + +\begin{figure} + \centering + \begin{align*} + y\hsub{M/y} &= M\\ + f(N)\hsub{M/y} &= f(N\hsub{M/y})\\ + \inl(N)\hsub{M/y} &= \inl(N\hsub{M/y})\\ + \inr(N)\hsub{M/y} &= \inr(N\hsub{M/y})\\ + \abort(y)\hsub{M/y} &= \abort'(M)\\ + \case(y,u.P,v.Q)\hsub{M/y} &= \case'(M,u.P,v.Q)\\ + \\ + \abort'(\abort(M)) &= \abort(M)\\ + \abort'(\case(M,u.P,v.Q)) &= \case(M,u.\abort'(P),v.\abort'(Q))\\ + \\ + \case'(\inl(M),u.P,v.Q) &= P\hsub{M/u}\\ + \case'(\inr(M),u.P,v.Q) &= Q\hsub{M/v}\\ + \case'(\abort(M),u.P,v.Q) &= \abort(M)\\ + \case'(\case(M,w.S,z.T),u.P,v.Q) &= \case(M,w.\case'(S,u.P,v.Q),z.\case'(T,u.P,v.Q)) + \end{align*} + \caption{Hereditary substitution for categories with coproducts} + \label{fig:catcoprod-hsub} +\end{figure} + +The resulting definition of hereditary substitution is shown in \cref{fig:catcoprod-atomcan}. +We have introduced notation $\abort'$ and $\case'$ for the operations defined by the inner recursions in the proof. +Note that these essentially constitute proofs that the unrestricted $\zeroE$ and $\plusE$ rules are admissible, just as the hereditary substitution from \cref{sec:atomcan-catprod} yielded an admissible unrestricted $\timesE$. + +The identity rule is much easier: + +\begin{thm}\label{thm:atomcan-catcoprod-idadm} + The canonincal identity rule is admissible: if $\types A\type$, then $x:A \types \hid{A}(x)\can A$. +\end{thm} +\begin{proof} + The defining clauses are + \begin{align*} + \hid{A}(x) &= x \quad\text{if }A\in \cG\\ + \hid{\zero}(x) &= \abort(x)\\ + \hid{A+B}(x) &= \case(x,u.\hid{A}(u),v.\hid{B}(v))\qedhere + \end{align*} +\end{proof} + +Like the admissible $\pi_1$ from \cref{sec:atomcan-catprod}, $\match'$ satisfies $\beta$-conversion as a syntactic equality (this is its first two defining clauses). +Unfortunately, this theory still does not validate the full $\eta$ rule for coproducts as a syntactic equality. +We do have the following weaker property: + +\begin{lem}\label{thm:atomcan-catcoprod-weaketa} + If $x:X \types M\can A+B$, then $M = \case'(M,u.\inl(u),v.\inr(v))$. + Similarly, if $x:X\types M\can\zero$, then $M=\abort'(M)$. +\end{lem} +\begin{proof} + An easy induction over the defining clauses of $\case'$ and $\abort'$. +\end{proof} + +In other words, it is still true (see footnote~\ref{fn:weak-eta}) that every term \emph{of type $A+B$} has a canonical form. +However, unlike the case of products this is insufficient to ensure the full uniqueness aspect of the universal property, since the ``mapping out'' universal property of $A+B$ constructs terms not of type $A+B$ itself but of some other type. +For instance, if we have +\begin{mathpar} + f\in\cG(A,C)\and + g\in\cG(B,C)\and + h\in\cG(C,D)\and +\end{mathpar} +then the induced morphism $A+B\to D$ is represented by both of the terms +\begin{align*} + x:A+B &\types \case(x,u.h(f(u)),v.h(g(v)))\can D\\ + x:A+B &\types h(\case(x,u.f(u),v.g(v)))\can D +\end{align*} +and these two terms are (syntactically) different, despite both yielding $h(f(u))$ and $h(g(v))$ under the hereditary substitutions $\hsub{\inl(u)/x}$ and $\hsub{\inr(v)/x}$. + +Thus, the terms/derivations in this type theory don't present a category with finite coproducts unless we impose some equivalence relation on them. +The above example also points the way to the correct equivalence relation. +We no longer need to assert $\beta$-conversion, nor do we need the weak form of $\eta$-conversion expressed by \cref{thm:atomcan-catcoprod-weaketa}; but we do need the relations shown in \cref{fig:catcoprod-commconv}. +\begin{figure} + \centering + \begin{align*} + f(\case(M,u.P,v.Q)) &\equiv \case(M,u.f(P),v.f(Q))\\ + \inl(\case(M,u.P,v.Q)) &\equiv \case(M,u.\inl(P),v.\inl(Q))\\ + \inr(\case(M,u.P,v.Q)) &\equiv \case(M,u.\inr(P),v.\inr(Q))\\ + \case(\case(M,u.P,v.Q),w.R,z.S) &\equiv \case(M,u.\case(P,w.R,z.S),v.\case(Q,w.R,z.S))\\ + \abort(\case(M,u.P,v.Q)) &\equiv \case(M,u.\abort(P),v.\abort(Q)) + \end{align*} + \caption{Commuting conversions for coproducts} + \label{fig:catcoprod-commconv} +\end{figure} +These are called \textbf{commuting conversions}. +They are a consequence of the strong form of $\eta$-conversion~\eqref{eq:catcoprod-eta}: +\begin{equation} + \inferrule{x:X \types M\atom A+B \\ y:A+B \types P\can C}{x:X \types \case(M,u.P[\inl(u)/y],v.P[\inr(v)/y]) \equiv P[M/y] \can C}\label{eq:catcoprod-eta-again} +\end{equation} +(take $P$ to be the left-hand side of each commuting conversion with $y$ in place of $M$). +Conversely, when combined with the weak $\eta$-conversion, the commuting conversions imply the strong $\eta$-conversion: + +\begin{thm}\label{thm:atomcan-catcoprod-eta} + If we augment the canonical/atomic calculus for categories with coproducts by an $\equiv$ on canonical terms generated by the relations in \cref{fig:catcoprod-commconv} (plus the usual congruence properties), then the strong $\eta$-rule~\eqref{eq:catcoprod-eta-again} is admissible. +\end{thm} +\begin{proof} + Induction on the derivation of $P$; each commuting conversion handles exactly one of the cases. +\end{proof} + +\begin{thm}\label{thm:atomcan-catcoprod-initial} + The free category with coproducts generated by a directed graph \cG can be presented by the canonical/atomic calculus for categories with coproducts modulo $\equiv$. +\end{thm} +\begin{proof} + Left to the reader as \cref{ex:atomcan-catcoprod-initial}. +\end{proof} + +[TODO: Molecular?] + + +\subsection*{Exercises} + +\begin{ex}\label{ex:atomcan-catcoprod-initial} + Prove \cref{thm:atomcan-catcoprod-initial} (initiality for the canonical/atomic calculus for categories with coproducts). +\end{ex} + +\begin{ex}\label{ex:atomcan-opfib} + Formulate a canonical/atomic calculus for opfibrations of categories, with an $\equiv$ for commuting conversions only, and prove its initiality theorem. + Then do the same for opfibrations of categories with coproducts. +\end{ex} + +\begin{ex}\label{ex:atomcan-prodcoprod} + Combine \cref{sec:atomcan-catprod,sec:atomcan-catcoprod} to give a canonical/atomic calculus for categories with both products and coproducts, and prove its initiality theorem. + (You will need some commuting conversions relating to $\timesI$ as well.) +\end{ex} + + +\section{Focusing} +\label{sec:focusing} + +For completeness, we now describe how the sequent calculus for meet-semilattices can also be modified to present free categories with products without needing an equivalence relation on terms. +This version is not as commonly used in categorical logic, but it is important in other applications of type theory, such as automated proof search; it is called \emph{focusing}. + +If we inspect the derivations of canonical terms in the type theory of \cref{sec:atomcan-catprod}, we see that they have the following form: first they apply some number of projections to variables, then they apply $\atomcan$, they apply some number of generating arrows between base types, and finally they apply some number of pairings. +For instance, if $f\in \cG(C,D)$ we have +\[x:(A\times B)\times C \types \pair{f(\pi_2(x))}{\pi_2(\pi_1(x))}\can D\times B\] +with derivation +\begin{mathpar} +\let\mytimes\times +\def\times{\mathord{\mytimes}} + \inferrule*{ + \inferrule*{\inferrule*{\inferrule*{ + x:(A\times B)\times C \types x\atom (A\times B)\times C + }{x:(A\times B)\times C \types \pi_2(x) \atom C + }}{x:(A\times B)\times C \types \pi_2(x) \can C + }}{x:(A\times B)\times C \types f(\pi_2(x)) \can D} + \\ + \inferrule*{\inferrule*{\inferrule*{ + x:(A\times B)\times C \types x\atom (A\times B)\times C + }{x:(A\times B)\times C \types \pi_1(x)\atom A\times B + }}{x:(A\times B)\times C \types \pi_2(\pi_1(x))\atom B} + }{x:(A\times B)\times C \types \pi_2(\pi_1(x))\can B} + }{x:(A\times B)\times C \types \pair{f(\pi_2(x))}{\pi_2(\pi_1(x))}\can D\times B} +\end{mathpar} +This suggests that we ought to consider as ``canonical'' the sequent calculus derivation that is closest to the above. +Roughly speaking, this means first applying left rules, then generators, then right rules\footnote{To be honest, we should point out that the fact that the canonical derivations can be described so simply is an artifact of the relative triviality of our current theory, with essentially only one operation $\times$. +One can still formulate canonical/atomic and focused versions of more general theories, but the canonical forms don't have as simple a description.}, as in the following derivation: +\begin{mathpar} + \inferrule*{ + \inferrule*{\inferrule*{C\types C + }{(A\times B)\times C \types C + }}{(A\times B)\times C \types D} + \\ + \inferrule*{\inferrule*{B \types B + }{A\times B \types B + }}{(A\times B)\times C \types B} + }{(A\times B)\times C \types D\times B} +\end{mathpar} +As in the natural deduction case, we can rule out the undesired sequent calculus derivations by using two judgments to indicate whether we are in the ``left phase'' or the ``right phase''. +We denote these by +\[ \focus{A} \types B +\qquad\text{and}\qquad +%A\types\focus{B} +A\types B +\] +respectively. +The brackets in the first case indicate that we are ``focused'' on the left side of the sequent. +You might think that in the second case we should write $A\types \focus B$ to indicate that we are focused on the right side, but in fact in the latter case we are not really ``focused'' at all; in more complicated situations there is also a ``right-focused'' judgment $A\types \focus B$ that is different from both $\focus A \types B$ and $A\types B$. +The asymmetry we see here is due to the fact that all universal properties we are considering are of the ``mapping in'' sort. + +We now modify the sequent calculus rules from \cref{sec:seqcalc-mslat} by stipulating that +the right rules only apply when we are in the right phase, +% \begin{mathpar} +% \inferrule{A\types \focus{B} \\ A\types \focus{C}}{A\types \focus{B\times C}}\and +% \inferrule{f\in \cG(A,B) \\ X\types \focus{A}}{X\types \focus{B}}\and +% \inferrule{\types A\type}{A\types \focus{\top}}\and +% \end{mathpar} +while the left rules apply only in the left phase; +% \begin{mathpar} +% \inferrule{A\in \cG}{\focus A\types A}\and +% \inferrule{\focus A\types C \\ \types B\type}{\focus {A\times B} \types C}\and +% \inferrule{\focus B\types C \\ \types A\type}{\focus{A\times B} \types C}\and +% \end{mathpar} +and we can transition from the left to the right phase, but not vice versa. +% \[ \inferrule{\focus A \types B}{A\types\focus B}\] +Since we are interested in distinguishing between derivations, we also annotate our sequents with terms; and +because the left rules of sequent calculus are not well-adapted to the use of formal variables, we go back to annotating the entire sequent with a term. +The rules with annotations for this \textbf{unary focused sequent calculus for categories with products} are shown in \cref{fig:catprod-focused-seqcalc}. + +\begin{figure} + \centering + \begin{mathpar} + % \inferrule{\phi:(A\types \focus{B}) \\ \psi:(A\types \focus{C})}{\pair{\phi}{\psi}:(A\types \focus{B\times C})}\and + % \inferrule{f\in \cG(A,B) \\ \phi:(X\types \focus{A})}{\postc f\phi:(X\types \focus{B})}\and + % \inferrule{\types A\type}{\ttt:(A\types \focus{\top})}\and + \inferrule{\phi:(A\types {B}) \\ \psi:(A\types {C})}{\pair{\phi}{\psi}:(A\types {B\times C})}\and + \inferrule{f\in \cG(A,B) \\ \phi:(X\types {A})}{\postc f\phi:(X\types {B})}\and + \inferrule{\types A\type}{\ttt:(A\types {\top})}\and + \inferrule{A\in \cG}{\idfunc_A:(\focus A\types A)}\and + \inferrule{\phi:(\focus A\types C) \\ \types B\type}{\prec{\phi}{\pi_1}:(\focus {A\times B} \types C)}\and + \inferrule{\phi:(\focus B\types C) \\ \types A\type}{\prec{\phi}{\pi_2}:(\focus{A\times B} \types C)}\and + \inferrule{\phi:(\focus A \types B)}{\phi:(A\types B)} + \end{mathpar} + \caption{Unary focused sequent calculus for categories with products} + \label{fig:catprod-focused-seqcalc} +\end{figure} + +For instance, the above derivation of $(A\times B)\times C \types D\times B$ can be given in the focused sequent calculus with term annotations as follows: +\begin{mathpar} + \let\mytimes\times + \def\times{\mathord{\mytimes}} + \inferrule*{ + \inferrule*{\inferrule*{\inferrule*{\idfunc_C:(\focus C\types C) + }{\prec{\idfunc_C}{\pi_2}:(\focus{(A\times B)\times C} \types C) + }}{\prec{\idfunc_C}{\pi_2}:((A\times B)\times C \types C) + }}{\postc{f}{\prec{\idfunc_C}{\pi_2}}:((A\times B)\times C \types D)} + \\ + \inferrule*{\inferrule*{\inferrule*{\idfunc_B:(\focus B \types B) + }{\prec{\idfunc_B}{\pi_2}:(\focus{A\times B} \types B) + }}{\prec{\prec{\idfunc_B}{\pi_2}}{\pi_1}:(\focus{(A\times B)\times C} \types B) + }}{\prec{\prec{\idfunc_B}{\pi_2}}{\pi_1}:((A\times B)\times C \types B)} + }{\pair{\postc{f}{\prec{\idfunc_C}{\pi_2}}}{\prec{\prec{\idfunc_B}{\pi_2}}{\pi_1}} + :((A\times B)\times C \types {D\times B})} + % \inferrule*{ + % \inferrule*{\inferrule*{\inferrule*{\idfunc_C:(\focus C\types C) + % }{\prec{\idfunc_C}{\pi_2}:(\focus{(A\times B)\times C} \types C) + % }}{\prec{\idfunc_C}{\pi_2}:((A\times B)\times C \types \focus C) + % }}{\postc{f}{\prec{\idfunc_C}{\pi_2}}:((A\times B)\times C \types \focus D)} + % \\ + % \inferrule*{\inferrule*{\inferrule*{\idfunc_B:(\focus B \types B) + % }{\prec{\idfunc_B}{\pi_2}:(\focus{A\times B} \types B) + % }}{\prec{\prec{\idfunc_B}{\pi_2}}{\pi_1}:(\focus{(A\times B)\times C} \types B) + % }}{\prec{\prec{\idfunc_B}{\pi_2}}{\pi_1}:((A\times B)\times C \types \focus B)} + % }{\pair{\postc{f}{\prec{\idfunc_C}{\pi_2}}}{\prec{\prec{\idfunc_B}{\pi_2}}{\pi_1}} + % :((A\times B)\times C \types \focus{D\times B})} +\end{mathpar} + +As usual, we need to prove the admissibility of identity and cut. +The proof of cut is very similar to that of \cref{thm:catprod-atomcan-subadm}. + +\begin{lem}\label{thm:focused-catprod-cutadm} + The following two cut rules are admissible in the unary focused sequent calculus for categories with products. + \begin{enumerate} + \item If $A\types B$ and $\focus B\types C$, then $A\types C$.\label{item:focused-catprod-cutadm-1} + \item If $A\types B$ and $B\types C$, then $A\types C$.\label{item:focused-catprod-cutadm-2} + \end{enumerate} +\end{lem} +\begin{proof} + First we prove~\ref{item:focused-catprod-cutadm-1} by induction on the derivation of $\focus B\types C$. + \begin{itemize} + \item If it is $\idfunc_B$, then $A\types B$ is $A\types C$. + \item If it ends with $\pi_1$, then $B$ is $B_1\times B_2$ and we have $\focus B_1\types C$. + Now consider the derivation of $A\types B$, i.e.\ $A\types B_1\times B_2$. + \textit{A priori} this could end either with the ``unfocus'' rule or with the $\times R$ rule. + But in fact, the unfocus rule is impossible, because it is impossible to derive $\focus A\types B$ unless $B$ is a base type (this is an easy induction). + Thus, we must have $A\types B_1$ and $A\types B_2$, so we can apply the inductive hypothesis on $B_1$ to get $A\types C$. + \end{itemize} + Now we prove~\ref{item:focused-catprod-cutadm-2}, by induction on the derivation of $B\types C$. + \begin{itemize} + \item If it ends with the right rule for $\times$ or $\unit$, or the generator rule for $f$, we can simply apply the inductive hypothesis and then the same rule, as usual. + \item If it ends with the unfocus rule, then we apply part~\ref{item:focused-catprod-cutadm-1}.\qedhere + \end{itemize} +\end{proof} + +However, if we try to prove admissibility of identity directly, we run into problems. +We need the following lemma first. + +\begin{lem}\label{thm:focused-catprod-leftadm} + The unfocused left rules for $\times$ are admissible in the unary focused sequent calculus for categories with products. + That is, if we have a derivation of $A\types C$ and $\types B\type$, we can construct a derivation of $A\times B\types C$, and dually. +\end{lem} +\begin{proof} + We induct on the derivation of $A\types C$. + \begin{itemize} + \item If it ends with the ``unfocus'' rule, whose premise is $\focus A\types C$, then we can apply the focused left rule to this to conclude $\focus{A\times B}\types C$, and then unfocus it to obtain $A\times B\types C$. + \item If it ends with the right rule for $\times$, then $C=C_1\times C_2$ and we have derivations of $A\types C_1$ and $A\types C_2$. + By the inductive hypothesis we get $A\times B\types C_1$ and $A\times B\types C_2$, whence $A\times B\types C$ by the right rule for $\times$. + \item If it ends with the generator rule for $f\in \cG(D,C)$, then we have a derivation of $A\types D$. + By the inductive hypothesis we get $A\times B\types D$, whence $A\times B\types C$. + \item Finally, if it ends with the right rule for $\unit$, then $C=\unit$, and so the same rule yields $A\times B\types C$.\qedhere + \end{itemize} +\end{proof} + +\begin{lem}\label{thm:focused-catprod-idadm} + The unfocused identity rule is admissible in the unary focused sequent calculus for categories with products. + That is, if $\types A\type$, then $A\types A$. +\end{lem} +\begin{proof} + Given \cref{thm:focused-catprod-leftadm}, we can use the same proof as \cref{thm:seqcalc-mslat-idadm}. +\end{proof} + +Of course, although the inductive argument for \cref{thm:focused-catprod-idadm} written in English is the same as that for \cref{thm:seqcalc-mslat-idadm}, the end result is different because we have the inductive construction of \cref{thm:focused-catprod-leftadm} frobnicating the results at each inductive step rather than simply applying the primitive left rule. +For instance, on $(A\times B)\times C$ the unmodified proof of \cref{thm:seqcalc-mslat-idadm} would give the derivation +\begin{mathpar} + \inferrule*{ + \inferrule*{\inferrule*{\inferrule*{A\types A}{A\times B\types A}\\ + \inferrule*{B\types B}{A\times B\types B} + }{A\times B\types A\times B} + }{(A\times B)\times C \types A\times B}\\ + \inferrule*{C\types C + }{(A\times B)\times C \types C} + }{(A\times B)\times C \types (A\times B)\times C} +\end{mathpar} +which cannot be ``focalized'' since it applies a left rule after a right rule. +Instead, from \cref{thm:focused-catprod-idadm} we obtain +\begin{mathpar} + \inferrule*{ + \inferrule*{ + \inferrule*{\inferrule*{\inferrule*{\focus A\types A}{\focus{A\times B}\types A} + }{\focus{(A\times B)\times C} \types A} + }{(A\times B)\times C \types A}\\ + \inferrule*{\inferrule*{\inferrule*{\focus B\types B}{\focus{A\times B}\types B} + }{\focus{(A\times B)\times C} \types B} + }{(A\times B)\times C \types B} + }{(A\times B)\times C \types A\times B}\\ + \inferrule*{\inferrule*{\focus C\types C + }{\focus {(A\times B)\times C} \types C} + }{(A\times B)\times C \types C} + }{(A\times B)\times C \types (A\times B)\times C} +\end{mathpar} +The resulting term is +\[ \pair{\pair{\prec{\prec{\idfunc_A}{\pi_1}}{\pi_1}}{\prec{\prec{\idfunc_B}{\pi_2}}{\pi_1}}}{\prec{\idfunc_C}{\pi_2}} : +({(A\times B)\times C \types (A\times B)\times C})\] + +We let the reader complete the argument (\cref{ex:focused-catprod-cutassoc,ex:focused-catprod-initial}). + +\begin{lem}\label{thm:focused-catprod-cutassoc} + Cut is associative and unital in the unary focused sequent calculus for categories with products.\qed +\end{lem} + +\begin{thm}\label{thm:focused-catprod-initial} + For any directed graph \cG, the free category with finite products generated by \cG can be described by the unary focused sequent calculus for categories with products under \cG, without any quotienting: its objects are the types $A$ such that $\types A\type$ is derivable, and its morphisms $A\to B$ are the terms $M$ such that $M:(A \types B)$ is derivable.\qed +\end{thm} + + +[TODO: Does focusing continue to identify unique canonical derivations in more complicated theories (with both positives and negatives)? Right now I think the answer is no, that we still need commuting conversions. How does focusing compare to canonical/atomic in theories with both positives and negatives? In theories with just positives, focusing should work just as well as in theories with just negatives, although canonical/atomic fails to give $\eta$.] + + +\subsection*{Exercises} + +\begin{ex}\label{ex:focused-catprod-cutassoc} + Prove \cref{thm:focused-catprod-cutassoc} (cut is associative and unital in the unary focused sequent calculus for categories with products). +\end{ex} + +\begin{ex}\label{ex:focused-catprod-initial} + Prove \cref{thm:focused-catprod-initial} (initiality for the unary focused sequent calculus for categories with products). +\end{ex} + + diff --git a/catlog.tex b/catlog.tex index 76743de..e8711fd 100644 --- a/catlog.tex +++ b/catlog.tex @@ -1265,7 +1265,8 @@ \subsection{Natural deduction for meet-semilattices} \begin{rmk} Because the proof of cut-elimination for natural deduction theories is so much simpler than that for sequent calculus, some people say that the former is ``trivial''. Triviality is subjective; but what seems inarguable is that cut-elimination for natural deduction is \emph{saying something different} than cut-elimination for sequent calculus. - The content of cut-elimination for sequent calculus corresponds more closely to $\beta$-reduction in natural deduction (see \cref{sec:beta-eta}), or to the cut-elimination (``hereditary substitution'') of a canonical/atomic natural deduction (see \cref{cha:canonical}). + The content of cut-elimination for sequent calculus corresponds more closely to $\beta$-reduction in natural deduction (see \cref{sec:beta-eta}). + % or to the cut-elimination (``hereditary substitution'') of a canonical/atomic natural deduction (see \cref{cha:canonical}). This difference is also evident in the fact that we have to assert the full identity rule in natural deduction. \end{rmk} @@ -1420,11 +1421,12 @@ \section{Categories with products} A natural deduction includes both introduction and elimination rules, so we will always be able to introduce a type and then eliminate it, essentially ``doing nothing''. By contrast, in a sequent calculus we have ``only introduction rules'' (of both left and right sorts), so this cannot happen. -In fact, in the simple case of categories with products, there are tricks enabling us to eliminate \emph{both} kinds of redundancy, and thereby do without any ``$\equiv$'' for both the sequent calculus and the natural deduction. -However, in even slightly more complicated theories the analogous tricks do not eliminate $\equiv$ completely, though they do reduce its complexity. -Thus, we focus in this section on theories with $\equiv$; we will return to the tricks in \cref{cha:canonical}. +In fact, in the simple case of categories with products, there are tricks enabling us to eliminate {both} kinds of redundancy, and thereby do without any ``$\equiv$'' for both the sequent calculus and the natural deduction. +However, in even slightly more complicated theories the analogous tricks do not eliminate $\equiv$ completely (though they do reduce its complexity). +Thus, we will focus on theories with $\equiv$. +% ; we will return to the tricks in \cref{cha:canonical}. -It is convenient to describe the reduction rules using a term syntax for derivations, as introduced in \cref{sec:category-cutadm}. +It is convenient to describe the rules for $\equiv$ using a term syntax for derivations, as introduced in \cref{sec:category-cutadm}. If we think of $A\times B$ as the ``type of pairs consisting of one element of $A$ and one element of $B$'', then it is natural to represent the $\timesI/\timesR$ rule as a pair of terms, one in $A$ and one in $B$. This idea leads us to write the natural deduction rules from \cref{sec:natded-mslat} as: \begin{mathpar} @@ -1437,7 +1439,8 @@ \section{Categories with products} \end{mathpar} Note how well the natural-deduction choice of ``all rules acting on the right'' matches the use of abstract variables: in all cases we can think of ``applying functions to arguments'' in a familiar way. It is possible to describe sequent calculus derivations using terms as well, but they are less pretty. -For this reason, we will henceforth use sequent calculus only for posetal theories, with a brief exception in \cref{sec:focusing}. +For this reason, we will henceforth use sequent calculus only for posetal theories. +% with a brief exception in \cref{sec:focusing}. The need to impose the identity rule for all types (not just those coming from \cG) also makes perfect sense from the abstract variable standpoint: a variable in any type is also a term of that type. @@ -1500,7 +1503,7 @@ \section{Categories with products} This suggests that we should be able to ``reduce'' an arbitrary term to a ``simplest possible form'' by successively applying $\beta$- and $\eta$-conversions. Such is indeed the case (although for technical reasons the $\eta$-conversion is usually applied in the less intuitive right-to-left direction and called an ``expansion'' rather than a ``reduction''.). This \emph{process of reduction} (and expansion) belongs to the ``computational'' side of type theory, which (though of course important in its own right) is somewhat tangential to our category-theoretic emphasis, so we will not discuss it in detail. - (However, in \cref{cha:canonical} we will directly characterize the \emph{result of reduction}, and thereby implicitly the process thereof.) + % (However, in \cref{cha:canonical} we will directly characterize the \emph{result of reduction}, and thereby implicitly the process thereof.) \end{rmk} \begin{thm}\label{thm:catprod-subadm} @@ -1695,7 +1698,9 @@ \section{Categories with coproducts} Similarly, the $\eta$-conversion rule\footnote{In fact, for types such as coproducts with a left universal property, there is no consensus on exactly what equality ``$\eta$'' refers to.\label{fn:weak-eta} From a categorical point of view this equality is the most natural, since like the $\eta$-conversion rule for products it expresses the uniqueness aspect of the universal property. But sometimes $\eta$ is used to refer only to the special case $\case(y,u.\inl(u),v.\inr(v))\equiv y$, which is also analogous to the $\eta$ rule for products in that it says that elements \emph{of the type in question} have a canonical form (a pair in a product or a case-split in a coproduct). - The relationship between these two, which involves ``commuting conversions'', is discussed further in \cref{cha:canonical}.} should say that morphisms out of a coproduct are determined uniquely by their composites with the projections: + The stronger property is equivalent to the weaker property combined with ``commuting conversions'' such as $\inl(\case(M,u.P,v.Q)) \equiv \case(M,u.\inl(P),v.\inl(Q))$.% + % The relationship between these two, which involves ``commuting conversions'', is discussed further in \cref{cha:canonical}. +} should say that morphisms out of a coproduct are determined uniquely by their composites with the projections: \begin{equation} \case(y,u.P[\inl(u)/y],v.P[\inr(v)/y]) \equiv P\label{eq:catcoprod-eta} \end{equation} @@ -1732,8 +1737,8 @@ \section{Categories with coproducts} Finally, we show by a further induction that this extension is actually a functor (preserves all composites). \end{proof} -At this point the reader is free (after doing some exercises) to move on directly to \cref{chap:simple}. -However, if you want to understand $\equiv$ a little more deeply, you may also continue with the somewhat digressive \cref{cha:canonical}. +% At this point the reader is free (after doing some exercises) to move on directly to \cref{chap:simple}. +% However, if you want to understand $\equiv$ a little more deeply, you may also continue with the somewhat digressive \cref{cha:canonical}. \subsection*{Exercises} @@ -1804,648 +1809,6 @@ \subsection*{Exercises} \end{ex} -\chapter{Computation and Canonicity} -\label{cha:canonical} - -[TODO: Is this chapter a good idea at all?] - -As observed in \cref{rmk:beta-reduction}, the $\beta$-reduction rule can be seen as a ``directed simplification'': clearly $M$ is simpler than $\pi_1(\pair M N)$. -Put differently, the derivation leading to the term $\pi_1(\pair M N)$ is ``redundant'' since it represents a morphism that already had a representative, namely $M$. -In this chapter we study theories that (at least partially) prevent such redundancy from occurring, eliminating (or reducing) the need for the equivalence relations $\equiv$ in presenting free categories. - -The idea is to prevent application of elimination rules (such as $\pi_1$) to terms resulting from introduction rules (such as $\pair M N$). -We do, of course, have to be able to apply elimination rules to some terms, in order to derive, say, $x:A\times B \types \pi_1(x):A$. -To distinguish between the ``terms that can be eliminated'' and those that can't, we replace the single judgment $x:A\types M:B$ with two: -\begin{mathpar} - x:A \types M\atom B\and - x:A \types M\can B. -\end{mathpar} -We read $M\atom B$ as ``$M$ is an \textbf{atomic} term of type $B$'' and $M\can B$ as ``$M$ is a \textbf{canonical} term of type $B$''. -Intuitively, the canonical terms are a subset of the ordinary ones with the property of being ``canonical representatives'' of a morphism in a free category. -If we succeed at proving an initiality theorem without needing to impose any equivalence relation on terms, then it will follow that in fact, every $\equiv$-equivalence class of ordinary terms has \emph{exactly one} representative that is ``canonical'' in the current sense. -Moreover, by translating the theories with $\equiv$ into the theories without $\equiv$ we obtain a ``reduction'' operation that computes the canonical form of any term. - - -\section{Categories with products} -\label{sec:atomcan-catprod} - -We consider first the case of categories with products only. -We assert the same natural deduction rules as before, but now with annotations describing which terms are canonical and which are atomic. -\begin{mathpar} - \inferrule{\types X\type}{x:X\types x\atom X}\;\idfunc\and - \inferrule{f\in \cG(A,B) \\ x:X\types M\can A}{x:X\types f(M)\atom B}\;fI\and - \inferrule{\types X\type}{x:X\types \ttt\can \unit}\;\unit I\and - \inferrule{x:X\types M\atom B\times C}{x:X \types \pi_1(M)\atom B}\;\timesE1\and - \inferrule{x:X\types M\atom B\times C}{x:X \types \pi_2(M)\atom C}\;\timesE2\and - \inferrule{x:X\types M\can B \\ x:X\types N\can C}{x:X\types \pair MN\can B\times C}\;\timesI -\end{mathpar} -Note particularly that in the $\timesE$ rules, $M$ must be atomic; whereas in the $\timesI$ rule, $\pair MN$ is only canonical; thus $\pi_1(\pair MN)$ cannot be formed. -We allow $M$ and $N$ in the $\timesI$ rule to also be canonical, so that we can form iterated pairs such as $\pair M{\pair NP}$; while similarly we say that $\pi_1(M)$ and $\pi_2(M)$ are again atomic, so that we can form iterated projections such as $\pi_1(\pi_2(M))$. -All variables are atomic, so that we can form $x:A\times B \types \pi_1(x):A$. - -Of course, this division into atomic and canonical is an artifact of the syntax; it has no natural counterpart in category theory. -Thus, to extract a description of a free category with products, we need some way to combine the two kinds of terms to describe one kind of morphism. -It turns out that the best way to do this is to assert that any atomic term \emph{belonging to a base type} (i.e.\ an object of \cG) is also canonical: -\begin{mathpar} - \inferrule{B\in\cG \\ x:A \types M\atom B}{x:A\types M\can B}\;\atomcan -\end{mathpar} -and then regard the canonical terms as the morphisms. -This completes the definition of our \textbf{unary canonical/atomic calculus for categories with products}. - -At this point it is a little difficult to explain why we regard a term of the form $f(M)$ to be atomic but allow the argument $M$ to be canonical. -It doesn't make much difference what choice we make regarding this rule in our current very simple theory, since both $M$ and $f(M)$ always belong to a base type, and for base types there is no difference between atomic and canonical terms (the only way to make a canonical term of a base type is to apply $\atomcan$). -So we just ask the reader to take our word for it that this choice is the best one; it will make more sense later [TODO]. - -The restriction $B\in\cG$ in $\atomcan$ is what removes the redundancy expressed by the \emph{other} generator of $\equiv$, namely the $\eta$-conversion $\pair{\pi_1(M)}{\pi_2(M)}\equiv M$. -However, it deals with it in a surprising way: it is the seemingly ``more complicated'' term $\pair{\pi_1(M)}{\pi_2(M)}$ that we regard as canonical! -For example, when $x=M$ we have the following derivation in our new system: -\begin{mathpar} - \inferrule*[Right=\timesI]{ - \inferrule*[Right=\atomcan]{ - \inferrule*[Right=\timesE]{\inferrule*{ }{x:A\times B\types x\atom A\times B}}{x:A\times B \types \pi_1(x)\atom A} - }{x:A\times B \types \pi_1(x)\can A} \\ - \inferrule*[Right=\atomcan]{ - \inferrule*[Right=\timesE]{\inferrule*{ }{x:A\times B\types x\atom A\times B}}{x:A\times B \types \pi_2(x)\atom B} - }{x:A\times B \types \pi_2(x)\can B} - }{ - x:A\times B \types \pair{\pi_1(x)}{\pi_2(x)}\can A\times B - } -\end{mathpar} -but while we have $x:A\times B\types x\atom A\times B$, we cannot apply $\atomcan$ to deduce $x:A\times B\types x\can A\times B$ since $A\times B$ is not a base type. -Put differently, when transforming an arbitrary term into a canonical one, we regard the $\beta$-conversion as a reduction, but the $\eta$-conversion as an \emph{expansion}. - -There are various reasons for this choice, foremost among which is that it works well. -Philosophically, it can be justified by saying that the type $A\times B$ is supposed to be a ``type whose elements are pairs'', and therefore the \emph{canonical form} of any element of it (even a variable) should \emph{be a pair}. -A category theorist can gain some intuition for it by thinking of $\beta$-reduction as analogous to the multiplication transformation $T^2\to T$ of a monad, while the $\eta$-expansion is analogous to the unit transformation $\mathsf{Id}\to T$. -In an example such as the free monoid monad, the multiplication ``simplifies'' a list $((a,b),(),(c,d,e))$ by removing redundant parentheses to get $(a,b,c,d,e)$, while the unit makes an element $a$ into a list $(a)$ by \emph{adding} parentheses. -Na\"ively one might say that $(a)$ is more complicated than $a$, but it has the virtue of being in the same ``canonical form'' as every other list. - -\begin{rmk} - Recall that we generally want to regard terms as simply a different syntactic representation of derivations, with a parse tree that inverts the derivation tree. - This is almost true for our current system: the only rule that breaks it is $\atomcan$, which uses the same term $M$ to represent two different derivations (one of $M\atom B$, and one of $M\can B$ obtained by following the former with $\atomcan$). - However, this can be regarded as simply a convenient abuse of notation: since otherwise the syntaxes producing atomic and canonical terms are disjoint, if when parsing $M\can B$ we see that $M$ looks like an atomic term, it must be that it was deduced from $\atomcan$ and so we can insert an appropriate node into the tree. -\end{rmk} - -The central lemma that justifies this theory is, as usual, the admissibility of cut/substitution. - -\begin{lem}\label{thm:catprod-atomcan-subadm} - The following two cut rules are admissible in the unary canonical/atomic calculus for categories with products. - \begin{enumerate} - \item If $x:A\types M\can B$ and $y:B\types N\atom C$ are derivable, then either $x:A\types P\atom C$ or $x:A\types P\can C$ is derivable for some $P$.\label{item:catprod-atomcan-subadm-1} - \item If $x:A\types M\can B$ and $y:B\types N\can C$ are derivable, then $x:A\types P\can C$ is derivable for some $P$.\label{item:catprod-atomcan-subadm-2} - \end{enumerate} -\end{lem} -For purposes of composition in a free category with products, we are mainly interested in~\ref{item:catprod-atomcan-subadm-2}. -However, for the induction to go through we must also prove~\ref{item:catprod-atomcan-subadm-1} by a simultaneous induction on derivations of both. -\begin{proof} - Here are the inductive cases for the derivation of $y:B\types N\atom C$: - \begin{itemize} - \item If it ends with $\idfunc$, then $B=C$ and $N=y$, whence $x:A\types M\can B$ is our desired result. - \item If it ends with $fI$ for some $f\in\cG(D,C)$, then $N=f(N')$ and $y:B\types N'\can D$. - Thus, by the inductive hypothesis of~\ref{item:catprod-atomcan-subadm-2}, we have $x:A\types P'\can D$. - Applying $fI$ again, we have $x:A\types f(P')\atom C$. - \item If it ends with $\timesE1$, then we have $N=\pi_1(N')$ and $y:B\types N'\atom C\times D$. - Thus, inductively we have $x:A\types P'\can C\times D$. - This is where the interesting thing happens: since $P'$ is canonical rather than atomic, we can't apply $\timesE1$ directly to obtain $\pi_1(P')$. - Instead we observe that \emph{any canonical term of $C\times D$ must be of the form $\pair PQ$}, simply because the only rule that builds canonical terms of a product type is $\timesI$. - Thus, we must have $P'=\pair PQ$ where $x:A\types P\can C$ and $x:A\types Q\can D$. - But $x:A\types P\can C$ is exactly what we wanted. - (Of course, the case of $\timesE2$ is symmetric.) - \end{itemize} - And here are the inductive cases for the derivation of $y:B\types N\can C$: - \begin{itemize} - \item If it ends with $\unit I$, then $C=\unit$ and so $x:A\types \ttt\can \unit$. - \item If it ends with $\timesI$, then $N=\pair{N_1}{N_2}$ with $y:B\types N_1\can C_1$ and $y:B\types N_2\can C_2$. - Thus, inductively we have $x:A\types P_1:C_1$ and $x:A\types P_2:C_2$, whence $x:A\types \pair{P_1}{P_2}\can C$. - \item If it ends with $\atomcan$, then we have $y:B\types N\atom C$, and hence by the inductive hypothesis of~\ref{item:catprod-atomcan-subadm-1} we have either $x:A\types P\atom C$ or $x:A\types P\can C$. - In the second case we are done. - In the first case, since we already applied $\atomcan$ at type $C$, $C$ must be a base type, so we can apply $\atomcan$ again to conclude $x:A\types P\can C$.\qedhere - \end{itemize} -\end{proof} - -Like \cref{thm:category-cutadm,thm:catprod-subadm}, the proof of \cref{thm:catprod-atomcan-subadm} defines a ``substitution'' operation (well, technically, two operations) on terms, which we write as $N\hsub{M/y}$. -However, compared to ordinary substitution, this operation is more powerful: it also performs ``$\beta$-simplification'' as it goes. -For instance, we have -\[ \pi_1(y)\hsub{\pair M N/y} = M \] -whereas ordinary substitution would give $\pi_1(\pair M N)$. -In type-theoretic lingo, this ``reducing substitution'' is called \textbf{hereditary substitution}. -Its recursive defining clauses are -\begin{align*} - y\hsub{M/y} &= M\\ - f(N)\hsub{M/y} &= f(N\hsub{M/y})\\ - \ttt\hsub{M/y} &= \ttt\\ - \pi_1(N)\hsub{M/y} &= P \qquad\text{where }N\hsub{M/y}=\pair P Q\\ - \pi_2(N)\hsub{M/y} &= Q \qquad\text{where }N\hsub{M/y}=\pair P Q\\ - \pair P Q \hsub{M/y} &= \pair{P\hsub{M/y}}{Q\hsub{M/y}}. -\end{align*} - -In particular, hereditary substitution implies that the usual natural deduction rules are also \emph{admissible} for canonical terms. -For instance, given a canonical term $x:X \types M\can A\times B$, we can construct a canonical term $x:X\types M' \can A$, even though $\pi_1$ cannot be applied directly to canonical terms; we can take $M' = \pi_1(y)\hsub{M/y}$. -(It may be tempting to write this as ``$\pi_1(M)$'', but that would probably be confusing since it hides the fact that a meta-operation on syntax is occurring, as we can't directly apply $\pi_1$ to $M$.) - -This gives our promised way to ``reduce'' terms in the type theory from \cref{sec:beta-eta}. -Like we did in \cref{sec:category-cutadm} for the cut-ful type theory of \cref{sec:category-cutful}, since all the rules of \cref{sec:beta-eta} are admissible in our canonical/atomic calculus, we can interpret any derivation --- and hence any term --- in that type theory into our current one. -With projections defined in terms of hereditary substitution as in the previous paragraph, the net effect of this is to automatically reduce all applications of a projection to a pair. - -Now recall that in ordinary natural deduction, we don't need to (and, indeed, can't) prove that identity rule $A\types A$ is also admissible; hence we assume the ``use a variable'' rule $x:A\types x:A$. -However, in the canonical/atomic calculus, we have only assumed that variables are \emph{atomic}; thus we need to also prove that there are \emph{canonical} identities. - -\begin{lem}\label{thm:catprod-atomcan-idadm} - If $\types A\type$ is derivable, then there is a term $\hid{A}(x)$ such that $x:A \types \hid{A}(x)\can A$. -\end{lem} -\begin{proof} - We induct on the derivation of $\types A\type$. - \begin{itemize} - \item If $A\in\cG$ is a base type, then we can apply $\atomcan$ to derive $x:A \types x\can A$. - \item If $A=\unit$, then $x:\unit \types \ttt\can \unit$. - \item If $A=A_1\times A_2$, then by induction we have $y:A_1 \types \hid{A_1}(y)\can A_1$ and $z:A_2 \types \hid{A_2}(z)\can A_2$. - Thus, $x:A \types \hid{A_1}(y)\hsub{\pi_1(x)/y}\can A_1$ and $x:A \types \hid{A_2}(z)\hsub{\pi_2(x)/z}\can A_2$, so we have - \[ x:A \types \pair{\hid{A_1}(y)\hsub{\pi_1(x)/y}}{\hid{A_2}(z)\hsub{\pi_2(x)/z}} \can A.\qedhere\] - \end{itemize} -\end{proof} - -As a recursively defined operation, the clauses of $\hid{A}$ are thus -\begin{align*} - \hid{A}(x) &= x \qquad\text{if }{A\in\cG}\\ - \hid{\unit}(x) &= \ttt\\ - \hid{A\times B}(x) &= \pair{\hid{A}(y)\hsub{\pi_1(x)/y}}{\hid{B}(z)\hsub{\pi_2(x)/z}}. -\end{align*} -Note that the hereditary substitution in the last clause is not doing any $\beta$-reduction, since the identity terms being substituted into are built only out of variables and pairs. -For instance, we have -\[ \hid{A\times (B\times C)}(x) = \pair{\pi_1(x)}{\pair{\pi_1(\pi_2(x))}{\pi_2(\pi_2(x))}} \] - -\begin{lem}\label{thm:atomcan-catprod-subassoc} - Hereditary substitution and identities form a category: - \begin{align*} - P\hsub{N/z}\hsub{M/y} &= P\hsub{N\hsub{M/y}/z}\\ - \hid{A}(y)\hsub{M/y} &= M\\ - N\hsub{\hid{A}(x)/y} &= N[x/y]. - \end{align*} -\end{lem} -\begin{proof} - Left to the reader as \cref{ex:atomcan-catprod-subassoc}. -\end{proof} - -\begin{thm}\label{thm:atomcan-catprod-initial} - For any directed graph \cG, the free category with finite products generated by \cG can be described by the unary canonical/atomic calculus for categories with products under \cG, without any quotienting: its objects are the types $A$ such that $\types A\type$ is derivable, and its morphisms $A\to B$ are the terms $M$ such that $x:A \types M\can B$ is derivable. -\end{thm} -\begin{proof} - \cref{thm:atomcan-catprod-subassoc} gives us a category, which we denote $\F\bPrCat\cG$. - The interesting thing is the proof that $\F\bPrCat\cG$ has finite products. - The product of $A$ and $B$ is, of course, supposesd to be $A\times B$, with projections - \begin{align*} - z:A\times B &\types \pi_1(w)\hsub{z/w}\can A\\ - z:A\times B &\types \pi_2(w)\hsub{z/w}\can B - \end{align*} - (We can't write $\pi_1(z)$ because $A$ may not be a base type.) - Now given any morphisms $x:X \types M\can A$ and $x:X \types N\can B$, we can certainly form $x:X \types \pair M N \can A\times B$, and its composite with $\pi_1$ is - \[ \pi_1(w)\hsub{z/w}\hsub{\pair M N/z} = \pi_1(w)\hsub{z\hsub{\pair M N/z}/w} = \pi_1(w)\hsub{\pair M N/w} = M \] - using the associativity of hereditary substitution and the definition of hereditary substitution on $\pi_1$. - Of course, the case of $\pi_2$ is similar. - In the other direction, given any morphism $x:X \types P\can A\times B$, as observed in the proof of \cref{thm:catprod-atomcan-subadm} $P$ must be a pair $\pair M N$ where $x:X\types M\can A$ and $x:X\types N\can B$, and for the same reasons $M$ and $N$ are the composites of $P$ with $\pi_1$ and $\pi_2$ respectively. - Thus, $A\times B$ has the universal property of a product with respect to \emph{syntactic equality} of terms/derivations. - - Now if \cM is a category with finite products and $P:\cG\to\cM$ a graph morphism, we extend $P$ to $\F\bPrCat\cG$ just as before by recursion on derivations. - We have to define $P$ on both atomic and canonical terms for the recursion to go through (since the atomic and canonical terms are defined by mutual induction); since there is no separation between ``atomic and canonical morphisms'' in \cM we just send both kinds of term to ordinary morphisms in \cM. - As usual, the defining clauses in this recursion are forced by functoriality and product-preservation, and we can then prove by induction on derivations that the resulting operation actually is a functor. -\end{proof} - - -\subsection*{Exercises} - -\begin{ex}\label{ex:atomcan-catprod-subassoc} - Prove \cref{thm:atomcan-catprod-subassoc} (hereditary substitution is associative). -\end{ex} - -\begin{ex}\label{ex:atomcan-catfib} - Formulate a canonical/atomic calculus for fibrations of categories and prove its initiality theorem. - Then do the same for fibrations of categories with products, as in \cref{ex:catprod-fib}. -\end{ex} - - -\section{Categories with coproducts} -\label{sec:atomcan-catcoprod} - -Now we consider a canonical/atomic calculus for categories with coproducts. -In general, objects with left (``mapping out'') universal properties are trickier to deal with in natural deduction systems, because our terms only appear on the \emph{right} of the $\types$. -We begin by rewriting the theory of \cref{sec:catcoprod} with atomic and canonical annotations; see \cref{fig:catcoprod-atomcan}. -\begin{figure} - \centering - \begin{mathpar} - \inferrule{\types X\type}{x:X\types x\atom X}\;\idfunc\and - \inferrule{f\in \cG(A,B) \\ x:X\types M\can A}{x:X\types f(M)\atom B}\;fI\and - \inferrule{x:X \types M\atom \zero \\ \types C\type}{x:X \types \abort(M)\can C}\;\zeroE\\ - \inferrule{x:X\types M\can A}{x:X\types \inl(M)\can A + B}\;\plusI1\and - \inferrule{x:X\types N\can B}{X\types \inr(N)\can A + B}\;\plusI2\and - \inferrule{u:A\types P\can C \\ v:B\types Q\can C \\ x:X\types M\atom A + B}{x:X\types \case(M,u.P,v.Q)\can C}\;\plusE\and - \inferrule{B\in\cG\\ x:A \types M\atom B}{x:A\types M\can B}\;\atomcan - \end{mathpar} - \caption{Unary canonical/atomic calculus for categories with coproducts} - \label{fig:catcoprod-atomcan} -\end{figure} -The principle is the same: we prevent ourselves from eliminating on the results of introduction rules by requiring elimination rules to act only on atomic terms. -The only perhaps surprising thing is that the ``branches'' $P,Q$ of $\case$, and the $\case$ term itself, are canonical, though the ``branch term'' $M$ must be atomic. - -The proof of admissibility of (hereditary) substitution for this theory is more complicated because of the presence of the rules $\zeroE$ and $\plusE$. -In \cref{sec:atomcan-catprod} we could see by inspection that canonical terms of a certain type must have a certain form, but $\zeroE$ and $\plusE$ can produce canonical terms of any type at all. - -\begin{thm}\label{thm:atomcan-catcoprod-subadm} - The following rules are admissible in the unary canonical/atomic calculus for categories with coproducts under \cG: - \begin{enumerate} - \item Hereditary substitution into atomic terms: if $x:A\types M\can B$ and $y:B\types N\atom C$ are derivable, then either $x:A\types P\atom C$ or $x:A\types P\can C$ is derivable for some $P$.\label{item:catcoprod-atomcan-subadm-1} - \item Hereditary substitution into canonical terms: if $x:A\types M\can B$ and $y:B\types N\can C$ are derivable, then $x:A\types P\can C$ is derivable for some $P$.\label{item:catcoprod-atomcan-subadm-2} - \end{enumerate} -\end{thm} -\begin{proof} - By mutual induction. - We outline the cases for each statement as follows. - \begin{enumerate} - \item A derivation of $y:B\types N\atom C$ can only end with $\idfunc$ and $fI$. - Both cases are just like those in \cref{thm:catprod-atomcan-subadm}; - recall that the second case uses the inductive hypothesis of~\ref{item:catcoprod-atomcan-subadm-2}. - \item A derivation of $y:B\types N\can C$ can end with $\atomcan$, $\plusI1$, $\plusI2$, $\zeroE$, or $\plusE$. - \begin{itemize} - \item If it ends with $\atomcan$, we apply the inductive hypothesis of~\ref{item:catcoprod-atomcan-subadm-1}. - \item If $N=\inl(N')$ with $y:B\types N'\can C_1$, then by the inductive hypothesis $x:A\types N'\hsub{M/y}\can C_1$ and so $x:A\types \inl(N'\hsub{M/y})\can C$. - The case of $\inr$ is dual. - \item If $N=\case(N',u.P,v.Q)$ with $y:B\types N'\atom D+E$ and $u:D\types P\can C$ and $v:E\types Q\can C$, then since the only rule that can produce an atomic term of type $D+E$ is $\idfunc$, we must have $B=D+E$ and $N'=y$. - % In a more general case, we would inspect the last rule in the derivation; the other ways to produce an atomic term could then be substituted by the inductive hypothesis of~\ref{item:catcoprod-atomcan-subadm-1} to give an atomic $N'\hsub{M/y}\atom D+E$ that we can apply $\case$ to directly. - Now we do a secondary inner induction on the derivation of $x:A\types M\can B$, which can likewise end with $\plusI1$, $\plusI2$, or $\zeroE$ or $\plusE$. - \begin{itemize} - \item If $M=\inl(M')$, then by the inductive hypothesis we have $x:A\types P\hsub{M'/u}\can C$. - \item Dually, if $M=\inr(M')$, we have $x:A\types Q\hsub{M'/v}\can C$. - \item If $M=\abort(M')$, then $x:A\types \abort(M')\can C$. - \item If $M=\case(M',w.S,z.T)$ with $x:A\types M'\atom F+G$ and $w:F\types S\can D+E$ and $z:G\types T\can D+E$, then - by the inner inductive hypothesis we have $w:F\types S'\can C$ and $z:G\types T'\can C$. - Thus, applying $\plusE$ we have $x:A\types \case(M',w.S',z.T')\can C$. - \end{itemize} - \item The case when $N=\abort(N')$ with $y:B\types N'\atom\zero$ is similar, but simpler. - We must have $B=\zero$ and $N'=y$, and we induct on the derivation of $x:A\types M\can B$, which must end with $\zeroE$ or $\plusE$. - \begin{itemize} - \item If $M=\abort(M')$, then $x:A\types \abort(M')\can C$. - \item If $M=\case(M',w.S,z.T)$ with $x:A\types M'\atom F+G$ and $w:F\types S\can \zero$ and $z:G\types T\can \zero$, then - by the inner inductive hypothesis we have $w:F\types S'\can C$ and $z:G\types T'\can C$, whence $x:A \types \case(M',w.S',z.T')\can C$.\qedhere - \end{itemize} - \end{itemize} - \end{enumerate} -\end{proof} - -\begin{figure} - \centering - \begin{align*} - y\hsub{M/y} &= M\\ - f(N)\hsub{M/y} &= f(N\hsub{M/y})\\ - \inl(N)\hsub{M/y} &= \inl(N\hsub{M/y})\\ - \inr(N)\hsub{M/y} &= \inr(N\hsub{M/y})\\ - \abort(y)\hsub{M/y} &= \abort'(M)\\ - \case(y,u.P,v.Q)\hsub{M/y} &= \case'(M,u.P,v.Q)\\ - \\ - \abort'(\abort(M)) &= \abort(M)\\ - \abort'(\case(M,u.P,v.Q)) &= \case(M,u.\abort'(P),v.\abort'(Q))\\ - \\ - \case'(\inl(M),u.P,v.Q) &= P\hsub{M/u}\\ - \case'(\inr(M),u.P,v.Q) &= Q\hsub{M/v}\\ - \case'(\abort(M),u.P,v.Q) &= \abort(M)\\ - \case'(\case(M,w.S,z.T),u.P,v.Q) &= \case(M,w.\case'(S,u.P,v.Q),z.\case'(T,u.P,v.Q)) - \end{align*} - \caption{Hereditary substitution for categories with coproducts} - \label{fig:catcoprod-hsub} -\end{figure} - -The resulting definition of hereditary substitution is shown in \cref{fig:catcoprod-atomcan}. -We have introduced notation $\abort'$ and $\case'$ for the operations defined by the inner recursions in the proof. -Note that these essentially constitute proofs that the unrestricted $\zeroE$ and $\plusE$ rules are admissible, just as the hereditary substitution from \cref{sec:atomcan-catprod} yielded an admissible unrestricted $\timesE$. - -The identity rule is much easier: - -\begin{thm}\label{thm:atomcan-catcoprod-idadm} - The canonincal identity rule is admissible: if $\types A\type$, then $x:A \types \hid{A}(x)\can A$. -\end{thm} -\begin{proof} - The defining clauses are - \begin{align*} - \hid{A}(x) &= x \quad\text{if }A\in \cG\\ - \hid{\zero}(x) &= \abort(x)\\ - \hid{A+B}(x) &= \case(x,u.\hid{A}(u),v.\hid{B}(v))\qedhere - \end{align*} -\end{proof} - -Like the admissible $\pi_1$ from \cref{sec:atomcan-catprod}, $\match'$ satisfies $\beta$-conversion as a syntactic equality (this is its first two defining clauses). -Unfortunately, this theory still does not validate the full $\eta$ rule for coproducts as a syntactic equality. -We do have the following weaker property: - -\begin{lem}\label{thm:atomcan-catcoprod-weaketa} - If $x:X \types M\can A+B$, then $M = \case'(M,u.\inl(u),v.\inr(v))$. - Similarly, if $x:X\types M\can\zero$, then $M=\abort'(M)$. -\end{lem} -\begin{proof} - An easy induction over the defining clauses of $\case'$ and $\abort'$. -\end{proof} - -In other words, it is still true (see footnote~\ref{fn:weak-eta}) that every term \emph{of type $A+B$} has a canonical form. -However, unlike the case of products this is insufficient to ensure the full uniqueness aspect of the universal property, since the ``mapping out'' universal property of $A+B$ constructs terms not of type $A+B$ itself but of some other type. -For instance, if we have -\begin{mathpar} - f\in\cG(A,C)\and - g\in\cG(B,C)\and - h\in\cG(C,D)\and -\end{mathpar} -then the induced morphism $A+B\to D$ is represented by both of the terms -\begin{align*} - x:A+B &\types \case(x,u.h(f(u)),v.h(g(v)))\can D\\ - x:A+B &\types h(\case(x,u.f(u),v.g(v)))\can D -\end{align*} -and these two terms are (syntactically) different, despite both yielding $h(f(u))$ and $h(g(v))$ under the hereditary substitutions $\hsub{\inl(u)/x}$ and $\hsub{\inr(v)/x}$. - -Thus, the terms/derivations in this type theory don't present a category with finite coproducts unless we impose some equivalence relation on them. -The above example also points the way to the correct equivalence relation. -We no longer need to assert $\beta$-conversion, nor do we need the weak form of $\eta$-conversion expressed by \cref{thm:atomcan-catcoprod-weaketa}; but we do need the relations shown in \cref{fig:catcoprod-commconv}. -\begin{figure} - \centering - \begin{align*} - f(\case(M,u.P,v.Q)) &\equiv \case(M,u.f(P),v.f(Q))\\ - \inl(\case(M,u.P,v.Q)) &\equiv \case(M,u.\inl(P),v.\inl(Q))\\ - \inr(\case(M,u.P,v.Q)) &\equiv \case(M,u.\inr(P),v.\inr(Q))\\ - \case(\case(M,u.P,v.Q),w.R,z.S) &\equiv \case(M,u.\case(P,w.R,z.S),v.\case(Q,w.R,z.S))\\ - \abort(\case(M,u.P,v.Q)) &\equiv \case(M,u.\abort(P),v.\abort(Q)) - \end{align*} - \caption{Commuting conversions for coproducts} - \label{fig:catcoprod-commconv} -\end{figure} -These are called \textbf{commuting conversions}. -They are a consequence of the strong form of $\eta$-conversion~\eqref{eq:catcoprod-eta}: -\begin{equation} - \inferrule{x:X \types M\atom A+B \\ y:A+B \types P\can C}{x:X \types \case(M,u.P[\inl(u)/y],v.P[\inr(v)/y]) \equiv P[M/y] \can C}\label{eq:catcoprod-eta-again} -\end{equation} -(take $P$ to be the left-hand side of each commuting conversion with $y$ in place of $M$). -Conversely, when combined with the weak $\eta$-conversion, the commuting conversions imply the strong $\eta$-conversion: - -\begin{thm}\label{thm:atomcan-catcoprod-eta} - If we augment the canonical/atomic calculus for categories with coproducts by an $\equiv$ on canonical terms generated by the relations in \cref{fig:catcoprod-commconv} (plus the usual congruence properties), then the strong $\eta$-rule~\eqref{eq:catcoprod-eta-again} is admissible. -\end{thm} -\begin{proof} - Induction on the derivation of $P$; each commuting conversion handles exactly one of the cases. -\end{proof} - -\begin{thm}\label{thm:atomcan-catcoprod-initial} - The free category with coproducts generated by a directed graph \cG can be presented by the canonical/atomic calculus for categories with coproducts modulo $\equiv$. -\end{thm} -\begin{proof} - Left to the reader as \cref{ex:atomcan-catcoprod-initial}. -\end{proof} - -[TODO: Molecular?] - - -\subsection*{Exercises} - -\begin{ex}\label{ex:atomcan-catcoprod-initial} - Prove \cref{thm:atomcan-catcoprod-initial} (initiality for the canonical/atomic calculus for categories with coproducts). -\end{ex} - -\begin{ex}\label{ex:atomcan-opfib} - Formulate a canonical/atomic calculus for opfibrations of categories, with an $\equiv$ for commuting conversions only, and prove its initiality theorem. - Then do the same for opfibrations of categories with coproducts. -\end{ex} - -\begin{ex}\label{ex:atomcan-prodcoprod} - Combine \cref{sec:atomcan-catprod,sec:atomcan-catcoprod} to give a canonical/atomic calculus for categories with both products and coproducts, and prove its initiality theorem. - (You will need some commuting conversions relating to $\timesI$ as well.) -\end{ex} - - -\section{Focusing} -\label{sec:focusing} - -For completeness, we now describe how the sequent calculus for meet-semilattices can also be modified to present free categories with products without needing an equivalence relation on terms. -This version is not as commonly used in categorical logic, but it is important in other applications of type theory, such as automated proof search; it is called \emph{focusing}. - -If we inspect the derivations of canonical terms in the type theory of \cref{sec:atomcan-catprod}, we see that they have the following form: first they apply some number of projections to variables, then they apply $\atomcan$, they apply some number of generating arrows between base types, and finally they apply some number of pairings. -For instance, if $f\in \cG(C,D)$ we have -\[x:(A\times B)\times C \types \pair{f(\pi_2(x))}{\pi_2(\pi_1(x))}\can D\times B\] -with derivation -\begin{mathpar} -\let\mytimes\times -\def\times{\mathord{\mytimes}} - \inferrule*{ - \inferrule*{\inferrule*{\inferrule*{ - x:(A\times B)\times C \types x\atom (A\times B)\times C - }{x:(A\times B)\times C \types \pi_2(x) \atom C - }}{x:(A\times B)\times C \types \pi_2(x) \can C - }}{x:(A\times B)\times C \types f(\pi_2(x)) \can D} - \\ - \inferrule*{\inferrule*{\inferrule*{ - x:(A\times B)\times C \types x\atom (A\times B)\times C - }{x:(A\times B)\times C \types \pi_1(x)\atom A\times B - }}{x:(A\times B)\times C \types \pi_2(\pi_1(x))\atom B} - }{x:(A\times B)\times C \types \pi_2(\pi_1(x))\can B} - }{x:(A\times B)\times C \types \pair{f(\pi_2(x))}{\pi_2(\pi_1(x))}\can D\times B} -\end{mathpar} -This suggests that we ought to consider as ``canonical'' the sequent calculus derivation that is closest to the above. -Roughly speaking, this means first applying left rules, then generators, then right rules\footnote{To be honest, we should point out that the fact that the canonical derivations can be described so simply is an artifact of the relative triviality of our current theory, with essentially only one operation $\times$. -One can still formulate canonical/atomic and focused versions of more general theories, but the canonical forms don't have as simple a description.}, as in the following derivation: -\begin{mathpar} - \inferrule*{ - \inferrule*{\inferrule*{C\types C - }{(A\times B)\times C \types C - }}{(A\times B)\times C \types D} - \\ - \inferrule*{\inferrule*{B \types B - }{A\times B \types B - }}{(A\times B)\times C \types B} - }{(A\times B)\times C \types D\times B} -\end{mathpar} -As in the natural deduction case, we can rule out the undesired sequent calculus derivations by using two judgments to indicate whether we are in the ``left phase'' or the ``right phase''. -We denote these by -\[ \focus{A} \types B -\qquad\text{and}\qquad -%A\types\focus{B} -A\types B -\] -respectively. -The brackets in the first case indicate that we are ``focused'' on the left side of the sequent. -You might think that in the second case we should write $A\types \focus B$ to indicate that we are focused on the right side, but in fact in the latter case we are not really ``focused'' at all; in more complicated situations there is also a ``right-focused'' judgment $A\types \focus B$ that is different from both $\focus A \types B$ and $A\types B$. -The asymmetry we see here is due to the fact that all universal properties we are considering are of the ``mapping in'' sort. - -We now modify the sequent calculus rules from \cref{sec:seqcalc-mslat} by stipulating that -the right rules only apply when we are in the right phase, -% \begin{mathpar} -% \inferrule{A\types \focus{B} \\ A\types \focus{C}}{A\types \focus{B\times C}}\and -% \inferrule{f\in \cG(A,B) \\ X\types \focus{A}}{X\types \focus{B}}\and -% \inferrule{\types A\type}{A\types \focus{\top}}\and -% \end{mathpar} -while the left rules apply only in the left phase; -% \begin{mathpar} -% \inferrule{A\in \cG}{\focus A\types A}\and -% \inferrule{\focus A\types C \\ \types B\type}{\focus {A\times B} \types C}\and -% \inferrule{\focus B\types C \\ \types A\type}{\focus{A\times B} \types C}\and -% \end{mathpar} -and we can transition from the left to the right phase, but not vice versa. -% \[ \inferrule{\focus A \types B}{A\types\focus B}\] -Since we are interested in distinguishing between derivations, we also annotate our sequents with terms; and -because the left rules of sequent calculus are not well-adapted to the use of formal variables, we go back to annotating the entire sequent with a term. -The rules with annotations for this \textbf{unary focused sequent calculus for categories with products} are shown in \cref{fig:catprod-focused-seqcalc}. - -\begin{figure} - \centering - \begin{mathpar} - % \inferrule{\phi:(A\types \focus{B}) \\ \psi:(A\types \focus{C})}{\pair{\phi}{\psi}:(A\types \focus{B\times C})}\and - % \inferrule{f\in \cG(A,B) \\ \phi:(X\types \focus{A})}{\postc f\phi:(X\types \focus{B})}\and - % \inferrule{\types A\type}{\ttt:(A\types \focus{\top})}\and - \inferrule{\phi:(A\types {B}) \\ \psi:(A\types {C})}{\pair{\phi}{\psi}:(A\types {B\times C})}\and - \inferrule{f\in \cG(A,B) \\ \phi:(X\types {A})}{\postc f\phi:(X\types {B})}\and - \inferrule{\types A\type}{\ttt:(A\types {\top})}\and - \inferrule{A\in \cG}{\idfunc_A:(\focus A\types A)}\and - \inferrule{\phi:(\focus A\types C) \\ \types B\type}{\prec{\phi}{\pi_1}:(\focus {A\times B} \types C)}\and - \inferrule{\phi:(\focus B\types C) \\ \types A\type}{\prec{\phi}{\pi_2}:(\focus{A\times B} \types C)}\and - \inferrule{\phi:(\focus A \types B)}{\phi:(A\types B)} - \end{mathpar} - \caption{Unary focused sequent calculus for categories with products} - \label{fig:catprod-focused-seqcalc} -\end{figure} - -For instance, the above derivation of $(A\times B)\times C \types D\times B$ can be given in the focused sequent calculus with term annotations as follows: -\begin{mathpar} - \let\mytimes\times - \def\times{\mathord{\mytimes}} - \inferrule*{ - \inferrule*{\inferrule*{\inferrule*{\idfunc_C:(\focus C\types C) - }{\prec{\idfunc_C}{\pi_2}:(\focus{(A\times B)\times C} \types C) - }}{\prec{\idfunc_C}{\pi_2}:((A\times B)\times C \types C) - }}{\postc{f}{\prec{\idfunc_C}{\pi_2}}:((A\times B)\times C \types D)} - \\ - \inferrule*{\inferrule*{\inferrule*{\idfunc_B:(\focus B \types B) - }{\prec{\idfunc_B}{\pi_2}:(\focus{A\times B} \types B) - }}{\prec{\prec{\idfunc_B}{\pi_2}}{\pi_1}:(\focus{(A\times B)\times C} \types B) - }}{\prec{\prec{\idfunc_B}{\pi_2}}{\pi_1}:((A\times B)\times C \types B)} - }{\pair{\postc{f}{\prec{\idfunc_C}{\pi_2}}}{\prec{\prec{\idfunc_B}{\pi_2}}{\pi_1}} - :((A\times B)\times C \types {D\times B})} - % \inferrule*{ - % \inferrule*{\inferrule*{\inferrule*{\idfunc_C:(\focus C\types C) - % }{\prec{\idfunc_C}{\pi_2}:(\focus{(A\times B)\times C} \types C) - % }}{\prec{\idfunc_C}{\pi_2}:((A\times B)\times C \types \focus C) - % }}{\postc{f}{\prec{\idfunc_C}{\pi_2}}:((A\times B)\times C \types \focus D)} - % \\ - % \inferrule*{\inferrule*{\inferrule*{\idfunc_B:(\focus B \types B) - % }{\prec{\idfunc_B}{\pi_2}:(\focus{A\times B} \types B) - % }}{\prec{\prec{\idfunc_B}{\pi_2}}{\pi_1}:(\focus{(A\times B)\times C} \types B) - % }}{\prec{\prec{\idfunc_B}{\pi_2}}{\pi_1}:((A\times B)\times C \types \focus B)} - % }{\pair{\postc{f}{\prec{\idfunc_C}{\pi_2}}}{\prec{\prec{\idfunc_B}{\pi_2}}{\pi_1}} - % :((A\times B)\times C \types \focus{D\times B})} -\end{mathpar} - -As usual, we need to prove the admissibility of identity and cut. -The proof of cut is very similar to that of \cref{thm:catprod-atomcan-subadm}. - -\begin{lem}\label{thm:focused-catprod-cutadm} - The following two cut rules are admissible in the unary focused sequent calculus for categories with products. - \begin{enumerate} - \item If $A\types B$ and $\focus B\types C$, then $A\types C$.\label{item:focused-catprod-cutadm-1} - \item If $A\types B$ and $B\types C$, then $A\types C$.\label{item:focused-catprod-cutadm-2} - \end{enumerate} -\end{lem} -\begin{proof} - First we prove~\ref{item:focused-catprod-cutadm-1} by induction on the derivation of $\focus B\types C$. - \begin{itemize} - \item If it is $\idfunc_B$, then $A\types B$ is $A\types C$. - \item If it ends with $\pi_1$, then $B$ is $B_1\times B_2$ and we have $\focus B_1\types C$. - Now consider the derivation of $A\types B$, i.e.\ $A\types B_1\times B_2$. - \textit{A priori} this could end either with the ``unfocus'' rule or with the $\times R$ rule. - But in fact, the unfocus rule is impossible, because it is impossible to derive $\focus A\types B$ unless $B$ is a base type (this is an easy induction). - Thus, we must have $A\types B_1$ and $A\types B_2$, so we can apply the inductive hypothesis on $B_1$ to get $A\types C$. - \end{itemize} - Now we prove~\ref{item:focused-catprod-cutadm-2}, by induction on the derivation of $B\types C$. - \begin{itemize} - \item If it ends with the right rule for $\times$ or $\unit$, or the generator rule for $f$, we can simply apply the inductive hypothesis and then the same rule, as usual. - \item If it ends with the unfocus rule, then we apply part~\ref{item:focused-catprod-cutadm-1}.\qedhere - \end{itemize} -\end{proof} - -However, if we try to prove admissibility of identity directly, we run into problems. -We need the following lemma first. - -\begin{lem}\label{thm:focused-catprod-leftadm} - The unfocused left rules for $\times$ are admissible in the unary focused sequent calculus for categories with products. - That is, if we have a derivation of $A\types C$ and $\types B\type$, we can construct a derivation of $A\times B\types C$, and dually. -\end{lem} -\begin{proof} - We induct on the derivation of $A\types C$. - \begin{itemize} - \item If it ends with the ``unfocus'' rule, whose premise is $\focus A\types C$, then we can apply the focused left rule to this to conclude $\focus{A\times B}\types C$, and then unfocus it to obtain $A\times B\types C$. - \item If it ends with the right rule for $\times$, then $C=C_1\times C_2$ and we have derivations of $A\types C_1$ and $A\types C_2$. - By the inductive hypothesis we get $A\times B\types C_1$ and $A\times B\types C_2$, whence $A\times B\types C$ by the right rule for $\times$. - \item If it ends with the generator rule for $f\in \cG(D,C)$, then we have a derivation of $A\types D$. - By the inductive hypothesis we get $A\times B\types D$, whence $A\times B\types C$. - \item Finally, if it ends with the right rule for $\unit$, then $C=\unit$, and so the same rule yields $A\times B\types C$.\qedhere - \end{itemize} -\end{proof} - -\begin{lem}\label{thm:focused-catprod-idadm} - The unfocused identity rule is admissible in the unary focused sequent calculus for categories with products. - That is, if $\types A\type$, then $A\types A$. -\end{lem} -\begin{proof} - Given \cref{thm:focused-catprod-leftadm}, we can use the same proof as \cref{thm:seqcalc-mslat-idadm}. -\end{proof} - -Of course, although the inductive argument for \cref{thm:focused-catprod-idadm} written in English is the same as that for \cref{thm:seqcalc-mslat-idadm}, the end result is different because we have the inductive construction of \cref{thm:focused-catprod-leftadm} frobnicating the results at each inductive step rather than simply applying the primitive left rule. -For instance, on $(A\times B)\times C$ the unmodified proof of \cref{thm:seqcalc-mslat-idadm} would give the derivation -\begin{mathpar} - \inferrule*{ - \inferrule*{\inferrule*{\inferrule*{A\types A}{A\times B\types A}\\ - \inferrule*{B\types B}{A\times B\types B} - }{A\times B\types A\times B} - }{(A\times B)\times C \types A\times B}\\ - \inferrule*{C\types C - }{(A\times B)\times C \types C} - }{(A\times B)\times C \types (A\times B)\times C} -\end{mathpar} -which cannot be ``focalized'' since it applies a left rule after a right rule. -Instead, from \cref{thm:focused-catprod-idadm} we obtain -\begin{mathpar} - \inferrule*{ - \inferrule*{ - \inferrule*{\inferrule*{\inferrule*{\focus A\types A}{\focus{A\times B}\types A} - }{\focus{(A\times B)\times C} \types A} - }{(A\times B)\times C \types A}\\ - \inferrule*{\inferrule*{\inferrule*{\focus B\types B}{\focus{A\times B}\types B} - }{\focus{(A\times B)\times C} \types B} - }{(A\times B)\times C \types B} - }{(A\times B)\times C \types A\times B}\\ - \inferrule*{\inferrule*{\focus C\types C - }{\focus {(A\times B)\times C} \types C} - }{(A\times B)\times C \types C} - }{(A\times B)\times C \types (A\times B)\times C} -\end{mathpar} -The resulting term is -\[ \pair{\pair{\prec{\prec{\idfunc_A}{\pi_1}}{\pi_1}}{\prec{\prec{\idfunc_B}{\pi_2}}{\pi_1}}}{\prec{\idfunc_C}{\pi_2}} : -({(A\times B)\times C \types (A\times B)\times C})\] - -We let the reader complete the argument (\cref{ex:focused-catprod-cutassoc,ex:focused-catprod-initial}). - -\begin{lem}\label{thm:focused-catprod-cutassoc} - Cut is associative and unital in the unary focused sequent calculus for categories with products.\qed -\end{lem} - -\begin{thm}\label{thm:focused-catprod-initial} - For any directed graph \cG, the free category with finite products generated by \cG can be described by the unary focused sequent calculus for categories with products under \cG, without any quotienting: its objects are the types $A$ such that $\types A\type$ is derivable, and its morphisms $A\to B$ are the terms $M$ such that $M:(A \types B)$ is derivable.\qed -\end{thm} - - -[TODO: Does focusing continue to identify unique canonical derivations in more complicated theories (with both positives and negatives)? Right now I think the answer is no, that we still need commuting conversions. How does focusing compare to canonical/atomic in theories with both positives and negatives? In theories with just positives, focusing should work just as well as in theories with just negatives, although canonical/atomic fails to give $\eta$.] - - -\subsection*{Exercises} - -\begin{ex}\label{ex:focused-catprod-cutassoc} - Prove \cref{thm:focused-catprod-cutassoc} (cut is associative and unital in the unary focused sequent calculus for categories with products). -\end{ex} - -\begin{ex}\label{ex:focused-catprod-initial} - Prove \cref{thm:focused-catprod-initial} (initiality for the unary focused sequent calculus for categories with products). -\end{ex} - - \chapter{Simple type theories} \label{chap:simple} @@ -4152,9 +3515,10 @@ \section{Rules and deductive systems} In many cases we can omit further information because it can be inferred from context; for instance, if we know that $h:C\to D$ then a term of the form ``$h\circ (-)$'' can only mean ``$h\circ_C (-)$''. Human mathematicians omit information informally and unsystematically, and we have done the same throughout the book. -The implementors of electronic mathematicians have elaborate and precise algorithms for ``inferring from context'' enabling the omission of information, but most of these are far beyond our scope.\footnote{One that is worth mentioning, however, is that a canonical/atomic calculus like that of \cref{sec:atomcan-catprod} can be type-checked in a ``bidirectional'' way. canonical terms $M\can A$ are type-checked as usual with both $M$ and $A$ being given, while atomic terms $M\atom A$ instead ``type-synthesize'': only $M$ is given and its type $A$ is deduced. - Paradoxically, this sometimes enables the omission of more information. - For instance, if when type-checking a function application $f(a)\can B$ the term $f$ can synthesize its type $A\to B$ (note that it is atomic since application is an elimination rule for a negative type), then we can extract the type $A$ at which we have to type-check the argument $a\can A$; thus the notation for function application doesn't need to notate the type $A$.} +The implementors of electronic mathematicians have elaborate and precise algorithms for ``inferring from context'' enabling the omission of information, but most of these are far beyond our scope. +% \footnote{One that is worth mentioning, however, is that a canonical/atomic calculus like that of \cref{sec:atomcan-catprod} can be type-checked in a ``bidirectional'' way. canonical terms $M\can A$ are type-checked as usual with both $M$ and $A$ being given, while atomic terms $M\atom A$ instead ``type-synthesize'': only $M$ is given and its type $A$ is deduced. +% Paradoxically, this sometimes enables the omission of more information. +% For instance, if when type-checking a function application $f(a)\can B$ the term $f$ can synthesize its type $A\to B$ (note that it is atomic since application is an elimination rule for a negative type), then we can extract the type $A$ at which we have to type-check the argument $a\can A$; thus the notation for function application doesn't need to notate the type $A$.} The other point I want to make is that with type-checking (and also ``proof search'') in mind, type theorists tend to read the rules of a deductive system ``bottom-up''. That is, instead of thinking of a rule @@ -4162,7 +3526,7 @@ \section{Rules and deductive systems} \inferrule*{\cJ_1 \\ \cJ_2}{\cJ} \end{mathpar} as meaning ``if we have $\cJ_1$ and $\cJ_2$ we can deduce $\cJ$'', they instead think ``if we want to deduce $\cJ$, it suffices to have $\cJ_1$ and $\cJ_2$''. -This is the direction that a type-checking algorithm applies the rule: given a parsed term $M$ and a putative type $A$, the rule tells us how to break down the job of checking that $M:A$ into simpler type-checking tasks that can be done recursively. +This is the direction that a type-checking algorithm applies the rule: given a parsed term $M$ and a putative type $A$, the rule tells us how to break down the job of checking that $M:A$ into simpler type-checking tasks that can be done recursively.\footnote{However, some more advanced theories are type-checked in a ``bidirectional'' way, with some judgments being read upwards in this way and others being read downwards as ``type synthesis'', where only the term is given and the type is inferred by the algorithm.} It is also the direction that the rule is often applied when \emph{searching} for a derivation of \cJ, by the same sort of recursive procedure. At least when talking to type theorists, it can be helpful to be familiar with this way of thinking.