minor

agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md

@@ -3,7 +3,7 @@
 {-# OPTIONS --allow-unsolved-metas --guardedness #-}
 open import Level
 open import Relation.Binary
-open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
+open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′)
 open import Data.Sum.Function.Setoid
 open import Data.Sum.Relation.Binary.Pointwise
 open import Function.Equality as SΠ renaming (id to idₛ)
@@ -186,9 +186,15 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where
     ; *-uniq = λ {B} f g g≋f {x} {y} x∼y → g≋f x∼y 
     }
     where
-      -- TODO use fixpoint for this 
-      *-preserves : ∀ {B : Elgot-Algebra} (f : delaySetoid A ⟶ Elgot-Algebra.A B) {X : Setoid ℓ ℓ} {g : X ⟶ (delaySetoid A) ⊎ₛ X} → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → Elgot-Algebra.A B [ (f ._⟨$⟩_ ∘′ iter {A} {X} (g ._⟨$⟩_)) x ∼ ((B Elgot-Algebra.#) _) ⟨$⟩ y ]
-      *-preserves {B} f {X} {g} {x} {y} x∼y = {!   !}
+    -- TODO use fixpoint for this 
+    *-preserves : ∀ {B : Elgot-Algebra} (f : delaySetoid A ⟶ Elgot-Algebra.A B) {X : Setoid ℓ ℓ} {g : X ⟶ (delaySetoid A) ⊎ₛ X} → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → Elgot-Algebra.A B [ (f ._⟨$⟩_ ∘′ iter {A} {X} (g ._⟨$⟩_)) x ∼ ((B Elgot-Algebra.#) _) ⟨$⟩ y ]
+    *-preserves {B} f {X} {g} {x} {y} x∼y = ∼-sym (Elgot-Algebra.A B) (∼-trans (Elgot-Algebra.A B) (#-Fixpoint (∼-sym X x∼y)) helper)
+      where
+      open Elgot-Algebra B using (#-Fixpoint)
+      helper : Elgot-Algebra.A B [ {!   !} x ∼ (f ._⟨$⟩_ ∘′ iter {A} {X} (g ._⟨$⟩_)) x ] -- ([ (f ._⟨$⟩_) , _ ] ∘′ g ._⟨$⟩_)
+      helper with g ⟨$⟩ x in eqx 
+      ...    | inj₁ a = {!   !}
+      ...    | inj₂ b = {!   !}
 
   -- TODO remove
   delayPreElgot : IsPreElgot delayMonad

thesis/bib.bib

@@ -1,4 +1,11 @@
-@inproceedings{10.1145/3437992.3439922,
+@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-categories,
   author    = {Hu, Jason Z. S. and Carette, Jacques},
   title     = {Formalizing Category Theory in Agda},
   year      = {2021},

thesis/main.tex

@@ -17,13 +17,19 @@
 \usepackage{graphicx}
 \usepackage[style=ieee, sorting=ynt]{biblatex}    %advanced citations
 \usepackage[english=british]{csquotes}           %biblatex recommended to load this
-\usepackage{listings}[language = haskell]
+\usepackage{listings}
+  [
+  language=agda, 
+  extendedchars=true, 
+  inputencoding=utf8, 
+  ]
 \usepackage{multicol}
 \addbibresource{bib.bib}
 %\usepackage[right]{showlabels}
 %\usepackage[justific=raggedright,totoc]{idxlayout}
 \usepackage[type=CC, modifier=by-sa,version=4.0]{doclicense}
 
+\lstset{mathescape}
 
 \addto\extrasenglish{%
   \renewcommand{\chapterautorefname}{Section}

thesis/src/01_preliminaries.tex

@@ -34,7 +34,7 @@ For programmers a second equivalent definition is more useful:
   \end{enumerate}
 \end{definition}
 
-In functional languages like Haskell the Kleisli lifting is usually called \textit{bind} or written infix as \lstinline{>>=} and $\eta$ is called $return$. Given two morphisms $f : X \rightarrow MY, g : Y \rightarrow MZ$, where $M$ is a Kleisli triple the composition $g^* \circ f$ can then be (pointfully) written as \lstinline{f x >>= g} or using Haskell's do-notation:
+In functional languages like Haskell the Kleisli lifting is usually called \textit{bind} or written infix as \lstinline{>>=} and $\eta$ is called $return$. Given two morphisms $f : X \rightarrow MY, g : Y \rightarrow MZ$, where $M$ is a Kleisli triple the composition $g^* \circ f$ can then be (in a pointful manner) written as \lstinline{f x >>= g} or using Haskell's do-notation:
 \begin{lstlisting}
   do y <- f x
      g y

thesis/src/02_agda-categories.tex

@@ -1,4 +1,19 @@
 \chapter{Formalizing Category Theory in Agda}
-% IDEAS:
-%% - why agda? talk about other approaches i.e. HOTT, coq, ...
-%% - show some basic definitions like category and functor 
+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.

thesis/src/A1_contributions.tex

@@ -4,7 +4,7 @@ Many basic definitions that were needed for the formalization of this thesis wer
 
 % TODO chapter formalizing category theory first 
 \section{Kleisli Triple}
-
+% citation for relative monad: https://arxiv.org/abs/1412.7148
 \section{Commutative Monad}
 \section{Distributive Categories}
 \section{Stable Natural Numbers Object}