leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

setoids chapter somewhat finished

Browse source
This commit is contained in:
Leon Vatthauer 2024-03-13 07:30:02 +01:00
parent 2a6da1ea17
commit 723c4b0175
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
5 changed files with 82 additions and 60 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
thesis/.vscode/ltex.dictionary.en-US.txt vendored
View file

@ -67,3 +67,4 @@ Martin-Löf
Set₀
Set₁
bisimilar
copatterns

14
thesis/agda/Coind.agda
View file

@ -35,8 +35,12 @@ module coLists where
field force : coList A
open coList′
mutual
repeat : {A : Set} (a : A) → coList A
repeat′ : {A : Set} (a : A) → coList′ A
repeat {A} a = a ∷ repeat′ a
force (repeat′ {A} a) = repeat a
module repeatMutual where
mutual
repeat : {A : Set} (a : A) → coList A
repeat′ : {A : Set} (a : A) → coList′ A
repeat a = a ∷ repeat′ a
force (repeat′ a) = repeat a
repeat : {A : Set} (a : A) → coList A
repeat a = a ∷ λ { .force → repeat a }

4
thesis/main.tex
View file

@ -1,4 +1,4 @@
\documentclass[a4paper,11pt,numbers=noenddot, draft]{scrbook}
\documentclass[a4paper,11pt,numbers=noenddot]{scrbook}
\usepackage[top=2cm,lmargin=1in,rmargin=1in,bottom=3cm,hmarginratio=1:1]{geometry}
\usepackage[ngerman, main=british]{babel}
@ -6,7 +6,7 @@
\usepackage{minted}
\setminted[agda]{
linenos=true,
% breaklines=true,
breaklines=true,
encoding=utf8,
fontsize=\small,
frame=lines,

33
thesis/src/02_agda-categories.tex
View file

@ -1,9 +1,9 @@
\chapter{Category Theory in Agda}\label{chp:agda-cat}
\chapter{Implementing Category Theory in Agda}\label{chp:agda-cat}
There are many formalizations of category theory in proof assistants like Coq or Agda. The benefits of such a formalization are clear: having a usable formalization allows one to reason about categorical notions in a type checked environment that makes errors less likely.
Ideally such a development will bring researchers together and enable them to work in a unified setting that enables efficient communication of ideas and concepts.
In this thesis we will work with the dependently typed programming language Agda~\cite{agda} and the agda-categories~\cite{agda-categories} library that serves as an extensive foundation of categorical definitions.
This chapter shall serve as a quick introduction to the type theory of Agda, the agda-categories library, and the formalization of this thesis.
This chapter shall serve as a quick introduction to the relevant parts of Agda's type theory, the agda-categories library, and the formalization of this thesis.
\section{The Underlying Type Theory}\label{sec:typetheory}
Agda implements a Martin-Löf style dependent type theory with \emph{inductive} and \emph{coinductive types} as well as an infinite hierarchy of universes \(Set_0, Set_1, \ldots\), where usually \(Set_0\) is abbreviated as \(Set\).
@ -17,15 +17,13 @@ Dually to inductive types that are defined by their \emph{constructors}, coinduc
head : A
tail : Stream A
\end{minted}
i.e.\ the type of streams containing elements of type \(A\) is defined by its two destructors \(head : Stream\;A \rightarrow A\) and \(tail : Stream\;A \rightarrow Stream\;A\) that return the head and the tail of the stream respectively. Now, \emph{corecursion} is a principle for defining functions into coinductive types by specifying how the function will be observed. Take for example the following function which defines an infinite stream repeating the same argument:
i.e.\ the type of streams containing elements of type \(A\) is defined by its two destructors \(head : Stream\;A \rightarrow A\) and \(tail : Stream\;A \rightarrow Stream\;A\) that return the head and the tail of the stream respectively. Now, \emph{corecursion} is a principle for defining functions into coinductive types by specifying how results of the function may be observed. Take for example the following function which defines an infinite stream repeating the same argument and is defined by use of Agda's \emph{copatterns}.
\begin{minted}{agda}
repeat : {A : Set} (a : A) → Stream A
head (repeat a) = a
tail (repeat a) = repeat a
\end{minted}
Let us introduce a notion of bisimilarity for streams. Given two streams, they are bisimilar if their heads are equal and their tails are bisimilar.
Let us introduce the usual notion of stream bisimilarity. Given two streams, they are bisimilar if their heads are equal and their tails are bisimilar.
\begin{minted}{agda}
record _≈_ {A} (s : Stream A) (t : Stream A) : Set where
coinductive
@ -33,21 +31,21 @@ Let us introduce a notion of bisimilarity for streams. Given two streams, they a
head : head s ≡ head t
tail : tail s ≈ tail t
\end{minted}
In this definition \(≡\) is the built-in propositional equality in Agda with the single constructor \(refl\). We can now use coinduction as a proof principle to proof a fact about streams:
In this definition \(≡\) is the built-in propositional equality in Agda with the single constructor \(refl\). We can now use coinduction as a proof principle to proof a fact about streams.
\begin{minted}{agda}
repeat-eq : ∀ {A} (a : A) → repeat a ≈ tail (repeat a)
head (repeat-eq {A} a) = refl
tail (repeat-eq {A} a) = repeat-eq a
\end{minted}
Streams are always infinite and thus this representation of coinductive types as coinductive records is well suited for them. However, consider the type of possibly infinite lists, that we will call \(coList\). In pseudo notation this type can be defined as
Where in the coinductive step we were able to assume that \(repeat\;a \approx tail(repeat\;a)\) already holds and showed that thus \(tail(repeat\;a) \approx tail(tail(repeat\;a))\) holds.
Streams are always infinite and thus this representation of coinductive types as coinductive records is well suited for them. However, consider the type of \emph{possibly} infinite lists, that we will call \(coList\). In pseudo notation this type can be defined as
\begin{minted}{agda}
codata coList (A : Set) : Set where
nil : coList A
_∷_ : A → coList A → coList A
\end{minted}
That is, the coinductive type \(coList\) is defined by the constructors \(nil\) and \(∷\). Agda does offer a way for defining coinductive types by constructors, however this style is discouraged, since it breaks subject reduction~\cite{agda-man}\cite{coq-man}. Instead, we can define \(coList\) as two mutual types, one inductive and the other coinductive:
That is, the coinductive type \(coList\) is defined by the constructors \(nil\) and \(∷\). Agda does implement a second kind of coinductive types that allows exactly such definitions, however the use of these sometimes called \emph{positive coinductive types} is discouraged, since it is known to break subject reduction~\cite{agda-man}\cite{coq-man}. Instead, sticking to coinductive records, we can define \(coList\) as two mutual types, one inductive and the other coinductive:
\begin{minted}{agda}
mutual
data coList (A : Set) : Set where
@ -57,17 +55,20 @@ That is, the coinductive type \(coList\) is defined by the constructors \(nil\)
coinductive
field force : coList A
\end{minted}
Unfortunately, this does add the overhead of having to define functions on \(coList\) as mutual recursive functions, e.g.\ the \(repeat\) function from before can be defined as
\begin{minted}{agda}
mutual
repeat : {A : Set} (a : A) → coList A
repeat′ : {A : Set} (a : A) → coList′ A
repeat {A} a = a ∷ repeat′ a
force (repeat′ {A} a) = repeat a
repeat a = a ∷ repeat′ a
force (repeat′ a) = repeat a
\end{minted}
In \autoref{chp:setoids} we will have to deal with such a coinductive type that is defined by constructors. To avoid the aforementioned overhead of mutual definitions, we will work in a type theory that does offer coinductive types with constructors and their respective corecursion and coinduction principles. The translation to Agda's coinductive types is straightforward, as illustrated by the previous example.
or more succinctly using an anonymous \(\lambda\)-function
\begin{minted}{agda}
repeat : {A : Set} (a : A) → coList A
repeat a = a ∷ λ { .force → repeat a }
\end{minted}
In \autoref{chp:setoids} we will have to deal with such a coinductive type that is defined by constructors. To avoid the overhead of defining every data type twice and using mutual function definitions in the thesis, we will work in a type theory that does offer coinductive types with constructors and their respective corecursion and coinduction principles. However, in the formalization we stick to using coinductive records as to implement best practices. The translation between the two styles is straightforward, as illustrated by the previous example.
\section{Setoid Enriched Categories}
Let us now consider how to implement category theory in Agda. The usual textbook definition of a category glosses over some design decisions that have to be made when implementing it in type theory. One would usually see something like this:

90
thesis/src/05_setoids.tex
View file

@ -1,6 +1,6 @@
\chapter{A Case Study on Setoids}\label{chp:setoids}
In \autoref{chp:partiality} we have argued that the delay monad is not an equational lifting monad, because it does not only model partiality, but it also respects computation time. One way to remedy this is to take the quotient of the delay monad where computations with the same result are identified. In this chapter we will use the quotients-as-setoid approach, i.e.\ we will work in the category of setoids and show that the quotiented delay monad is the initial pre-Elgot monad in this category.
In \autoref{chp:partiality} we have argued that the delay monad is not an equational lifting monad, because it does not only model partiality, but it also respects computation time. One way to remedy this is to take the quotient of the delay monad where computations with the same result are identified. In this chapter we will use the quotients-as-setoid approach, i.e.\ we will work in the category of setoids and show that the quotiented delay monad is an instance of the previously defined monad \(\mathbf{K}\) in this category.
\section{Setoids in Type Theory}
We will now introduce the category that the rest of the chapter will take place in. Let us start with some basic definitions.
@ -9,24 +9,21 @@ We will now introduce the category that the rest of the chapter will take place
A setoid is a tuple \((A, \overset{A}{=})\) where \(A\) (usually called the \textit{carrier}) is a type and \(\overset{A}{=}\) is an equivalence relation on the inhabitants of \(A\).
\end{definition}
In the rest of this chapter we will not use the tuple notation for introducing setoids, instead we will just say `Let \(A\) be a setoid' and implicitly call the equivalence relation \(\overset{A}{=}\).
For brevity, we will not use the tuple notation most of the time, instead we will just say `Let \(A\) be a setoid' and implicitly call the equivalence relation \(\overset{A}{=}\).
\begin{definition}[Setoid Function]
A function on setoids \(A\) and \(B\) is a function \(f : A \rightarrow B\) between the carriers, such that \(f\) respects the equivalences, i.e.\ for any \(x,y : A\), \(x \overset{A}{=} y\) implies \(f\;x \overset{B}{=} f\;y\). We will denote setoid functions as \(A \leadsto B\).
\end{definition}
The function space setoid is of special interest, since it defines equality between functions.
Let us now consider the function space setoid, which is of special interest, since it defines a notion of equality between functions.
\begin{definition}[Function Space Setoid]
Given two setoids \(A\) and \(B\). The function space setoid on these setoids is defined as \((A \leadsto B, \doteq)\) or just \(A \leadsto B\), where \(\doteq\) is point wise equality on setoid functions.
\end{definition}
Setoids together with setoid functions form a category that we will call \(\setoids\). Properties of \(\setoids\) have already been examined in~\cite{setoids}, however we will reiterate some of these properties now to introduce notation that will be used for the rest of the chapter.
\begin{lemma}
\begin{proposition}
\(\setoids\) is a distributive category.
\end{lemma}
\end{proposition}
\begin{proof}
To show that \(\setoids\) is (co)Cartesian we will give the respective data types and unique functions. % chktex 36
For brevity, we will omit the proofs that the functions respect the corresponding equivalences, these are however included in the Agda standard library~\cite{agda-stdlib}.
@ -90,12 +87,12 @@ Setoids together with setoid functions form a category that we will call \(\seto
distributeˡ (x , i₁ y) = i₁ (x , y)
distributeˡ (x , i₂ y) = i₂ (x , y)
\end{minted}
Note that these functions are inverse by definition, and it is easy to show that they are setoid functions.
Note that these functions are inverse by definition, and it follows quickly that they are setoid functions.
\end{proof}
\begin{lemma}
\begin{proposition}\label{prop:setoids-ccc}
\(\setoids\) is Cartesian closed.
\end{lemma}
\end{proposition}
\begin{proof}
Let \(A\) and \(B\) be two setoids. The function space setoid \(A \leadsto B\) is an exponential object of \(A\) and \(B\), together with the functions \(curry\) and \(eval\) defined in the following listing.
\begin{minted}{agda}
@ -122,9 +119,9 @@ Now, recall from previous chapters that Capretta's delay monad~\cite{delay} is a
\mprset{fraction={===}}\inferrule*{x : A}{now\; x : D\;A} \qquad
\inferrule*{x : D\;A}{later \;x : D\;A} \qquad
\]
Furthermore, let us now recall two notions of equality between inhabitants of the delay type that have been introduced in~\cite{delay}. Afterwards, we will state some facts that have been proven in~\cite{quotienting} to then finally prove that the quotiented delay type extends to an instance of the monad \(\mathbf{K}\) that has been introduced in \autoref{chp:iteration}.
Furthermore, let us recall two different notions of bisimilarity between inhabitants of the delay type that have been studied previously in~\cite{quotienting}. Afterwards, we will reiterate some facts that have been proven in~\cite{quotienting} to then finally prove that the quotiented delay type extends to an instance of the monad \(\mathbf{K}\) that has been introduced in \autoref{chp:iteration}.
Let \(A\) be a setoid. Lifting the equivalence \(\overset{A}{=}\) to \(D\;A\) yields another equivalence called \emph{strong bisimilarity}. This equivalence is defined by the following rules.
Let \(A\) be a setoid. Lifting the equivalence \(\overset{A}{=}\) to \(D\;A\) yields another equivalence called \emph{strong bisimilarity}. This equivalence is defined by the rules
\[
\mprset{fraction={===}}\inferrule*{x \overset{A}{=} y}{x \sim y} \qquad
@ -159,7 +156,13 @@ Now, we call two computations \(p\) and \(q\) \emph{weakly bisimilar} or \(p \ap
later(\mu\;z) & \text{if } x = later\;z
\end{cases}\]
It has been shown in~\cite{delay} that this indeed a monad.
Given a function \(f : A \rightarrow B\), the lifted function \(Df : D\;A \rightarrow D\;B\) is defined as
\[Df\;x = \begin{cases}
now(f\;z) & \text{if } x = now\;z \\
later(Df\;z) & \text{if } x = later\;z
\end{cases}\]
It has been shown in~\cite{delay} that this indeed extends to a monad.
\end{proof}
For the rest of this chapter we will abbreviate \(\tilde{D}\;A = (D_A , \sim)\) and \(\dbtilde{D}\;A = (D_A, \approx)\).
@ -211,7 +214,7 @@ For the rest of this chapter we will abbreviate \(\tilde{D}\;A = (D_A , \sim)\)
\case{} \(f\;c = i_2\;a\)
\[f^\sharp\;c \approx later(f^\sharp\;a) \approx later({[(id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;a)) \approx {[(id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;c)\]
\end{mycase}
Thus, we are done. Let us now proceed with the proof of \ref{law:folding}, by case distinction on \(z\): % chktex 2
We will now proceed with the proof of \ref{law:folding}, by case distinction on \(z\): % chktex 2
\begin{mycase}
\case{} \(z = i_1\;x\)\\
Another case distinction on \(f\;x\) yields:
@ -251,17 +254,16 @@ For the rest of this chapter we will abbreviate \(\tilde{D}\;A = (D_A , \sim)\)
In the next proof a notion of \emph{discretized} setoid is needed, i.e.\ given a setoid \(Z\), we can discretize \(Z\) by replacing the equivalence relation with propositional equality, yielding \(\disc{Z} := (Z, \equiv)\). Now, the following corollary describes how to transform an iteration on \(\dbtilde{D}\;A\) into an iteration on \(\tilde{D}\;A\).
\begin{corollary}\label{cor:discretize}
Given a setoid function \(g : X \rightarrow \dbtilde{D}\;A + X\). There exists a setoid function \(\bar{g} : \disc{X} \rightarrow \tilde{D}\;A + \disc{X}\) such that \(g^\sharp\;x \sim \bar{g}^\sharp\;x\) for any \(x : X\).
Given a setoid function \(g : X \leadsto \dbtilde{D}\;A + X\). There exists a setoid function \(\bar{g} : \disc{X} \leadsto \tilde{D}\;A + \disc{X}\) such that \(g^\sharp\;x \sim \bar{g}^{\tilde{\sharp}}\;x\) for any \(x : X\).
\end{corollary}
\begin{proof}
It is clear that propositional equality implies strong bisimilarity and thus \(\bar{g}\) is a setoid function that behaves as \(g\) does but with a different type profile.
The requisite property follows by case distinction on \(g\;x\).
\begin{mycase}
\case{} \(g\;x = i_1\;a\)\\
We are done, since \(g^\sharp\;x \sim a \sim \bar{g}^\sharp\;x\)
We are done, since \(g^\sharp\;x \sim a \sim \bar{g}^{\tilde{\sharp}}\;x\)
\case{} \(g\;x = i_2\;a\)\\
By coinduction \(g^\sharp\;x \sim later(g^\sharp\;a) \sim later(\bar{g}^\sharp\;a) \sim \bar{g}^\sharp\;x\), which concludes the proof.
By coinduction \(g^\sharp\;x \sim later(g^\sharp\;a) \sim later(\bar{g}^{\tilde{\sharp}}\;a) \sim \bar{g}^{\tilde{\sharp}}\;x\), which concludes the proof.
\qedhere
\end{mycase}
\end{proof}
@ -278,19 +280,17 @@ In the next proof a notion of \emph{discretized} setoid is needed, i.e.\ given a
i_2\;a & \text{if } x = later\;a
\end{cases}\]
\(g\) trivially respects strong bisimilarity, thus consider \(g^{\sharp_b} : \tilde{D}\;A \leadsto B\). We need to show that \(g^{\sharp_b}\) also respects weak bisimilarity, thus yielding the requisite function \(\free{f} = g^{\sharp_b} : \dbtilde{D}\;A \leadsto B\). However, the proof turns out to be rather complex, let us postpone it to~\autoref{cor:respects}
\(g\) trivially respects strong bisimilarity, thus consider \(g^{\sharp_b} : \tilde{D}\;A \leadsto B\). We need to show that \(g^{\sharp_b}\) also respects weak bisimilarity, thus yielding the requisite function \(\free{f} = g^{\sharp_b} : \dbtilde{D}\;A \leadsto B\). However, the proof turns out to be rather complex, let us postpone it to~\autoref{cor:respects}.
Let us now show that \(g^{\sharp_b}\) is iteration preserving. Given a setoid function \(h : X \leadsto \dbtilde{D}\;A + X\), we need to show that \(g^{\sharp_b} (h^\sharp\;x) \overset{B}{=} {((g^{\sharp_b} + id) \circ h)}^{\sharp_b}\;x\) for any \(x : X\).
Using \autoref{cor:discretize} we will proceed to show
Instead, we will continue with the proof. Let us now show that \(g^{\sharp_b}\) is iteration preserving. Given a setoid function \(h : X \leadsto \dbtilde{D}\;A + X\), we need to show that \(g^{\sharp_b} (h^\sharp\;x) \overset{B}{=} {((g^{\sharp_b} + id) \circ h)}^{\sharp_b}\;x\) for any \(x : X\). Using \autoref{cor:discretize} we will proceed to show
\[g^{\sharp_b} (h^\sharp\;x) \overset{B}{=} {((g^{\sharp_b} + id) \circ \bar{h})}^{\sharp_b}\;x \overset{B}{=} {((g^{\sharp_b} + id) \circ h)}^{\sharp_b}\;x.\]
The second step instantly follows by \ref{law:uniformity}, considering that the identity function easily extends to a setoid function \(id : \disc{X} \leadsto X\), and thus \({((g^{\sharp_b} + id) \circ \bar{h})}^{\sharp_b}\;x \overset{B}{=} {((g^{\sharp_b} + id) \circ h)}^{\sharp_b}(id\;x)\). % chktex 2
The second step instantly follows by \ref{law:uniformity}, considering that the identity function easily extends to a setoid function \(id : \disc{X} \leadsto X\), and thus the second step can be reduced to \({((g^{\sharp_b} + id) \circ \bar{h})}^{\sharp_b}\;x \overset{B}{=} {((g^{\sharp_b} + id) \circ h)}^{\sharp_b}(id\;x)\). % chktex 2
For the first step consider
\begin{alignat*}{1}
& g^{\sharp_b} (h^\sharp\;x)
\\\overset{B}{=}\;&g^{\sharp_b} (\bar{h}^\sharp\;x)\tag{\autoref{cor:discretize}}
\\\overset{B}{=}\;&(g^{\sharp_b} \circ [ id , \bar{h}^\sharp])(i_2\;x)
\\\overset{B}{=}\;&g^{\sharp_b} (\bar{h}^{\tilde{\sharp}}\;x)\tag{\autoref{cor:discretize}}
\\\overset{B}{=}\;&(g^{\sharp_b} \circ [ id , \bar{h}^{\tilde{\sharp}}])(i_2\;x)
\\\overset{B}{=}\;&{([(id + i_1) \circ g , i_2 \circ i_2 ] \circ [i_1 , h])}^{\sharp_b} (i_2\;x)\tag{\ref{law:uniformity}}
\\\overset{B}{=}\;&{((g^{\sharp_b} + id) \circ h)}^{\sharp_b}\;x.\tag{\ref{law:compositionality}}
\end{alignat*}
@ -341,7 +341,7 @@ In the next proof a notion of \emph{discretized} setoid is needed, i.e.\ given a
It has thus been proven that every \(\dbtilde{D}\;A\) admits a free Elgot algebra structure.
\end{proof}
Let us now establish some functions for inspecting and manipulating the computation of elements of \(D\;A\). These functions and some key facts will then be used to finish the remaining proof of \autoref{thm:Dfreeelgot}.
Let us now establish some functions for inspecting and manipulating the computation of elements of \(D\;A\). These functions and some key facts will then be used to finish the remaining proof needed for \autoref{thm:Dfreeelgot}.
First, consider the ordering with respect to execution time on elements of \(D\;A\), defined by
\[
@ -362,8 +362,8 @@ The following Corollary, whose proof can be found in the formalization, will be
\begin{corollary}\label{cor:race}
\(race\) satisfies the following properties:
\begin{alignat*}{3}
& x \approx y & & \text{ implies } race\;x\;y \sim race\;y\;x & \text{ for any } x, y : D\;a
\\ &x \approx y && \text{ implies } race\;x\;y \lesssim y &\text{ for any } x, y : D\;A.
& x \approx y & & \text{ implies } race\;x\;y \sim race\;y\;x & \text{for any } x, y : D\;A
\\ &x \approx y && \text{ implies } race\;x\;y \lesssim y & \text{ for any } x, y : D\;A.
\end{alignat*}
\end{corollary}
@ -379,13 +379,14 @@ Similarly, consider \(\Delta : (x, y : D\;A) \rightarrow x \lesssim y \rightarro
later(\Delta\;a\;b\;q) & \text{if } x = later\;a, y = later\;b \text{ and } p = later_\lesssim q
\end{cases}\]
Lastly, consider the function \(\iota : A \times \mathbb{N} \rightarrow D\;A\), which adds a number of \(later\) in front of a value and is given by
Lastly, consider the function \(\iota : A \times \mathbb{N} \rightarrow D\;A\), which adds a number of \(later\) constructors in front of a value and is given by
\[\iota\;(a, n) := \begin{cases}
now\;x & \text{if } n = 0 \\
later(\iota\;(a, m)) & \text{if } n = m + 1
\end{cases}\]
Trivially, \(\iota\) can be extended to a setoid function \(\iota : A \times \mathbb{N} \leadsto \tilde{D}\;A\), where the equivalence on \(\mathbb{N}\) is propositional equality. Let us state two facts about \(\Delta\), the proof can again be found in the formalization.
Trivially, \(\iota\) can be extended to a setoid function \(\iota : A \times \mathbb{N} \leadsto \tilde{D}\;A\), where the equivalence on \(\mathbb{N}\) is propositional equality.
Let us state two facts about \(\Delta\), the proofs can again be found in the formalization.
\begin{corollary}\label{cor:delta}
\(\Delta\) satisfies the following properties:
\begin{alignat*}{4}
@ -423,7 +424,7 @@ Let us now return to the missing Corollary of \autoref{thm:Dfreeelgot}.
\\\overset{B}{=}\;&g^{\sharp_b}(\iota^*\;z). \tag{\ref{law:uniformity}}
\end{alignat*}
Now, we are left to find suitable \(g_1, g_2 : \tilde{D}(A \times \mathbb{N}) \leadsto B + \tilde{D} (A \times \mathbb{N})\). Consider,
Which leaves us to find suitable \(g_1, g_2 : \tilde{D}(A \times \mathbb{N}) \leadsto B + \tilde{D} (A \times \mathbb{N})\). Consider,
\[g_1\;p := \begin{cases}
i_1(f\;x) & \text{if } p = now\;(x, zero) \\
i_2(\tilde{D}o (\iota\;(x,n))) & \text{if } p = now\;(x, n + 1) \\
@ -431,12 +432,14 @@ Let us now return to the missing Corollary of \autoref{thm:Dfreeelgot}.
\end{cases}\]
and
\[g_2\;p := \begin{cases}
i_1(f\;x) & \text{if } p = now\;(x , n) \\
i_2\;(x , n) & \text{if } p = later\;(x, n)
i_1(f\;x) & \text{if } p = now\;(x , n) \\
i_2\;q & \text{if } p = later\;q
\end{cases}\]
where \(o : A \leadsto A \times \mathbb{N}\) is a setoid function that maps every \(z : A\) to \((z , 0) : A \times \mathbb{N}\). The applications of \ref{law:uniformity} are then justified by the definitions of \(g_1\) and \(g_2\) as well as the fact that \(\iota \circ o \doteq now\). % chktex 2
We are thus done after showing that \(g_1^{\sharp_b}\;z \overset{B}{=} g_2^{\sharp_b}\;z\). Consider another setoid function \[g_3 : \tilde{D}(A \times \mathbb{N}) \rightarrow B + \tilde{D}(A \times \mathbb{N}) + \tilde{D}(A \times \mathbb{N}),\]
We are thus done after showing that \(g_1^{\sharp_b}\;z \overset{B}{=} g_2^{\sharp_b}\;z\).
Consider another setoid function
\[g_3 : \tilde{D}(A \times \mathbb{N}) \leadsto B + \tilde{D}(A \times \mathbb{N}) + \tilde{D}(A \times \mathbb{N}),\]
defined by
\[g_3\;p := \begin{cases}
i_1(f\;x) & \text{if } p = now\;(x, 0) \\
@ -500,7 +503,20 @@ Let us now return to the missing Corollary of \autoref{thm:Dfreeelgot}.
\\\overset{B}{=}\;&([ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ] \circ (id + [ id , id]) \circ g_3) (later(\tilde{D}o(\iota\;(y,m))))\tag{\ref{law:fixpoint}}
\\\overset{B}{=}\;&([ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ] \circ (id + [ id , id])) (i_2(i_2(\tilde{D}o(\iota\;(y,m)))))
\\\overset{B}{=}\;&[ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ](\tilde{D}o(\iota\;(y,m)))
\\\overset{B}{=}\;&f\;y\tag*{\qedhere}
\\\overset{B}{=}\;&f\;y
\end{alignat*}
\case{} \(x = later\;p\)\\
The goal reduces to
\begin{alignat*}{1}
& [ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (g_3\;x)
\\\overset{+}{=}\;&[ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (i_2(i_2\;p))
\\\overset{+}{=}\;&i_2\;p
\\\overset{+}{=}\;&g_2\;x,
\end{alignat*}
which instantly follows by definition.
\end{mycase}
\end{proof}
This finishes the proof of the Corollary and thus \autoref{thm:Dfreeelgot} holds.
\end{proof}
We have shown in \autoref{thm:Dfreeelgot} that every \(\dbtilde{D}\;A\) extends to a free Elgot algebra. Together with \autoref{prop:setoids-ccc} and \autoref{thm:stability} this yields a description for the monad \(\mathbf{K}\) which has been defined in \autoref{chp:iteration}, in the category \(\setoids\).