minor

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

@@ -118,7 +118,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
       helper'' rewrite eqx = ∼-refl (A ⊥ₛ ⊎ₛ Y)
       helper : (A ⊥ₛ ⊎ₛ Y) [ inj₂ (h ⟨$⟩ a) ∼ inj₁ c ]
       helper rewrite (≡-sym eqc) = ∼-trans (A ⊥ₛ ⊎ₛ Y) helper'' helper'
-  ...                                                                  | inj₂ c = ≈-trans (later≈ {A} {_} {♯ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ a)} (♯ (iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh (∼-refl X)))) (later≈ (♯ iter-cong g (∼-sym Y helper)))
+  ...                                                                  | inj₂ c = later≈ {!   !} -- ≈-trans (later≈ {A} {_} {♯ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ a)} (♯ (iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh (∼-refl X)))) (later≈ (♯ iter-cong g (∼-sym Y helper)))
   -- why does this not terminate??
   -- | inj₂ c = ≈-trans (later≈ {A} {_} {♯ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ a)} (♯ (iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh (∼-refl X)))) (later≈ (♯ iter-cong g (∼-sym Y helper)))
     where
@@ -193,7 +193,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
 
   delay-lift' : ∀ {A B : Set ℓ} → (A → B) → A ⊥ → B
   delay-lift' {A} {B} f (now x) = f x
-  delay-lift' {A} {B} f (later x) = {!    !}
+  delay-lift' {A} {B} f (later x) = {!    !} -- (id + f ∘ out)#b
 
   delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B
   delay-lift {A} {B} f = record { h = record { _⟨$⟩_ = delay-lift' {∣ A ∣} {∣ ⟦ B ⟧ ∣} (f ._⟨$⟩_) ; cong = {!   !} } ; preserves = {!   !} }

thesis/main.tex

@@ -103,10 +103,11 @@ Erlangen, \today{} \rule{7cm}{1pt}\\
 %%% - introduce notions in latex and later give agda code (maybe in appendix)
 %%% - introduce notions in agda directly (maybe unreadable, maybe duplication with appendix)
 \include{src/01_preliminaries}
-\include{src/02_agda-categories}
-\include{src/03_iteration}
-\include{src/04_partiality-monads}
-\include{src/05_monadK}
+%\include{src/03_iteration}
+%\include{src/04_partiality-monads}
+\chapter{Modelling partiality}
+% \include{src/05_monadK}
+\chapter{Case Study: The Quotiented Delay Monad}
 \include{src/10_conclusion}
 
 \appendix

thesis/src/01_preliminaries.tex

@@ -1,15 +1,30 @@
-\chapter{Preliminaries}
+\chapter{Category Theory in Agda}
+
+There are many formalizations of category theory in proof assistants like Coq or Agda. The benefits are clear, having a usable formalization allows one to reason about categorical notions in a typechecked environment that makes errors less likely.
+Also ideally such a development will bring researchers together and enable them to work in a unified setting.
+In this thesis we will work with the dependently typed programming language Agda~\cite{agda} and the agda-categories~\cite{agda-categories} library by Jason Hu and Jacques Carette that gives us a good foundation of categorical definitions to work with. In this section we will talk about some design decisions that Hu and Carette made in their library that influence this development.
+
+\section{Setoid Enriched Categories}
+The usual textbook definition of category hides 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}
+  \item A collection of objects
+  \item A collection of morphisms between objects
+  \item For every two morphisms $f : X \rightarrow Y, g : Y \rightarrow Z$ another morphism $g \circ f : X \rightarrow Z$ called the composition
+  \item For every object $X$ a morphism $id_X : X \rightarrow X$ called the identity
+\end{itemize}
+where the composition is associative and the identity morphisms are identities with respect to the composition.
+\end{definition}
+
+Here a \textit{collection} usually is something that behaves set-like, but prevents size issues (there is no collection of all collections, avoiding Russel's Paradox). Agda's type theory does not have these size problems, so one can use Agda's built-in infinite \lstinline|Set| hierarchy for the collections. One question that is still open is how to express equality between morphisms. A tempting possibility is the built-in propositional equality \lstinline|_$\equiv$_| ... but bla bla use setoid, give category definition in agda.
+
+
+% TODO move
 We assume familiarity with basic concepts of category theory that should be taught in any introductory course, or can be looked up in~\cite{Lane1971}. In particular we will need the notions of category, functor, functor algebra, natural transformation, product and coproduct.
 
-In the rest of this section we will look at other categorical notions that are either less well-known, or crucial for this thesis and therefore require special attention.
-
-% TODO add conventions i.e. \C for categories, how do products and coproducts look, etc.
-
-\section{Stable Natural Numbers Object}
-
-\section{Extensive and Distributive Categories}
-
 \section{Monads}
+% TODO do in Agda
 Monads are widely known among programmers as a way of modelling effects in pure languages. Categorically a Monad is a monoid in the category of endofunctors of a category, or in more accessible terms:
 
 \begin{definition}[Monad~\cite{Lane1971}]
@@ -98,4 +113,8 @@ Now we can express the above condition:
   \[
   \tau_{X,Y}^* \circ \hat{\tau}_{X, MY} = \hat{\tau}_{X,Y}^* \circ \tau_{X, MY}
   \]
-\end{definition}
+\end{definition}
+
+\section{Stable Natural Numbers Object}
+
+\section{Extensive and Distributive Categories}

thesis/src/02_agda-categories.tex

@@ -1,19 +0,0 @@
-\chapter{Formalizing Category Theory in Agda}
-There are many formalizations of category theory in proof assistants like Coq or Agda. The benefits are clear, having a usable formalization allows one to reason about categorical notions in a typechecked environment that makes errors less likely.
-Also ideally such a development will bring researchers together and enable them to work in a unified setting.
-In this thesis we will work with the dependently typed programming language Agda~\cite{agda} and the agda-categories~\cite{agda-categories} library by Jason Hu and Jacques Carette that gives us a good foundation of categorical definitions to work with. In this section we will talk about some design decisions that Hu and Carette made in their library that influence this development.
-
-\section{Setoid Enriched Categories}
-The usual textbook definition of category hides 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}
-  \item A collection of objects
-  \item A collection of morphisms between objects
-  \item For every two morphisms $f : X \rightarrow Y, g : Y \rightarrow Z$ another morphism $g \circ f : X \rightarrow Z$ called the composition
-  \item For every object $X$ a morphism $id_X : X \rightarrow X$ called the identity
-\end{itemize}
-where the composition is associative and the identity morphisms are identities with respect to the composition.
-\end{definition}
-
-Here a \textit{collection} usually is something that behaves set-like, but prevents size issues (there is no collection of all collections, avoiding Russel's Paradox). Agda's type theory does not have these size problems, so one can use Agda's built-in infinite \lstinline|Set| hierarchy for the collections. One question that is still open is how to express equality between morphisms. A tempting possibility is the built-in propositional equality \lstinline|_$\equiv$_| ... but bla bla use setoid, give category definition in agda.