From 2c00cf2406341532502794d604f55a7c58874e42 Mon Sep 17 00:00:00 2001 From: Matt Earnshaw Date: Thu, 19 Oct 2023 18:53:23 +0300 Subject: [PATCH] typos --- simple.tex | 6 +++--- unary.tex | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/simple.tex b/simple.tex index 4f18663..7e4a576 100644 --- a/simple.tex +++ b/simple.tex @@ -355,7 +355,7 @@ \subsection{Multiposets} We induct on the derivation of $\Delta,A,\Psi\types B$. If it is the identity rule, then $A=B$ and $\Delta$ and $\Psi$ are empty, so our given derivation of $\Gamma\types A$ is all we need. Otherwise, it comes from some relation $A_1,\dots,A_n \le B$ in \cG, where we have derivations of $\Gamma_i \types A_i$. - Since then $\Delta,A,\Psi = \Gamma_1,\dots,\Gamma_n$, there msut be an $i$ such that $\Gamma_i = \Gamma_i',A,\Gamma_i''$, while $\Delta = \Gamma_1,\dots,\Gamma_{i-1},\Gamma_i'$ and $\Psi = \Gamma_i'',\Gamma_{i+1},\dots,\Gamma_n$. + Since then $\Delta,A,\Psi = \Gamma_1,\dots,\Gamma_n$, there must be an $i$ such that $\Gamma_i = \Gamma_i',A,\Gamma_i''$, while $\Delta = \Gamma_1,\dots,\Gamma_{i-1},\Gamma_i'$ and $\Psi = \Gamma_i'',\Gamma_{i+1},\dots,\Gamma_n$. Now by the inductive hypothesis, we can construct a derivation of $\Gamma_i',\Gamma,\Gamma_i''\types A_i$. Applying the rule for $A_1,\dots,A_n \le B$ again, with this derivation in place of the original $\Gamma_i \types A_i$, gives the desired result. \end{proof} @@ -832,12 +832,12 @@ \subsection{Multicategories} But we encourage the interested reader to write down a multi--substitution too (\cref{ex:moncat-multisubadm}). \begin{thm}\label{thm:multicat-subadm} - Substitution is admissible in the cut-free type theory for multicategories under \cG: given derivations of $\Gamma\types M:A$ and of $\Delta,x:A,\Psi\types N:B$, we can construct a derivation of $\Delta,\Gamma,\Psi\types M[N/x]:B$. + Substitution is admissible in the cut-free type theory for multicategories under \cG: given derivations of $\Gamma\types M:A$ and of $\Delta,x:A,\Psi\types N:B$, we can construct a derivation of $\Delta,\Gamma,\Psi\types N[M/x]:B$. \end{thm} \begin{proof} This is essentially just \cref{thm:multiposet-cutadm}, with terms carried along. There is one thing to be said: since the variables used in any context must be distinct, including the given context $\Delta,x:A,\Psi$, it must be that the variables in $\Delta$ and $\Psi$ are pairwise distinct, and all of them are distinct from $x$. - But the variables in $\Delta,\Psi$ may not be pairwise distinct from those in $\Gamma$, so the context of the desired conclusion $\Delta,\Gamma,\Psi\types M[N/x]:B$ may involve an $\alpha$-equivalence. + But the variables in $\Delta,\Psi$ may not be pairwise distinct from those in $\Gamma$, so the context of the desired conclusion $\Delta,\Gamma,\Psi\types N[M/x]:B$ may involve an $\alpha$-equivalence. For instance, if we have $y:C\types f(y):A$ and $y:C,x:A,z:D\types g(y,x,z):B$, we cannot naively conclude $y:C,y:C,z:D\types g(y,f(y),z):B$; we have to rename one of the $y$'s first and get $y:C,w:C,z:D\types g(y,f(w),z):B$. We emphasize, however, that this is only a point about the term notation. The proof of \cref{thm:multiposet-cutadm}, which doesn't mention variables or terms at all, \emph{is already} an operation on derivations, and the renaming of variables only arises when we notate those derivations in a particular way. diff --git a/unary.tex b/unary.tex index 4f2dd19..3f720c7 100644 --- a/unary.tex +++ b/unary.tex @@ -107,7 +107,7 @@ \section{Posets} Formally speaking, what we have observed is the following \emph{initiality theorem}. \begin{thm}\label{thm:poset-initial-1} - For any relational graph \cG, the free poset $\F{\bPoset}\cG$ that it generates is has the same objects and its morphisms are the judgments that are derivable from \cG in free type theory of posets. + For any relational graph \cG, the free poset $\F{\bPoset}\cG$ that it generates has the same objects and its morphisms are the judgments that are derivable from \cG in free type theory of posets. \end{thm} \begin{proof} In the preceding discussion we assumed it as known that the free poset on a relational graph is its reflexive-transitive closure, which makes this theorem more or less obvious. @@ -479,7 +479,7 @@ \subsection{Cut admissibility} Note that cut-elimination is a fairly straightforward consequence of cut-admissibility: the latter allows us to eliminate each cut one by one. This will nearly always be true for our type theories, so we will usually just prove cut admissibility and rarely remark on the cut-elimination theorem that follows from it. -On the other hand, cut admissibility is a special case of cut-elimination, and sometimes people prove cut-elimination directly without explicitly using cut-elimination as a lemma. +On the other hand, cut admissibility is a special case of cut-elimination, and sometimes people prove cut-elimination directly without explicitly using cut-admissibility as a lemma. Under this approach, the inductive step in cut-admissibility is viewed instead as a step of ``pushing cuts upwards'' through a derivation: given a derivation as on the left below in the theory with cut, we transform it into the derivation on the right in which the cut is higher up. \begin{equation*} \inferrule*[right=cut]{\inferrule*{\sD_1\\\\\vdots}{A\types B} \\