Fix figure 8 (modulo small).HEADmaster

1 files changed, 24 insertions, 23 deletions

diff --git a/sec/compiler.ltx b/sec/compiler.ltx
index f1abca9..a9ab7f8 100644
--- a/sec/compiler.ltx
+++ b/sec/compiler.ltx
@@ -90,14 +90,26 @@ raw AST.\@
 \subsection{Bidirectional Type Checker}
 
 \begin{figure}
+  \small
   \[
-  \begin{array}{cccc}
+  \begin{array}{ccc}
     \begin{prooftree}
       \hypo{x : A \in \Gamma}
       \infer1{\judgement{\Gamma}{x}[\Rightarrow]{A}}
     \end{prooftree}
     &
     \begin{prooftree}
+      \hypo{\judgement{\Gamma}{t}[\Rightarrow]{A}}
+      \hypo{A = B}
+      \infer2{\judgement{\Gamma}{t}[\Leftarrow]{B}}
+    \end{prooftree}
+    &
+    \begin{prooftree}
+      \hypo{\judgement{\Gamma}{t}[\Leftarrow]{A}}
+      \infer1{\judgement{\Gamma}{t : A}[\Rightarrow]{A}}
+    \end{prooftree}
+    \\\\
+    \begin{prooftree}
       \hypo{\judgement{\Gamma, x : A}{t}[\Leftarrow]{B}}
       \infer1{\judgement{\Gamma}{\lambda x.t}[\Leftarrow]{A \to B}}
     \end{prooftree}
@@ -115,35 +127,24 @@ raw AST.\@
     \end{prooftree}
     \\\\
     \begin{prooftree}
-      \hypo{\rangeover{\judgement{\Gamma}{t_i}[\Leftrightarrow]{A_i}}{i}}
-      \infer1{\judgement{\Gamma}{\tuple{\rangeover{t_i}{i}}}[\Leftrightarrow]{\prod_i A_i}}
+      \hypo{\rangeover{\judgement{\Gamma}{t_\ell}[\Leftrightarrow]{A_\ell}}{\ell}}
+      \infer1{\judgement{\Gamma}{\tuple{\ell : \rangeover{t_\ell}{\ell}}}[\Leftrightarrow]{\prod_{\ell \in I} A_\ell}}
     \end{prooftree}
     &
     \begin{prooftree}
-      \hypo{\judgement{\Gamma}{t}[\Rightarrow]{\prod_i A_i}}
-      \infer1{\judgement{\Gamma}{t.i}[\Rightarrow]{A_i}}
+      \hypo{\judgement{\Gamma}{t}[\Leftarrow]{A_{\hat{\ell}}}}
+      \infer1{\judgement{\Gamma}{\hat{\ell}~t}[\Leftarrow]{\sum_{\ell \in I} A_\ell}}
     \end{prooftree}
     &
     \begin{prooftree}
-      \hypo{\judgement{\Gamma}{t}[\Leftarrow]{A_i}}
-      \infer1{\judgement{\Gamma}{\tuple{i, t}}[\Leftarrow]{\sum_i A_i}}
-    \end{prooftree}
-    &
-    \begin{prooftree}
-      \hypo{\judgement{\Gamma}{t}[\Rightarrow]{\sum_i A_i}}
-      \hypo{\rangeover{\judgement{\Gamma, x_i : A_i}{t_i}[\Leftarrow]{B}}{i}}
-      \infer2{\judgement{\Gamma}{\casetm{t}{\tuple{i,x_i}}{t_i}{i}}[\Leftarrow]{B}}
+      \hypo{\judgement{\Gamma}{t}[\Rightarrow]{\sum_{\ell \in I} A_\ell}}
+      \hypo{\rangeover{\judgement{\Gamma, x_\ell : A_\ell}{t_\ell}[\Leftarrow]{B}}{\ell}}
+      \infer2{\judgement{\Gamma}{\casetm{t}{\ell~x_\ell}{t_\ell}{\ell}}[\Leftarrow]{B}}
     \end{prooftree}
     \\\\
     \begin{prooftree}
-      \hypo{\judgement{\Gamma}{t}[\Rightarrow]{A}}
-      \hypo{A = B}
-      \infer2{\judgement{\Gamma}{t}[\Leftarrow]{B}}
-    \end{prooftree}
-    &
-    \begin{prooftree}
-      \hypo{\judgement{\Gamma}{t}[\Leftarrow]{A}}
-      \infer1{\judgement{\Gamma}{t : A}[\Rightarrow]{A}}
+      \hypo{\judgement{\Gamma}{t}[\Rightarrow]{\prod_{\ell \in I} A_\ell}}
+      \infer1{\judgement{\Gamma}{t.\hat{\ell}}[\Rightarrow]{A_{\hat{\ell}}}}
     \end{prooftree}
     &
     \begin{prooftree}
@@ -158,7 +159,7 @@ raw AST.\@
     \end{prooftree}
   \end{array}
   \]
-  \caption{Bidirectional typing rules for
+  \caption{\TODO{un-small}. Bidirectional typing rules for
     \lang{}.\@ We say \(t\) synthesises type \(A\) when
     \(\judgement{\Gamma}{t}[\Rightarrow]{A}\) and \(t\) checks at type \(A\) when
     \(\judgement{\Gamma}{t}[\Leftarrow]{A}\). We use \(\Leftrightarrow\) when a term can both
@@ -168,7 +169,7 @@ raw AST.\@
 
 \Cref{fig:bidir} shows how we have modified the \lang{} typing rules
 for bidirectional type checking. The changes are
-standard~\cref{bidir}. Products can both check and synthesise types.
+standard~\cite{bidir}. Products can both check and synthesise types.
 The \roll{} operator can only be checked as there is no unique correct
 guess for the shape type. The body of a \foldkw{} must be checked. The
 induction hypothesis is added to the context, so its type must be