minor

agda/src/Monad/Instance/Setoids/K.lagda.md

@@ -142,7 +142,7 @@ Now we show that `iter` defines an Elgot algebra structure on `Delay≈`
     ...                                       | inj₁ a = ≈-refl A
     ...                                       | inj₂ a = later≈ λ { .force≈ → helper a } 
       where
-      helper : ∀ (b : ∣ X ∣) → [ A ][ iter < f > b ≈ iter [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₁ b) ]
+      helper : ∀ (b : ∣ X ∣) → [ A ][ iter {A} {X} < f > b ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₁ b) ]
       helper b with f ⟨$⟩ b in eqb 
       ...               | inj₁ c = ≈-refl A
       ...               | inj₂ c = later≈ λ { .force≈ → helper c }

thesis/src/05_setoids.tex

@@ -190,7 +190,7 @@ Now we can relate two computations \textit{iff} they evaluate to the same result
 \end{theorem}
 \begin{proof}
   We need to show that for every setoid \((A, =^A)\) the resulting setoid \((Delay\;A, \approx)\) can be extended to a stable free Elgot algebra.
-  Stability follows automatically by theorem~\ref{thm:stability} and the fact that \(\setoids\) is Cartesian closed, so it suffices to define a free Elgot Algebra on \((Delay\;A, \approx)\).
+  Stability follows automatically by \autoref{thm:stability} and the fact that \(\setoids\) is Cartesian closed, so it suffices to define a free Elgot Algebra on \((Delay\;A, \approx)\).
 
   Let \((X , =^X) \in \obj{\setoids}\) and \(f : X \rightarrow Delay\; A + X\) be a setoid morphism, we define \(f^\sharp : X \rightarrow Delay\;A\) point wise:
   \[
@@ -218,19 +218,41 @@ Now we can relate two computations \textit{iff} they evaluate to the same result
   Now we check the iteration laws:
 
   \change[inline]{change the equivalence sign of coproducts}
+  \todo[inline]{Add types}
 
   \begin{itemize}
-    \item \textbf{Fixpoint}: We need to show that \(f^\sharp (x) \approx ([ id , f^\sharp ] \circ f)(x)\):
+    \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{itemize}
-            \item Case \(f(x) =^+ i_1 (a)\):
-                  \[ f^\sharp(x) \approx a \approx [ id , f^\sharp ] (i_1 (a)) = ([ id , f^\sharp ] \circ f) (x) \]
-            \item Case \(f(x) =^+ i_2 (a)\):
+            \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\).
-    \item \textbf{Uniformity}: Let \((Y , =^Y) \in \setoids\) and \(g : Y \rightarrow Delay\; A + Y, h : X \rightarrow Y\) be setoid morphisms with \((id + h) \circ f = g \circ h\).
-    \item \textbf{Folding}:
+    \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\):\\
+                  Consider that \((id + h) \circ f = g \circ h\) on \(x\) yields \(i_1 \; a = i_1 \; b\) and thus \(a \approx b\). Then indeed,
+                  \[f^\sharp\; x \approx a \approx b \approx g^\sharp (h\;x)\]
+            \item Case \(f\;x = i_2\;a\) and \(g (h\;x) = i_2\;b\):\\
+                  Note that now \((id + h) \circ f = g \circ h\) on \(x\) yields \(i_2(h\;a) = i_2\;b\) and thus \(h\;a = b\).
+                  We need to show that
+                  \[f^\sharp\;x = later(f^\sharp\;a) = later(g^\sharp(h\;a)) = later(g^\sharp\;b) = g^\sharp (h\;x),\]
+                  which indeed follows by coinduction.
+          \end{itemize}
+    \item \textbf{Folding}: Let \((Y , =^Y) \in \obj{\setoids}\) and \(h : Y \rightarrow X + Y\), we need to show that \({(f^\sharp + h)}^\sharp\;z = [ (id + i_1) \circ f , i_2 \circ h ]\;z\) for any \(z : X + Y\).
+          \begin{itemize}
+            \item Case \(z = i_1\;x\):\\
+                  We are left to show that \({(f^\sharp + h)}^\sharp(i_1 \; x) = (id + i_1) (f\;x)\). Let us proceed by case distinction on \(f\;x\):
+                  \begin{itemize}
+                    \item Case \(f\;x = i_1\;a\): We are done since \({(f^\sharp + h)}^\sharp(i_1 \; x) = i_1\;a = (id + i_1) (f\;x)\)
+                    \item Case \(f\;x = i_2\;a\): The goal reduces to
+                          \[{(f^\sharp + h)}^\sharp(i_1 \; x) = later(f^\sharp\;a) = later({[(id + i_1) \circ f] , i_2 \circ h}^\sharp (i_1\;a)) = \]
+                  \end{itemize}
+            \item Case \(z = i_2\;y\):\\
+
+          \end{itemize}
   \end{itemize}