typeset definitions of casts

paper/gtt.tex

@@ -1024,21 +1024,22 @@ TODO: do we actually know what would go wrong in that case?
 
     \bigskip
     
-    \framebox{Error Universal Properties}
-    
     \begin{mathpar}
+    \framebox{Error Universal Properties}
+    \qquad
     \inferrule{ \Gamma' \mid \cdot \vdash M' : \u B' }
               { \Gamma \ltdyn \Gamma' \mid \cdot \vdash \err \ltdyn M : \u B \ltdyn \u B'}
-    
+    \qquad
     \inferrule { \Gamma \mid x : \u B \vdash S : \u B'}
                {\Gamma \mid \cdot \vdash S[\err_{\u B}] \ltdyn \err_{\u{B'}} : \u B'}
     \end{mathpar}
 
     \bigskip
 
-    \framebox{Cast Success/Failure}
 
     \[
+    \framebox{Cast Success/Failure}
+    \quad
     \begin{array}{c}
       %% TODO prove these:
       %% x : A \vdash \dncast{\u F A}{\u F A'}{(\ret{(\upcast{A}{A'}{x})})} \ltdyn \ret{x} : \u F A \\
@@ -1400,31 +1401,64 @@ $\eta$-expansion \emph{up to cast at smaller type}.
 
 
 \begin{theorem}{Characterization of Casts}
-  \begin{enumerate}
-    
-  \item[+] $\upcast{A_1 + A_2}{A_1' + A_2'} \equidyn \ldots$
-  and $\dncast{\u F (A_1' + A_2')}{\u F (A_1 + A_2)} \equidyn \ldots$
+  \begin{small}
+\[
+  \begin{array}{l}
+  \upcast{A_1 + A_2}{A_1' + A_2'}{s} \equidyn \caseofXthenYelseZ{s}{x_1.\inl{(\upcast{A_1}{A_1'}{x_1})}}{x_2.\inr{(\upcast{A_2}{A_2'}{x_2})}}\\
+    \dncast{\u F (A_1' + A_2')}{\u F (A_1 + A_2)}{\bullet} \equidyn \\
+    \bindXtoYinZ{\bullet}{(s : (A_1' +
+      A_2'))}{}\\
+     \quad
+         {\caseofXthenYelseZ{s}
+           {x_1'.\bindXtoYinZ{(\dncast{\u F A_1}{\u F A_1'}{(\ret{x_1'})})}{x_1}{\ret{(\inl {x_1})}}}
+           {x_2'.\bindXtoYinZ{(\dncast{\u F A_2}{\u F A_2'}{(\ret{x_2'})})}{x_2}{\ret{(\inr {x_2})}}}}\\
+    \\
+    \upcast{A_1 \times A_2}{A_1' \times A_2'}{p} \equidyn \pmpairWtoXYinZ{p}{x_1}{x_2}{(\upcast{A_1}{A_1'}{x_1},\upcast{A_2}{A_2'}{x_2})} \\
+    \begin{array}{l}
+      \dncast{\u F (A_1' \times A_2')}{\u F (A_1 \times A_2)}{\bullet}
+      \equidyn \\
+      \qquad
+      \bindXtoYinZ{\bullet}{p'}{\pmpairWtoXYinZ{p'}{x_1'}{x_2'}{
+          \bindXtoYinZ{\dncast{\u F A_1}{\u F A_1'}{\ret x_1'}}{x_1}{
+            \bindXtoYinZ{\dncast{\u F A_2}{\u F A_2'}{\ret x_2'}}{x_2} {\ret (x_1,x_2) }}}}
+      \equidyn \\
+      \qquad
+      \bindXtoYinZ{\bullet}{p'}{\pmpairWtoXYinZ{p'}{x_1'}{x_2'}{
+          \bindXtoYinZ{\dncast{\u F A_2}{\u F A_2'}{\ret x_2'}}{x_2}{
+            \bindXtoYinZ{\dncast{\u F A_1}{\u F A_1'}{\ret x_1'}}{x_1} {\ret (x_1,x_2) }}}}
+    \end{array}\\
 
-  \item[$\times$] $\upcast{A_1 \times A_2}{A_1' \times A_2'} \equidyn \ldots$
-  and $\dncast{\u F (A_1' \times A_2')}{\u F (A_1 \times A_2)} \equidyn \ldots$
-  (both orders)
+    \\
+    \dncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}{\bullet} \equidyn
+    \pair{\dncast{\u B_1}{\u B_1'}{\pi \bullet}}{\dncast{\u B_2}{\u B_2'}{\pi' \bullet}}\\
+    \begin{array}{l}
+      \upcast{U (\u B_1 \with \u B_2)}{U (\u B_1' \with \u B_2')}{p} \equidyn\\
+      \thunk{\pair{\force{(\upcast{U \u B_1}{U \u B_1'}{(\thunk{\pi (\force{p})})})}}{\force{(\upcast{U \u B_2}{U \u B_2'}{(\thunk{\pi' (\force{p})})})}}}
+    \end{array}
+    \\
 
-  \item[$\with$] $\dncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'} \equidyn \ldots$
-  and $\upcast{U (\u B_1 \with \u B_2)}{U (\u B_1' \with \u B_2')} \equidyn \ldots$
-  
-  \item[$\to$] $\dncast{A \to \u B}{A' \to \u B'} \equidyn \ldots$
-  and $\upcast{U (A \to \u B)}{U (A' \to \u B')} \equidyn \ldots$
-  
-  \item[0]
-    $\upcast{0}{A}V \equidyn \absurd V$ and 
-    $\dncast{\u F 0}{\u F A} \equidyn \err$
-  \item[1]
-    $\dncast{1}{\u B} \equidyn \{\}$ and
-    $\upcast{U 1}{U \u B} \equidyn \thunk \err$
-  \item[$\top$] $\dncast{\u B}{\top} \equiv \ldots$ 
-    $\upcast{U \u B}{U \top} \equiv \ldots$
-  
-  \end{enumerate}
+    \\
+    \dncast{A \to \u B}{A' \to \u B'}{\bullet} \equidyn
+    \lambda{x}.{\dncast{B}{B'}{(\bullet \, (\upcast{A}{A'}{x}))}} \\
+    \begin{array}{l}
+      \upcast{U (A \to \u B)}{U (A' \to \u B')}{f} \equidyn\\
+      \thunk{(\lambda x'.\bindXtoYinZ{\dncast{\u F A}{\u F A'}{(\ret
+            x')}}{x}{ \force{(\upcast{U \u B}{U \u B'}{(\thunk{(\force{(f)}\,x)})})}})}
+    \end{array}
+        \\
+
+    \\
+    \upcast{0}{A}z \equidyn \absurd z\\
+    \dncast{\u F 0}{\u F A}{M} \equidyn \err\\
+
+    \\
+    \dncast{\top}{\u B}{\bullet} \equidyn \{\}\\
+    \upcast{U \top}{U \u B}{u} \equidyn \thunk \err
+  %% \item[$\top$] $\dncast{\u B}{\top} \equiv \ldots$ 
+  %%   $\upcast{U \u B}{U \top} \equiv \ldots$
+  \end{array}
+  \]
+  \end{small}
 \end{theorem}
 
 \subsection{Upcasts are Thunkable, Downcasts are Linear, a posteriori}