From 64f76f92f75e5c575674b93ca43009097e4f283a Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Sun, 10 Mar 2024 20:59:35 +0100 Subject: [PATCH] minor --- agda/src/Monad/Instance/Setoids/K.lagda.md | 2 +- thesis/src/05_setoids.tex | 36 +++++++++++++++++----- 2 files changed, 30 insertions(+), 8 deletions(-) diff --git a/agda/src/Monad/Instance/Setoids/K.lagda.md b/agda/src/Monad/Instance/Setoids/K.lagda.md index 304a5b1..d2ee949 100644 --- a/agda/src/Monad/Instance/Setoids/K.lagda.md +++ b/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 } diff --git a/thesis/src/05_setoids.tex b/thesis/src/05_setoids.tex index 1bc73d7..b33ab24 100644 --- a/thesis/src/05_setoids.tex +++ b/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}