work on thesis

thesis/bib.bib

@@ -239,4 +239,11 @@
   timestamp  = {Mon, 13 Aug 2018 16:47:19 +0200},
   biburl     = {https://dblp.org/rec/journals/corr/GoncharovSR14.bib},
   bibsource  = {dblp computer science bibliography, https://dblp.org}
+}
+
+@online{nad-delay,
+  author = {Nils Anders Danielsson},
+  title = {The delay monad, defined coinductively},
+  url = {https://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.html},
+  urldate = {2024-15-02}
 }

thesis/main.tex

@@ -10,7 +10,8 @@
   breaklines=true,
   encoding=utf8,
   fontsize=\small,
-  frame=lines
+  frame=lines,
+  autogobble
 }
 \usepackage[dvipsnames]{xcolor}  % Coloured text etc.
 \usepackage{amssymb}

thesis/src/05_setoids.tex

@@ -18,9 +18,88 @@ Morphisms between setoids are functions that respect the equivalence relation:
 
 Setoids and setoid morphisms form a category that we call $\setoids$.
 
+\improvement[inline]{Talk about equality between setoid morphisms}
 \improvement[inline]{Text is not good}
-\todo[inline]{sketch the proof that setoids is CCC and cocartesian}
 
+\begin{lemma}
+  $\setoids$ is a distributive category.
+\end{lemma}
+\begin{proof}
+  To show that $\setoids$ is (co-)cartesian we will give the respective datatypes 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.
+
+  \begin{itemize}
+    \item \textbf{Products}:
+    \begin{minted}{agda}
+      record _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
+        constructor _,_
+        field
+          fst : A
+          snd : B
+  
+      <_,_> : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} 
+              → (A → B) → (A → C) → A → (B × C)
+      < f , g > x = (f x , g x)
+    \end{minted}
+    \item \textbf{Terminal Object}:
+    \begin{minted}{agda}
+      record ⊤ {l} : Set l where
+        constructor tt
+    
+      ! : ∀ {l} {X : Set l} → X → ⊤ {l}
+      ! _ = tt
+    \end{minted}
+    \item \textbf{Coproducts}:
+    \begin{minted}{agda}
+      data _+_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
+        i₁ : A → A + B
+        i₂ : B → A + B 
+    
+      [_,_] : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
+              → (A → C) → (B → C) → (A + B) → C
+      [ f , g ] (i₁ x) = f x
+      [ f , g ] (i₂ x) = g x
+    \end{minted}
+    \item \textbf{Initial Object}:
+    \begin{minted}{agda}
+      data ⊥ {l} : Set l where
+
+      ¡ : ∀ {l} {X : Set l} → ⊥ {l} → X
+      ¡ ()    
+    \end{minted}
+  \end{itemize}
+
+  Lastly we need to show that the canonical distributivity morphism is an iso. Recall that the canonical distributive morphism is defined as $dstl^{-1} = [ id \times i_1 , id \times i_2 ] : A \times B + A \times C \rightarrow A \times (B + C)$. This corresponds to the following definition using pattern matching:
+  \begin{minted}{agda}
+    distributeˡ⁻¹ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} 
+                    → (A × B) + (A × C) → A × (B + C)
+    distributeˡ⁻¹ (i₁ (x , y)) = (x , i₁ y)
+    distributeˡ⁻¹ (i₂ (x , y)) = (x , i₂ y)
+  \end{minted}
+  The inverse can be defined similarly:
+  \begin{minted}{agda}
+    distributeˡ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} 
+                  → A × (B + C) → (A × B) + (A × C)
+    distributeˡ (x , i₁ y) = i₁ (x , y)
+    distributeˡ (x , i₂ y) = i₂ (x , y)
+  \end{minted}
+  Then these functions are inverse by definition and it is easy to show that they are setoid morphisms.
+\end{proof}
+
+\begin{lemma}
+  $\setoids$ is cartesian closed.
+\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 pointwise equality of setoid morphisms i.e. $f , g : A \rightarrow B$ are pointwise equal $f \doteq g$ \textit{iff} $f x =^B g x$ for any $x : A$. $curry$ and $eval$ are then defined as usual:
+  \begin{minted}{agda}
+    curry : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} 
+            → (C × A → B) → C → A → B
+    curry f x y = f (x , y) 
+
+    eval : ∀ {a b} {A : Set a} {B : Set b} → ((A → B) × A) → B
+    eval (f , x) = f x
+  \end{minted}
+\end{proof}
 
 \section{Quotienting the Delay Monad}
 % TODO merge this into introduction
@@ -31,14 +110,14 @@ Setoids and setoid morphisms form a category that we call $\setoids$.
 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
+  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:
+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