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

work on setoids

Browse source
This commit is contained in:
Leon Vatthauer 2024-03-11 18:15:46 +01:00
parent 4e856d72f5
commit c631cf1bc3
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
11 changed files with 343 additions and 159 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -63,3 +63,7 @@ subobject
isomorphisms
epicness
fixpoint
Martin-Löf
Set₀
Set₁
bisimilar

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

@ -30,3 +30,4 @@
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qlaw:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: Note that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q since \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Qlaw:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: First, note that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q can equivalently be reformulated as \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q since \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Using \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, we are left to show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qlaw:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: First, note that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q can equivalently be reformulated as \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q since \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Using \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, we are left to show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"IF_IS","sentence":"^\\QLet \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q be a setoid morphism, we define \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q point wise: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}

42
thesis/agda/Coind.agda Normal file
View file

@ -0,0 +1,42 @@
{-# OPTIONS --guardedness #-}
open import Agda.Builtin.Equality
module Coind where
module Streams where
record Stream (A : Set) : Set where
coinductive
field
head : A
tail : Stream A
open Stream
repeat : {A : Set} (a : A) → Stream A
head (repeat a) = a
tail (repeat a) = repeat a
record _≈_ {A} (s : Stream A) (t : Stream A) : Set where
coinductive
field
head : head s ≡ head t
tail : tail s ≈ tail t
open _≈_
repeat-eq : ∀ {A} (a : A) → repeat a ≈ tail (repeat a)
head (repeat-eq {A} a) = refl
tail (repeat-eq {A} a) = repeat-eq a
module coLists where
mutual
data coList (A : Set) : Set where
nil : coList A
_∷_ : A → coList′ A → coList A
record coList′ (A : Set) : Set where
coinductive
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

2
thesis/agda/setoids.agda → thesis/agda/Setoids.agda
View file

@ -1,4 +1,4 @@
module Foo where
module Setoids where
open import Level
record _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where

3
thesis/agda/agda.agda-lib Normal file
View file

@ -0,0 +1,3 @@
name: agda
include: .
depend: standard-library

60
thesis/bib.bib
View file

@ -1,8 +1,35 @@
@inproceedings{agda,
title = {Towards a practical programming language based on dependent type theory},
author = {Ulf Norell},
year = {2007},
url = {https://api.semanticscholar.org/CorpusID:118357515}
% @inproceedings{agda,
% title = {Towards a practical programming language based on dependent type theory},
% author = {Ulf Norell},
% year = {2007},
% url = {https://api.semanticscholar.org/CorpusID:118357515}
% }
@software{agda,
author = {{Agda Developers}},
title = {{Agda}},
url = {https://agda.readthedocs.io/},
version = {2.6.5}
}
@manual{agda-man,
title = {Agda User Manual},
author = {The Agda Team},
year = {2024},
month = {03},
day = {06},
version = {2.6.4.3},
url = {https://agda.readthedocs.io/en/v2.6.4.3/}
}
@manual{coq-man,
title = {The Coq Reference Manual},
author = {The Coq Development Team},
year = {2024},
month = {03},
day = {01},
version = {8.19.1},
url = {https://coq.inria.fr/doc/V8.19.0/refman/}
}
@inproceedings{agda-categories,
@ -268,10 +295,21 @@
}
@article{manes,
title={Algebraic Theories in a Category},
author={Manes, Ernest G},
journal={Algebraic Theories},
pages={161--279},
year={1976},
publisher={Springer}
title = {Algebraic Theories in a Category},
author = {Manes, Ernest G},
journal = {Algebraic Theories},
pages = {161--279},
year = {1976},
publisher = {Springer}
}
@article{kozencoinduction,
title = {Practical coinduction},
author = {Kozen, Dexter and Silva, Alexandra},
journal = {Mathematical Structures in Computer Science},
volume = {27},
number = {7},
pages = {1132--1152},
year = {2017},
publisher = {Cambridge University Press}
}

15
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,
@ -160,6 +160,9 @@
% terminal coalgebra
\newcommand*{\coalg}[1]{\ensuremath{\lbparen#1\rbparen}}
% discretized setoids
\newcommand*{\disc}[1]{\ensuremath{\vert #1 \vert}}
% 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]
@ -197,6 +200,10 @@
\chapter*{Licensing}
\doclicenseThis{}
\chapter*{Abstract}
\todo[inline]{abstract}
\tableofcontents
\listoftodos\
@ -238,6 +245,6 @@
\printbibliography[heading=bibintoc]{}
% https://tex.stackexchange.com/questions/74857/toc-like-list-of-definitions-using-theorem-environments
\renewcommand*{\listtheoremname}{List of Definitions}
\listoftheorems[ignoreall,show={definition}]
% \renewcommand*{\listtheoremname}{List of Definitions}
% \listoftheorems[ignoreall,show={definition}]
\end{document}

78
thesis/src/01_preliminaries.tex
View file

@ -201,7 +201,7 @@ A Cartesian closed category is a Cartesian category \(\C \) that also has an exp
The internal logic of Cartesian closed categories is the simply typed \(\lambda \)-calculus, which makes them a suitable target for interpreting programming languages. For the rest of this thesis we will work in an ambient distributive category that however does not have to be Cartesian closed as to be more general.
\section{F-Coalgebras}
Let \(F : \C \rightarrow \C \) be an endofunctor. Recall that F-algebras are tuples \((X, \alpha : FX \rightarrow X)\) consisting of an object of \(\C \) and a morphism out of the functor. Initial F-algebras have been studied extensively as a means of modelling inductive data types together with induction and recursion principles~\cite{inductive}. For this thesis we will be more interested in the dual concept namely terminal coalgebras; let us formally introduce them now.
Let \(F : \C \rightarrow \C \) be an endofunctor. Recall that F-algebras are tuples \((X, \alpha : FX \rightarrow X)\) consisting of an object of \(\C \) and a morphism out of the functor. Initial F-algebras have been studied extensively as a means of modeling inductive data types together with induction and recursion principles~\cite{inductive}. For this thesis we will be more interested in the dual concept namely terminal coalgebras; let us formally introduce them now.
\begin{definition}[F-Coalgebra]
A tuple \((X \in \obj{\C}, \alpha : X \rightarrow FX)\) is called an F-coalgebra.
@ -242,7 +242,7 @@ Let \(F : \C \rightarrow \C \) be an endofunctor. Recall that F-algebras are tup
\end{alignat*}
\end{proof}
The terminal object of \(Coalg(F)\) is sometimes called \textit{final F-coalgebra} and can now similarly to initial F-algebras be used for modelling the semantics of coinductive data types where terminality of the coalgebra yields corecursion as a definitional principle and coinduction as a proof principle. Let us make the universal property of terminal F-coalgebras concrete:
The terminal object of \(Coalg(F)\) is sometimes called \textit{final F-coalgebra}, we will however call it the \textit{terminal F-coalgebra} for consistency with initial F-algebras. Similarly to initial F-algebras, the final F-coalgebra can be used for modeling the semantics of coinductive data types where terminality of the coalgebra yields corecursion as a definitional principle and coinduction as a proof principle. Let us make the universal property of terminal F-coalgebras concrete:
\begin{definition}[Terminal F-Coalgebra]
An F-coalgebra \((T, t : T \rightarrow FT)\) is called a terminal F-coalgebra if for any other F-coalgebra \((X, \alpha : X \rightarrow FX)\) there exists a unique morphism \(\coalg{\alpha} : X \rightarrow T\) satisfying:
@ -261,49 +261,51 @@ The terminal object of \(Coalg(F)\) is sometimes called \textit{final F-coalgebr
\]
\end{definition}
We will discuss the concrete form that induction and coinduction take in a type theory in \autoref{chp:agda-cat}. Let us now reiterate a famous Lemma concerning terminal F-coalgebras.
\begin{lemma}[Lambek's Lemma~\cite{lambek}]
Let \((T, t : T \rightarrow FT)\) be a terminal F-coalgebra. Then \(t\) is an isomorphism.
\end{lemma}
\begin{proof}
First note that \((FT, Ft : FT \rightarrow FFT)\) is also an F-coalgebra. This yields the unique morphism \(\coalg{Ft} : FT \rightarrow T\) satisfying:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJGVCJdLFsyLDAsIkZGVCJdLFswLDIsIlQiXSxbMiwyLCJGVCJdLFswLDEsIkZ0Il0sWzIsMywidCJdLFswLDIsIlxcbGxicmFja2V0IEZ0IFxccnJicmFja2V0IiwyLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzEsMywiRlxcbGxicmFja2V0IEZ0IFxccnJicmFja2V0Il1d
\[
\begin{tikzcd}[ampersand replacement=\&]
FT \&\& FFT \\
\\
T \&\& FT
\arrow["Ft", from=1-1, to=1-3]
\arrow["t", from=3-1, to=3-3]
\arrow["{\coalg{Ft}}"', dashed, from=1-1, to=3-1]
\arrow["{F\coalg{Ft}}", from=1-3, to=3-3]
\end{tikzcd}
\]
% \begin{proof}
% First note that \((FT, Ft : FT \rightarrow FFT)\) is also an F-coalgebra. This yields the unique morphism \(\coalg{Ft} : FT \rightarrow T\) satisfying:
% % https://q.uiver.app/#q=WzAsNCxbMCwwLCJGVCJdLFsyLDAsIkZGVCJdLFswLDIsIlQiXSxbMiwyLCJGVCJdLFswLDEsIkZ0Il0sWzIsMywidCJdLFswLDIsIlxcbGxicmFja2V0IEZ0IFxccnJicmFja2V0IiwyLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzEsMywiRlxcbGxicmFja2V0IEZ0IFxccnJicmFja2V0Il1d
% \[
% \begin{tikzcd}[ampersand replacement=\&]
% FT \&\& FFT \\
% \\
% T \&\& FT
% \arrow["Ft", from=1-1, to=1-3]
% \arrow["t", from=3-1, to=3-3]
% \arrow["{\coalg{Ft}}"', dashed, from=1-1, to=3-1]
% \arrow["{F\coalg{Ft}}", from=1-3, to=3-3]
% \end{tikzcd}
% \]
\(\coalg{Ft}\) is inverse to \(t\):
% \(\coalg{Ft}\) is inverse to \(t\):
\begin{enumerate}
\item \(\coalg{Ft} \circ t : (T, t) \rightarrow (T, t)\) is a morphism between F-coalgebras since
\begin{alignat*}{1}
& F(\coalg{Ft} \circ t) \circ t \\
=\; & F \coalg{Ft} \circ t \circ t \\
=\; & F \coalg{Ft} \circ Ft \circ t \\
=\; & t \circ \coalg{Ft} \circ t
\end{alignat*}
By uniqueness of the identity on \((T, t)\) we follow that \(\coalg{Ft} \circ t = id\).
% \begin{enumerate}
% \item \(\coalg{Ft} \circ t : (T, t) \rightarrow (T, t)\) is a morphism between F-coalgebras since
% \begin{alignat*}{1}
% & F(\coalg{Ft} \circ t) \circ t \\
% =\; & F \coalg{Ft} \circ t \circ t \\
% =\; & F \coalg{Ft} \circ Ft \circ t \\
% =\; & t \circ \coalg{Ft} \circ t
% \end{alignat*}
% By uniqueness of the identity on \((T, t)\) we follow that \(\coalg{Ft} \circ t = id\).
\item \(t \circ \coalg{Ft} = id : (FT, Ft) \rightarrow (FT, Ft)\) follows by:
\begin{alignat*}{1}
& t \circ \coalg{Ft} \\
=\; & F\coalg{Ft} \circ Ft \\
=\; & F(\coalg{Ft} \circ t) \\
=\; & F(id) \\
=\; & id
\end{alignat*}
\end{enumerate}
\end{proof}
% \item \(t \circ \coalg{Ft} = id : (FT, Ft) \rightarrow (FT, Ft)\) follows by:
% \begin{alignat*}{1}
% & t \circ \coalg{Ft} \\
% =\; & F\coalg{Ft} \circ Ft \\
% =\; & F(\coalg{Ft} \circ t) \\
% =\; & F(id) \\
% =\; & id
% \end{alignat*}
% \end{enumerate}
% \end{proof}
\section{Monads}
Monads are widely known among programmers as a way of modelling effects in pure languages and are also central to this thesis. Let us recall the basic definitions\cite{Lane1971}\cite{moggi}.
Monads are widely known among programmers as a way of modeling effects in pure languages and are also central to this thesis. Let us recall the basic definitions\cite{Lane1971}\cite{moggi}.
\begin{definition}[Monad]
A monad \(\mathbf{T}\) on a category \(\C \) is a triple \((T, \eta, \mu)\), where \(T : \C \rightarrow \C \) is an endofunctor and \(\eta : Id \rightarrow T, \mu : TT \rightarrow T\) are natural transformations, satisfying the following laws:
@ -409,7 +411,7 @@ The possibility of Kleisli composition enables us to define the category of prog
For the rest of this thesis we will use both equivalent notions interchangeably to make definitions easier.
\section{Strong and Commutative Monads}
When modelling partiality with a monad, one would expect the following two programs to be equivalent
When modeling partiality with a monad, one would expect the following two programs to be equivalent
\begin{multicols}{2}
\begin{minted}{haskell}
do x <- p

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

@ -1,12 +1,76 @@
\chapter{Category Theory in Agda}
\chapter{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 library and the formalization of this thesis.
This chapter shall serve as a quick introduction to the type theory of Agda, 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\).
Recall that inductive types usually come with a principle for defining functions from inductive types, called \emph{recursion} and a principle for proving facts about inductive types, called \emph{induction}.
These are standard notions and need no further introduction. Coinductive types come with dual principles that are however lesser known.
Dually to inductive types that are defined by their \emph{constructors}, coinductive types are defined by their \emph{destructors} or their observational behavior. Take the type of streams over a type \(A\), for example. In Agda one would define this type as a coinductive record like so:
\begin{minted}{agda}
record Stream (A : Set) : Set where
coinductive
field
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:
\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.
\begin{minted}{agda}
record _≈_ {A} (s : Stream A) (t : Stream A) : Set where
coinductive
field
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:
\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
\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:
\begin{minted}{agda}
mutual
data coList (A : Set) : Set where
nil : coList A
_∷_ : A → coList′ A → coList A
record coList′ (A : Set) : Set where
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
\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.
\section{Setoid Enriched Categories}
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:
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:
\begin{definition}[Category]
A category consists of
\begin{itemize}

6
thesis/src/03_partiality-monads.tex
View file

@ -1,7 +1,7 @@
\chapter{Partiality Monads}\label{chp:partiality}
Moggi's categorical semantics~\cite{moggi} describe a way to interpret an effectful programming language in a category. For this one needs a (strong) monad \(T\) capturing the desired effects, then we can take the elements of \(TA\) as denotations for programs of type \(A\). The Kleisli category of \(T\) can be viewed as the category of programs, which gives us a way of composing programs (Kleisli composition).
For this thesis we will restrict ourselves to monads for modelling partiality, the goal of this chapter is to capture what it means to be a partiality monad and look at two common examples.
For this thesis we will restrict ourselves to monads for modeling partiality, the goal of this chapter is to capture what it means to be a partiality monad and look at two common examples.
\section{Properties of Partiality Monads}
We will now look at how to express the following non-controversial properties of a minimal partiality monad categorically:
@ -148,7 +148,7 @@ The endofunctor \(MX = X + 1\) extends to a monad by taking \(\eta_X = i_1 : X \
\end{alignat*}
\end{proof}
In the setting of classical mathematics this monad is therefore sufficient for modelling partiality, but in general it will not be useful for modelling non-termination as a side effect, since one would need to know beforehand whether a program terminates or not. For the purpose of modelling possibly non-terminating computations another monad has been developed by Capretta~\cite{delay}.
In the setting of classical mathematics this monad is therefore sufficient for modeling partiality, but in general it will not be useful for modeling non-termination as a side effect, since one would need to know beforehand whether a program terminates or not. For the purpose of modeling possibly non-terminating computations another monad has been developed by Capretta~\cite{delay}.
\section{The Delay Monad}
\todo[inline]{Take introduction from setoids chapter and put it here!}
@ -576,6 +576,6 @@ Let us record some facts that we will use to prove commutativity of \(\mathbf{D}
\end{proof}
\improvement[inline]{Elaborate more?}
We have now seen that \(\mathbf{D}\) is strong and commutative, however it is not an equational lifting monad, since besides modelling non-termination, the delay monad also counts the execution time of a computation. This is a result of the too intensional notion of equality that this monad comes with.
We have now seen that \(\mathbf{D}\) is strong and commutative, however it is not an equational lifting monad, since besides modeling non-termination, the delay monad also counts the execution time of a computation. This is a result of the too intensional notion of equality that this monad comes with.
In \autoref{chp:setoids} we will see a way to remedy this: taking the quotient of the delay monad where execution time is ignored. This will then yield an equational lifting monad on the category of setoids. However, in a general setting it is generally believed to be impossible to define a monad structure on this quotient. Chapman et al.\ have identified the axiom of countable choice (which crucially holds in the category of setoids) as a sufficient requirement for defining a monad structure on the quotient of \(\mathbf{D}\).

221
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 the initial pre-Elgot monad in this category.
Let us introduce the category that we are working in:
@ -25,7 +25,10 @@ Setoids and setoid morphisms form a category that we call \(\setoids\).
\(\setoids\) is a distributive category.
\end{lemma}
\begin{proof}
To show that \(\setoids\) is (co-)Cartesian we will give the respective data types and unique morphisms, this also introduces notation we will use for the rest of the chapter. We will not include the proofs that the morphisms are setoid morphisms, these can be looked up in the Agda standard library.
To show that \(\setoids\) is (co)Cartesian we will give the respective data types and unique morphisms, this also introduces notation we will use for the rest of the chapter. We will not include the proofs that the morphisms are setoid morphisms, these can be looked up in the Agda standard library. % chktex 36
\todo[inline]{Cite agda-stdlib}
\todo[inline]{Introduce coproduct equality sign}
\begin{itemize}
\item \textbf{Products}:
@ -90,7 +93,7 @@ Setoids and setoid morphisms form a category that we call \(\setoids\).
\end{lemma}
\begin{proof}
We have already shown that \(\setoids\) is Cartesian, we need to show that given two setoids \((A, =^A), (B, =^B)\) we can construct an exponential object.
Indeed, take the function space setoid \((A \rightarrow B, \doteq)\) where \(\doteq\) is point wise equality of setoid morphisms i.e. \(f , g : A \rightarrow B\) are point wise equal \(f \doteq g\) \textit{iff} \(f x =^B g x\) for any \(x : A\). \(curry\) and \(eval\) are then defined as usual:
Indeed, take the function space setoid \((A \rightarrow B, \doteq)\) where \(\doteq\) is point wise equality of setoid morphisms i.e. \(f , g : A \rightarrow B\) are point wise equal \(f \doteq g\) \textit{iff} \(f x =^B g x\) for any \(x : A\). \(curry\) and \(eval\) are then defined as expected.
\begin{minted}{agda}
curry : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
→ (C × A → B) → C → A → B
@ -107,72 +110,54 @@ Setoids and setoid morphisms form a category that we call \(\setoids\).
% Historically proof assistants like Agda and Coq have been offering multiple ways of defining coinductive types, nowadays the manuals of both Agda and Coq advise users to use coinductive records instead of defining coinductive types by constructors, we will heed this advice.
% Since the delay monad is usually defined by the constructors \(now\) and \(later\)
Originally the delay monad has been introduced as a coinductive datatype with two constructors, in pseudo Agda like code this would look something like:
\begin{minted}{agda}
codata (A : Set) : Set where
now : A → Delay A
later : Delay A → Delay A
\end{minted}
This style is sometimes called \textit{positively coinductive} and is nowadays advised against in the manuals of both Agda and Coq\todo{cite}. Instead, one is advised to use coinductive records, we will heed this advice and use the following representation of the delay monad in Agda:\change{rephrase}
\todo[inline]{Cite https://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.html somehow}
\cite{nad-delay}
\begin{minted}{agda}
mutual
data Delay (A : Set) : Set where
now : A → Delay A
later : Delay′ A → Delay A
record Delay′ (A : Set) : Set where
coinductive
field force : Delay A
\end{minted}
Here \Verb{Delay} is defined as an inductive datatype where the coinductive part of the original definition (i.e. the coinductive occurrence of the delay type in the \Verb{later} constructor) references a coinductive record \Verb{Delay'} which consists of only one field that forces a coinductive value to an inductive one.
For the sake of readability we will introduce other concepts only by inference rules instead of Agda code, for the delay monad this looks like:
Recall from previous chapters that Capretta's delay monad~\cite{delay} is a coinductive type defined by the two constructors:
\[
\inferrule*{x : A}{now\; x : Delay \;A} \hskip 1cm
\inferrule*{x : Delay' \;A}{later \;x : Delay\; A} \hskip 1cm
\mprset{fraction={===}}\inferrule*{x : Delay' \;A}{force \;x : Delay \;A}
\mprset{fraction={===}}\inferrule*{x : A}{now\; x : Delay \;A} \qquad
\inferrule*{x : Delay \;A}{later \;x : Delay\; A} \qquad
\]
We will now introduce two notions of equality on inhabitants of the delay type, given a setoid \((A, =^A)\) we call the equivalence received by lifting \(=^A\) to \(Delay\;A\) \textit{strong bisimilarity}, the definition is as follows:
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 \(\mathbf{K}\).
Given a setoid \((A , \overset{A}{=})\), the equivalence relation that is received by lifting \(\overset{A}{=}\) to \(Delay\;A\) is called \emph{strong bisimilarity}, it is defined by the rules
\[
\inferrule*{eq : x =^A y}{now \;eq : x \sim y} \hskip 1cm
\inferrule*{eq : force \;x \sim' force\; y}{later\;eq : later\; x \sim later\; y} \hskip 1cm
\mprset{fraction={===}}\inferrule*{eq : x \sim' y}{force\; eq : x \sim y}
\mprset{fraction={===}}\inferrule*{eq : x =^A y}{now \;eq : x \sim y} \qquad
\inferrule*{eq : force \;x \sim force\; y}{later\;eq : later\; x \sim later\; y} \qquad
\]
\begin{lemma}
\begin{proposition}[\cite{quotienting}]
\((Delay\;A, \sim)\) is a setoid.
\end{lemma}
\end{proposition}
In \((Delay\;A, \sim)\) computations that evaluate to the same result but in a different amount of time are not equal. We will now build the quotient of this type by weak bisimilarity, i.e. we will identify all computations that terminate with the same result. Let us first consider what it means for a computation to evaluate to some result:
\begin{proposition}[\cite{quotienting}]
\((Delay\;A, \sim)\) is a setoid.
\end{proposition}
In \((Delay\;A, \sim)\) computations that evaluate to the same result are not identified if their computation times differ. In many contexts this behavior is too intensional. Instead, we will now consider the quotient of this setoid, where all computations that evaluate to the same result are identified. Let us first define a relation that states that two computations evaluate to the same result
% In \((Delay\;A, \sim)\) computations that evaluate to the same result but in a different amount of time are not equal. We will now build the quotient of this type by weak bisimilarity, i.e. we will identify all computations that terminate with the same result. Let us first consider what it means for a computation to evaluate to some result:
\[
\inferrule*{eq : x =^A y}{now\; eq : now\;x \downarrow y} \hskip 1cm
\inferrule*{eq : x =^A y}{now\; eq : now\;x \downarrow y} \qquad
\inferrule*{d : force\;x \downarrow c}{later\;d : later\;x \downarrow c }
\]
Now we can relate two computations \textit{iff} they evaluate to the same result:
Now, we call two computations \(p\) and \(q\) \emph{weakly bisimilar} or \(p \approx q\) if they evaluate to the same result, or don't evaluate at all, which is specified by these rules
\[
\inferrule*{eq : a =^A b \\ xa : x \downarrow a \\ yb : y \downarrow b}{\downarrow\approx \; eq \; xa \; yb : x \approx y} \hskip 1cm
\inferrule*{eq : force \;x \approx' force \;y}{later\;eq : later \;x \approx later \;y} \hskip 1cm
\mprset{fraction={===}}\inferrule*{eq : x \approx' y}{force\;eq : x \approx y}
\mprset{fraction={===}}\inferrule*{eq : a =^A b \\ xa : x \downarrow a \\ yb : y \downarrow b}{\downarrow\approx \; eq \; xa \; yb : x \approx y} \qquad
\inferrule*{eq : force \;x \approx force \;y}{later\;eq : later \;x \approx later \;y} \qquad
\]
\begin{lemma}
\begin{proposition}[\cite{delay}]
\((Delay\;A, \approx)\) is a setoid.
\end{lemma}
\end{proposition}
\begin{theorem}
\begin{proposition}[\cite{delay}]
\((Delay\;A, \approx)\) is a monad.
\end{theorem}
\end{proposition}
\begin{proof}
The monad unit is the constructor \Verb{now} and monad multiplication can be defined as follows:
The monad unit is the constructor \texttt{now} and the multiplication can be defined as follows:
\begin{minted}{agda}
μ : Delay (Delay X) → Delay X
@ -186,76 +171,114 @@ Now we can relate two computations \textit{iff} they evaluate to the same result
\end{proof}
\begin{theorem}
\((Delay\;A , \approx)\) is an instance of \(\mathbf{K}\) in the category \(\setoids\).
Every \((Delay\;A , \approx)\) can be equipped with a free Elgot algebra structure.
\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 \autoref{thm:stability} and the fact that \(\setoids\) is Cartesian closed, so it suffices to define a free Elgot Algebra on \((Delay\;A, \approx)\).
We need to show that for every setoid \((A, =^A)\) the resulting setoid \((Delay\;A, \approx)\) can be extended to a free Elgot algebra.
% 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:
Let \((X , \overset{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:
\[
f^\sharp (x) :=
\begin{cases}
a & \text{if } f\;x = i_1 (a) \\
later\;(f^{\sharp'} a) & \text{if } f\;x = i_2 (a)
a & \text{if } f\;x = i_1 (a) \\
later\;(f^{\sharp} a) & \text{if } f\;x = i_2 (a)
\end{cases}
\]
where \(f^{\sharp'} : X \rightarrow Delay'\;A\) is defined corecursively by:
\[
force (f^{\sharp'}(x)) = f^\sharp(x)
\]
Let us first show that \(f^\sharp\) is a setoid morphism, i.e. given \(x, y : X\) with \(x =^X y\), we need to show that \(f^\sharp(x) = f^\sharp(y)\). Since \(f\) is a setoid morphism we know that \(f(x) =^+ f(y)\) in the coproduct setoid \((Delay\;A + X, =^+)\). We proceed by case distinction on \(f(x)\):
Let us first show that \(f^\sharp\) is a setoid morphism, i.e.\ given \(x, y : X\) with \(x \overset{X}{=} y\), we need to show that \(f^\sharp(x) = f^\sharp(y)\). Since \(f\) is a setoid morphism we know that \(f(x) \overset{+}{=} f(y)\) in the coproduct setoid \((Delay\;A + X, \overset{+}{=})\). We proceed by case distinction on \(f(x)\):
\begin{mycase}
\case{} \(f(x) = i_1 (a)\)
\[f^\sharp (x) = a = f^\sharp(y)\]
\case{} \(f(x) = i_2 (a)\)
\[f^\sharp (x) = later (f^{\sharp}(a)) = f^\sharp (y)\]
\end{mycase}
Next, we check the iteration laws:
\begin{itemize}
\item Case \(f(x) = i_1 (a)\):
\[f^\sharp (x) = a = f^\sharp(y)\]
\item Case \(f(x) = i_2 (a)\):
\[f^\sharp (x) = later (f^{\sharp'}(a)) = f^\sharp (y)\]
\end{itemize}
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)\) for any \(x : X\). Let us proceed by case distinction:
\item \ref{law: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\).
\[ f^\sharp(x) \approx later (f^{\sharp}(a)) \approx f^\sharp(a) \approx [ id , f^\sharp ] (i_2 (a)) \approx ([ id , f^\sharp ] \circ f) (x)\]
\end{mycase}
\item \ref{law: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 need to show that \(f^\sharp\;x = g^\sharp(h\;x)\), for any \(x : X\). Let us 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{mycase}
\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)\]
\case{} \(f\;x = i_2\;a\) and \(g (h\;x) = i_2\;b\)\\
Note that \((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{mycase}
\item \ref{law: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 ]}^\sharp\;z\) for any \(z : X + Y\).
Let us first establish the following fact
\[f^\sharp\;c = {[(id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;c) \qquad \text{for any } c : X, \tag{*}\label{folding-helper}\]
which follows by case distinction on \(f\;c\) and coinduction:
\begin{mycase}
\case{} \(f\;c = i_1\;a\)
\[f^\sharp\;c \approx a \approx {[(id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;c)\]
\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\):
\begin{mycase}
\case{} \(z = i_1\;x\)\\
Another case distinction on \(f\;x\) yields:
\subcase{} \(f\;x = i_1\;a\)\\
We are done, since \({(f^\sharp + h)}^\sharp(i_1 \; x) = i_1\;a = (id + i_1) (f\;x) = {[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;x)\)
\subcase{} \(f\;x = i_2\;a\)\\
This concludes the first case, since:
\begin{alignat*}{1}
& {(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))\tag{\ref{folding-helper}}
\\=\;&{[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;x).
\end{alignat*}
\case{} \(z = i_2\;y\)\\
Let us proceed by discriminating on \(h\;y\).
\subcase{} \(h\;y = i_1\;a\)\\
Indeed by coinduction,
\begin{alignat*}{1}
& {(f^\sharp + h)}^\sharp(i_2 \; y)
\\=\;&later((f^\sharp + h)(i_1\;a))
\\=\;&later({[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;a))
\\=\;&{[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_2\;y)
\end{alignat*}
\subcase{} \(h\;y = i_2\;a\)\\
Similarly by coinduction,
\begin{alignat*}{1}
& {(f^\sharp + h)}^\sharp(i_2 \; y)
\\=\;&later((f^\sharp + h)(i_2\;a))
\\=\;&later({[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_2\;a))
\\=\;&{[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_2\;y)
\end{alignat*}
\end{mycase}
\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\):\\
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}
This concludes the proof that every \((Delay\;A,\approx)\) can be extended to an Elgot algebra, let us now show that these Elgot algebras are free.
Given an Elgot algebra \((B , \overset{B}{=}, {(-)}^{\sharp_b})\) and a setoid morphism \(f : A \rightarrow B\). We need to define an Elgot algebra morphism \(\free{f} : Delay\;A \rightarrow B\). Consider \(g : Delay\;A \rightarrow B + Delay\;A\) defined by
\[g\;x =
\begin{cases}
i_1(f\;a) & \text{if } x = now\;a \\
i_2\;a & \text{if } x = later\;a
\end{cases}\]
\(g\) is trivially a setoid morphism with respect to strong bisimilarity, we can thus take \(\free{f} = g^{\sharp_b} : Delay\;A \rightarrow B\). Next, we need to show that \(g^{\sharp_b}\) is a setoid morphism with respect to weak bisimilarity.
Let us now show that \(g^{\sharp_b}\) is iteration preserving. Given a setoid morphism \(h : X \rightarrow Delay\;A + X\) with respect to weak bisimilarity, 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\).
We will first need to introduce the notion of discretized setoid. Given a setoid \((Z, \overset{Z}{=})\) the discretized setoid is defined as \(\disc{Z} := (Z , \equiv)\). Given a setoid morphism \(u : (Z, \overset{Z}{=}) \rightarrow (A, \approx) + (Z, \overset{Z}{=})\), we can define its discretized version \(\bar{u} : \disc{Z} \rightarrow (A, \sim) + \disc{Z}\) which is a setoid morphism with respect to strong bisimilarity. Now, the following will be key for proving preservation:
\[u^\sharp\;x \sim \bar{u}^\sharp\;x \qquad \text{ for any } x : X,\]
which follows by coinduction and case distinction on \(u\;x\).
Now, we can continue with the proof of preservation. We will proceed by showing that
\[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\]
\end{proof}