minor

thesis/main.tex

@@ -160,7 +160,27 @@
 % terminal coalgebra
 \newcommand*{\coalg}[1]{\ensuremath{\lbparen#1\rbparen}}
 
-\newcommand*{\noqed}{\def\qed{}}
+% Defines the `mycase` environment, copied from https://tex.stackexchange.com/questions/251053/how-to-use-case-1-case-2-in-a-proof-ieee-confs
+\newcounter{cases}
+\newcounter{subcases}[cases]
+\newenvironment{mycase}
+{
+    \setcounter{cases}{0}
+    \setcounter{subcases}{0}
+    \newcommand{\case}
+    {
+        \par\indent\stepcounter{cases}\textbf{Case \thecases.}
+    }
+    \newcommand{\subcase}
+    {
+        \par\indent\stepcounter{subcases}\textit{Subcase (\thesubcases):}
+    }
+}
+{
+    \par
+}
+\renewcommand*\thecases{\arabic{cases}}
+\renewcommand*\thesubcases{\roman{subcases}}
 
 \begin{document}
 \pagestyle{plain}

thesis/src/05_setoids.tex

@@ -222,14 +222,15 @@ Now we can relate two computations \textit{iff} they evaluate to the same result
 
   \begin{itemize}
     \item \textbf{Fixpoint}: We need to show that \(f^\sharp (x) \approx ([ id , f^\sharp ] \circ f)(x)\) for any \(x : X\). Let us proceed by case distinction:
+          \begin{mycase}
+            \case{} \(f(x) = i_1 (a)\)
+            \[ f^\sharp(x) \approx a \approx [ id , f^\sharp ] (i_1 (a)) \approx ([ id , f^\sharp ] \circ f) (x) \]
+            \case{} \(f(x) = i_2 (a)\)
+            \[ f^\sharp(x) \approx later (f^{\sharp'}(a)) \overset{(*)}{\approx} f^\sharp(a) \approx [ id , f^\sharp ] (i_2 (a)) \approx ([ id , f^\sharp ] \circ f) (x)\]
+            where \((*)\) follows from a general fact: any \(z : Delay'\;A\) satisfies \(force\;z \approx later\;z\).
+          \end{mycase}
 
-          \begin{itemize}
-            \item Case \(f(x) = i_1 (a)\):
-                  \[ f^\sharp(x) \approx a \approx [ id , f^\sharp ] (i_1 (a)) \approx ([ id , f^\sharp ] \circ f) (x) \]
-            \item Case \(f(x) = i_2 (a)\):
-                  \[ f^\sharp(x) \approx later (f^{\sharp'}(a)) \overset{(*)}{\approx} f^\sharp(a) \approx [ id , f^\sharp ] (i_2 (a)) \approx ([ id , f^\sharp ] \circ f) (x)\]
-          \end{itemize}
-          where \((*)\) follows from a general fact: any \(z : Delay'\;A\) satisfies \(force\;z \approx later\;z\).
+          \todo[inline]{Update folding with case and subcase}
     \item \textbf{Uniformity}: Let \((Y , =^Y) \in \obj{\setoids}\) and \(g : Y \rightarrow Delay\; A + Y, h : X \rightarrow Y\) be setoid morphisms, where \((id + h) \circ f = g \circ h\). We proceed by case distinction over \(f\;x\) and \(g (h\;x)\), note that by the requisite equation \((id + h) \circ f = g \circ h\), we only need to consider two cases:
           \begin{itemize}
             \item Case \(f\;x = i_1\;a\) and \(g (h\;x) = i_1\;b\):\\