Added thesis, changed folder structure

.gitignore

@@ -1,3 +1,4 @@
+# agda 
 *.agdai
 *.pdf
 *.log
@@ -5,3 +6,47 @@ Everything.agda
 public/
 .direnv
 .DS_Store
+
+# latex
+# put this to .git/info/exclude in git repos managing latex
+#
+# git ls-files --others --exclude-from=.git/info/exclude
+# Lines that start with '#' are comments.
+# For a project mostly in C, the following would be a good set of
+# exclude patterns (uncomment them if you want to use them):
+# *.[oa]
+.*.swp
+.#*
+*~
+*.pdf
+# AUTOGENERATED
+# All wildcards below this marker are used to remove generated files in
+# 'make clean'
+*.aux
+*.fdb_latexmk
+*.log
+*.out
+*.pdf
+*.synctex.gz
+*.toc
+*.bbl
+*.blg
+*.idx
+*.ilg
+*.fls
+*.ind
+*.zip
+*.dvi
+*.eps
+*.bcf
+*.run.xml
+*.nav
+*.snm
+*.vrb
+*.vtc
+*.spl
+*.nlo
+*.nls
+*.auxlock
+.auctex-auto/
+_region_.tex

thesis/.vscode/settings.json

@@ -0,0 +1,25 @@
+{
+"latex-workshop.latex.tools" : [
+  {
+    "name": "latexmk-main",
+    "command": "latexmk",
+    "args": [
+      "-synctex=1",
+      "-interaction=nonstopmode",
+      "-file-line-error",
+      "-pdf",
+      "-outdir=%OUTDIR%",
+      "main.tex"
+    ],
+    "env": {}
+  }
+],
+"latex-workshop.latex.recipes": [
+  {
+    "name": "latexmk-main",
+    "tools": [
+      "latexmk-main"
+    ]
+  },
+]
+}

thesis/Makefile

@@ -0,0 +1,20 @@
+src = $(wildcard *.tex)
+pdf = $(src:.tex=.pdf)
+imgpdf = $(wildcard img/*.pdf)
+
+.PHONY: all clean install
+
+all: $(pdf) $(imgpdf)
+
+%.pdf: %.tex $(wildcard src/*.tex) $(wildcard *.bib) $(imgpdf)
+	latexmk -file-line-error -synctex=1 -halt-on-error -pdf $<
+
+fast:
+	# enforce tex execution
+	pdflatex -synctex=1 $(src)
+
+clean:
+	latexmk -C $(src)
+	rm -f $(wildcard *.out *.nls *.nlo *.bbl *.blg *-blx.bib *.run.xml *.bcf *.synctex.gz *.fdb_latexmk *.fls *.toc)
+	rm -f $(wildcard src/*.aux)
+

thesis/README.adoc

@@ -0,0 +1,42 @@
+README
+======
+
+About
+-----
+The present collection of files offers a template for a final thesis (no matter
+whether project, bachelor, or master thesis). You are welcome to modify anything
+to your personal needs. In case of any ambiguity, consult your supervisor on
+formal aspects of the document, instead of just relying of my design choices for
+the present template.
+
+Also see the content of template-master-thesis.pdf for some more suggestions.
+
+Usage
+-----
+It is strongly recommended to use a latex wrapper like latexmk (or rubber), in
+order to build it. You can find a Makefile in the toplevel directory providing
+a nice interface to latexmk:
+
+Type `make` In order to build the PDF, type `make clean` to remove all
+automatically generated files (including the PDF).
+
+License of this Template
+------------------------
+You can freely use the present template for your final thesis (i.e. master or bachelor or project thesis).
+It is not mandatory at all to use this template for your final thesis.
+It is just a suggestion! You are also allowed to change anything you would like to change in order to fit your needs/taste/...
+
+License for your Thesis
+-----------------------
+The template includes a http://creativecommons.org/licenses/by-sa/4.0/[Creative Commons Attribution-ShareAlike 4.0 International License] license remark as suggested license for your thesis.
+We suggest you keep this license although you are free to choose a different license.
+
+License for your Implementation
+-------------------------------
+For implementations you write as part of your thesis we recommend to use a different repository and license this code under an Open Source license like GPL-3 or Apache.
+When choosing a license for your implementations keep in mind that containing/modifying previous implementations licensed under GPL-3 requires you to use GPL-3 for your code as well.
+
+It is common to indicate the license of your code via a file called LICENSE in the folder of your repository.
+If such a file does not exist already, GitLab displays a button "Add LICENSE" where you can select from common licenses as a template.
+
+// vim: tw=80 ft=asciidoc

thesis/agda/motivation.agda

@@ -0,0 +1,75 @@
+{-# OPTIONS --guardedness #-}
+
+-- Take this example as motivation:
+-- https://stackoverflow.com/questions/21808186/agda-reading-a-line-of-standard-input-as-a-string-instead-of-a-costring
+
+open import Level
+open import Agda.Builtin.Coinduction
+module thesis.motivation where
+
+module old-delay where
+  private
+    variable
+      a : Level
+  data _⊥ (A : Set a) : Set a where
+    now : A → A ⊥
+    later : ∞ (A ⊥) → A ⊥
+
+  never : ∀ {A : Set a} → A ⊥
+  never = later (♯ never)
+
+module ReverseInput where
+  open import Data.Char
+  open import Data.Nat
+  open import Data.List using (List; []; _∷_)
+  open import Data.String
+  open import Data.Unit.Polymorphic
+  open import Codata.Musical.Costring
+  open import Codata.Musical.Colist using ([]; _∷_)
+  -- open import IO using (IO; seq; bind; return; Main; run; putStrLn)
+  open import IO.Primitive
+  open import IO.Primitive.Infinite using (getContents)
+  open import Agda.Builtin.IO using ()
+
+  open old-delay
+  -- IDEA: start in haskell, then motivate in agda and define delay type
+  -- next talk about bisimilarity.
+  -- idea for slide title: dlrowolleh.hs and dlrowolleh.agda
+
+  private
+    variable
+      a : Level
+
+  -- reverse : Costring → String ⊥
+  -- reverse = go []
+  --   where
+  --   go : List Char → Costring → String ⊥
+  --   go acc []       = now (fromList acc)
+  --   go acc (x ∷ xs) = later (♯ go (x ∷ acc) (♭ xs))
+
+  -- putStrLn⊥ : String ⊥ → IO {a} ⊤
+  -- putStrLn⊥ (now   s) = putStrLn s
+  -- putStrLn⊥ (later s) = seq (♯ return tt) (♯ putStrLn⊥ (♭ s))
+
+  -- main : Main
+  -- main = run (bind (♯ {!  getContents !}) {!   !}) --(λ c → ♯ putStrLn⊥ (reverse c)))
+
+-- NOTE: This is not very understandable... Better stick to the outdated syntax
+module delay where
+  mutual
+    data _⊥ (A : Set) : Set where
+      now : A → A ⊥
+      later : A ⊥' → A ⊥
+    
+    record _⊥' (A : Set) : Set where
+      coinductive
+      field
+        force : A ⊥
+  open _⊥'
+
+  mutual
+    never : ∀ {A : Set} → A ⊥
+    never = later never'
+
+    never' : ∀ {A : Set} → A ⊥'
+    force never' = never

thesis/bib.bib

@@ -0,0 +1,52 @@
+@inproceedings{10.1145/3437992.3439922,
+  author    = {Hu, Jason Z. S. and Carette, Jacques},
+  title     = {Formalizing Category Theory in Agda},
+  year      = {2021},
+  isbn      = {9781450382991},
+  publisher = {Association for Computing Machinery},
+  address   = {New York, NY, USA},
+  url       = {https://doi.org/10.1145/3437992.3439922},
+  doi       = {10.1145/3437992.3439922},
+  abstract  = {The generality and pervasiveness of category theory in modern mathematics makes it a frequent and useful target of formalization. It is however quite challenging to formalize, for a variety of reasons. Agda currently (i.e. in 2020) does not have a standard, working formalization of category theory. We document our work on solving this dilemma. The formalization revealed a number of potential design choices, and we present, motivate and explain the ones we picked. In particular, we find that alternative definitions or alternative proofs from those found in standard textbooks can be advantageous, as well as "fit" Agda's type theory more smoothly. Some definitions regarded as equivalent in standard textbooks turn out to make different "universe level" assumptions, with some being more polymorphic than others. We also pay close attention to engineering issues so that the library integrates well with Agda's own standard library, as well as being compatible with as many of supported type theories in Agda as possible.},
+  booktitle = {Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs},
+  pages     = {327–342},
+  numpages  = {16},
+  keywords  = {formal mathematics, Agda, category theory},
+  location  = {Virtual, Denmark},
+  series    = {CPP 2021}
+}
+
+@incollection{Altenkirch_2017,
+  doi       = {10.1007/978-3-662-54458-7_31},
+  url       = {https://doi.org/10.1007%2F978-3-662-54458-7_31},
+  year      = {2017},
+  publisher = {Springer Berlin Heidelberg},
+  pages     = {534--549},
+  author    = {Thorsten Altenkirch and Nils Anders Danielsson and Nicolai Kraus},
+  title     = {Partiality, Revisited},
+  booktitle = {Lecture Notes in Computer Science}
+}
+
+@article{delay2005,
+  doi       = {10.2168/lmcs-1(2:1)2005},
+  url       = {https://doi.org/10.2168%2Flmcs-1%282%3A1%292005},
+  year      = {2005},
+  month     = {jul},
+  publisher = {Centre pour la Communication Scientifique Directe ({CCSD})},
+  volume    = {Volume 1, Issue 2},
+  author    = {Venanzio Capretta},
+  title     = {General Recursion via Coinductive Types},
+  journal   = {Logical Methods in Computer Science}
+}
+
+@inproceedings{uni-elgot2021,
+  doi       = {10.4230/LIPICS.ICALP.2021.131},
+  url       = {https://drops.dagstuhl.de/opus/volltexte/2021/14200/},
+  author    = {Goncharov, Sergey},
+  keywords  = {Elgot monad, partiality monad, delay monad, restriction category, Theory of computation → Categorical semantics, Theory of computation → Constructive mathematics},
+  language  = {en},
+  title     = {Uniform Elgot Iteration in Foundations},
+  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
+  year      = {2021},
+  copyright = {Creative Commons Attribution 4.0 International license}
+}

thesis/main.tex

@@ -0,0 +1,110 @@
+\documentclass[a4paper,11pt,numbers=noenddot]{scrbook}
+
+\usepackage[top=2cm,lmargin=1in,rmargin=1in,bottom=3cm,hmarginratio=1:1]{geometry}
+\usepackage[utf8]{inputenc}
+\usepackage[ngerman,english]{babel}
+\babeltags{german=ngerman}
+\usepackage{amssymb}
+\usepackage{amsthm}
+\usepackage{thmtools}
+\usepackage{fancyvrb}
+\usepackage{mathtools}
+\usepackage{amsmath}
+\usepackage{ifthen}
+\usepackage{xspace}
+\usepackage{hyperref}
+\usepackage{makeidx}
+\usepackage{graphicx}
+\usepackage[style=ieee, sorting=ynt]{biblatex}    %advanced citations
+\usepackage[english=british]{csquotes}           %biblatex recommended to load this
+\addbibresource{bib.bib}
+%\usepackage[right]{showlabels}
+%\usepackage[justific=raggedright,totoc]{idxlayout}
+\usepackage[type=CC, modifier=by-sa,version=4.0]{doclicense}
+
+
+\addto\extrasenglish{%
+  \renewcommand{\chapterautorefname}{Section}
+  \renewcommand{\sectionautorefname}{Section}
+  \renewcommand{\subsectionautorefname}{Subsection}
+  }
+
+\newcommand\chap[1]{%
+  \chapter*{#1}%
+  \chaptermark{#1}%
+  \addcontentsline{toc}{chapter}{#1}}
+
+\declaretheorem[name=Definition,style=definition,numberwithin=chapter]{definition}
+\declaretheorem[name=Example,style=definition,sibling=definition]{example}
+\declaretheorem[style=definition,numbered=no]{exercise}
+\declaretheorem[name=Remark,style=definition,sibling=definition]{remark}
+\declaretheorem[name=Assumption,style=definition,sibling=definition]{assumption}
+\declaretheorem[name=Observation,style=definition,sibling=definition]{observation}
+\declaretheorem[name=Theorem,sibling=definition]{theorem}
+\declaretheorem[sibling=definition]{corollary}
+\declaretheorem[name=Fact,sibling=definition]{fact}
+\declaretheorem[sibling=definition]{lemma}
+\declaretheorem[sibling=lemma]{proposition}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                                                                         %
+%                   Spacing settings                                      %
+%                                                                         %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\setlength{\parindent}{0pt}
+\setlength{\parskip}{6pt}
+\setlength{\marginparsep}{0cm}
+
+\title{Implementing Notions of Partiality and Delay in Agda}
+
+\author{Leon Vatthauer}
+
+\makeatletter
+\hypersetup{
+  pdfauthor={\@author},
+  pdftitle={\@title},
+  % kill those ugly red rectangles around links
+  hidelinks,
+}
+\newcommand*{\theauthor}{\@author}
+\makeatother
+
+\begin{document}
+\pagestyle{plain}
+\input{src/titlepage}%
+\chapter*{Disclaimer}
+\begin{german}
+Ich versichere, dass ich die Arbeit ohne fremde Hilfe und ohne Benutzung anderer als der angegebenen Quellen angefertigt habe und dass die Arbeit in gleicher oder ähnlicher Form noch keiner anderen Prüfungsbehörde vorgelegen hat und von dieser als Teil einer Prüfungsleistung angenommen wurde.
+Alle Ausführungen, die wörtlich oder sinngemäß übernommen wurden, sind als solche gekennzeichnet.
+
+\vspace{5em}
+Erlangen, \today{} \rule{7cm}{1pt}\\
+\phantom{Erlangen, \today{}} \theauthor{}
+\end{german}
+
+\chapter*{Licensing}
+\doclicenseThis{}
+\tableofcontents
+% \include{src/examples}
+\include{src/00_introduction}
+
+%% IDEA: swap chapter 01 and 02, first introduce category theory in agda and then subsequently explain every notion in preliminaries with agda code.
+%% This is a major design decision..., there are two alternatives:
+%%% - 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/10_conclusion}
+
+\appendix
+\include{src/A1_contributions}
+
+\medskip
+
+\printbibliography[heading=bibintoc]{}
+\end{document}
+
+% vim: tw=80 nospell spelllang=en nocul

thesis/src/00_introduction.tex

@@ -0,0 +1,2 @@
+\chapter{Introduction}
+citing elgot~\cite{uni-elgot2021}

thesis/src/01_preliminaries.tex

@@ -0,0 +1,4 @@
+\chapter{Preliminaries}
+\section{Stable Natural Numbers Object}
+\section{Extensive and Distributive Categories}
+\section{Strong and Commutative Monads}

thesis/src/02_agda-categories.tex

@@ -0,0 +1,4 @@
+\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 

thesis/src/03_iteration.tex

@@ -0,0 +1,3 @@
+\chapter{Iteration Algebras and Monads}
+\section{Elgot Algebras}
+\section{Pre-Elgot Monads}

thesis/src/04_partiality-monads.tex

@@ -0,0 +1,4 @@
+\chapter{Partiality Monads}
+\section{Classifying Partiality Monads}
+\section{The Maybe Monad}
+\section{The Delay Monad}

thesis/src/05_monadK.tex

@@ -0,0 +1 @@
+\chapter{The K monad}

thesis/src/10_conclusion.tex

@@ -0,0 +1 @@
+\chapter{Conclusion}

thesis/src/A1_contributions.tex

@@ -0,0 +1,5 @@
+\chapter{Open Source Contributions}
+% IDEA: Include formalization of kleisli-triple, distributive category and PNNO in appendix.
+\section{Kleisli Triple}
+\section{Distributive Categories}
+\section{Stable Natural Numbers Object}

thesis/src/examples.tex

@@ -0,0 +1,129 @@
+\chapter{Some Introduction and Examples}
+You can freely use the present template for your final thesis (i.e.~master or
+bachelor or project thesis).
+
+This template was made from the following theses:
+\begin{itemize}
+\item \url{http://thorsten-wissmann.de/theses/ma-wissmann.pdf}
+\item \url{http://thorsten-wissmann.de/theses/project-wissmann.pdf}
+\item \url{http://thorsten-wissmann.de/theses/bachelor-thesis-wissmann.pdf}
+\end{itemize}
+
+\section{Meaning}
+It is not mandatory at all to use this template for your final thesis. It is
+just a suggestion! You are also allowed to change anything you would like to
+change in order to fit your needs/taste/$\ldots$.
+
+Of course, you should adjust some places when using it for your final thesis:
+\begin{enumerate}
+\item In the parameters to the \texttt{hyperref}-package, you should adjust the
+fields \texttt{pdfauthor} and \texttt{pdftitle} to your name and the title of
+your thesis.
+
+\item In \texttt{src/titlepage.tex} you should adjust the title and (possibly
+the) subtitle of your thesis, the degree of your thesis (Masters degree?
+Bachelor?), your name and the name of your advisors.
+
+\end{enumerate}
+
+\section{Some hints}
+\subsection{Macros}
+
+% some macros only needed for these hints here
+\newcommand{\C}{\ensuremath{\mathcal{C}}\xspace}
+\newcommand{\preview}[2]{
+\begin{center}
+\fbox{\begin{minipage}[t]{.47\textwidth}
+#1
+\end{minipage}}%
+\hspace{.02\textwidth}%
+\fbox{\begin{minipage}[t]{.47\textwidth}
+#2
+\end{minipage}}%
+\end{center}}
+
+When using certain mathematical symbols very often, it makes sense to define
+macros for them, e.g.~
+\begin{verbatim}
+\newcommand{\C}{\ensuremath{\mathcal{C}}\xspace}
+\end{verbatim}
+The \texttt{ensuremath} enforces mathmode and the \texttt{xspace} inserts a
+space if necessary:
+\preview{
+\Verb|Some \textbackslash C in the midle of the sentence|
+\Verb|and at the end: \textbackslash C.|
+}{
+Some \C in the midle of the sentence
+and at the end: \C.
+}
+
+\subsection{UTF-8}
+
+I strongly recommend exploiting the utf8 capability of \LaTeX:
+
+\begin{verbatim}
+\usepackage{newunicodechar}
+\newunicodechar{∀}{\ensuremath{\forall}}
+\newunicodechar{∃}{\ensuremath{\exists}}
+\newunicodechar{×}{\ensuremath{\times}}
+\newunicodechar{ø}{\ensuremath{\emptyset}}
+\newunicodechar{≤}{\ensuremath{\le}}
+\newunicodechar{∈}{\ensuremath{\in}}
+\newunicodechar{→}{\ensuremath{\to}}
+\newunicodechar{⊆}{\ensuremath{\subseteq}}
+\newunicodechar{⊗}{\ensuremath{\otimes}}
+\newunicodechar{∧}{\ensuremath{\wedge}}
+\end{verbatim}
+
+with that, you can write:
+\begin{verbatim}
+    \begin{definition}[Transitivity]
+    A relation $\text{``}≤\text{''} ⊆ X×X$ has upper bounds if
+    \[
+        ∀a,b ∈ X\ ∃ c ∈ X: a ≤ c ∧ b ≤ c
+    \]
+    \end{definition}
+\end{verbatim}
+
+It will result in the following:
+
+    \begin{definition}[Transitivity]
+    A relation $\text{``}≤\text{''} ⊆ X×X$ has upper bounds if
+    \[
+        ∀a,b ∈ X\ ∃ c ∈ X: a ≤ c ∧ b ≤ c
+    \]
+    \end{definition}
+
+In order to input unicode characters, just configure a compose key, e.g.:
+\begin{itemize}
+\item \url{https://en.wikipedia.org/wiki/Compose_key}
+\item
+\url{https://wiki.archlinux.org/index.php/Keyboard_configuration_in_Xorg#Configuring_compose_key}
+
+\end{itemize}
+
+\subsection{Autoref}
+
+Let \LaTeX~include whether something references is a definition or what else
+using the \texttt{\textbackslash autoref} command:
+
+\begin{verbatim}
+    \begin{definition}[label={relation},name={Relation}]
+    A relation $R$ between sets $X$ and $Y$ is just a subset of $X×Y$.
+    \end{definition}
+    We have just seen \autoref{relation}.
+\end{verbatim}
+
+This results in:
+
+
+    \begin{definition}[label={relation},name={Relation}]
+    A relation $R$ between sets $X$ and $Y$ is just a subset of $X×Y$.
+    \end{definition}
+    We have just seen \autoref{relation}.
+
+\subsection{Further Comments}
+For even more convenience while writing, you should look at the following:
+synctex, git (for managing your \TeX-sources).
+
+% vim: tw=80 nospell spelllang=en nocul

thesis/src/titlepage.tex

@@ -0,0 +1,50 @@
+\begin{titlepage}
+\newcommand{\drop}{0.07\textheight}
+\begin{center}
+\begingroup%
+\vfill
+{\LARGE\textsc{%
+Friedrich-Alexander-Universität\\[2mm]
+Erlangen-Nürnberg%
+}}\\[\drop]
+{%
+% trim= left bottom right top
+\includegraphics[height=1.8cm,trim=0cm 0mm 0 0mm]{img/tcs}\\
+\textsc{\large Chair for Computer Science 8}\\
+\textsc{\large Theoretical Computer Science}}%\\[\drop]
+\vfill
+\rule{\textwidth}{1pt}\par
+\vspace{0.5\baselineskip}
+{% maybe \itshape?
+  \Huge\bfseries
+  \makeatletter
+  \@title \\[1cm]
+  \makeatother
+\large\bfseries
+An exploration of \ldots % TODo
+\\ and \ldots
+\\[1cm]
+\textbf{\large Bachelor Thesis in Computer Science}
+}\\[0.5\baselineskip]
+\rule{\textwidth}{1pt}\par
+\vfill
+{\Large{\makeatletter\@author\makeatother}
+  %\\ {\large\normalsize{maybe-ur-mail@example.org}}
+}
+\vfill
+\large Advisor:
+\vfill
+\begin{tabular}{ccc}
+    \large
+    Sergey Goncharov
+\end{tabular}
+\vfill
+% trim= left bottom right top
+\includegraphics[height=1.8cm,trim=0cm -5mm 0 0mm]{img/fau}
+\vfill
+{\large Erlangen, \today}
+\endgroup
+\end{center}
+\end{titlepage}
+
+% vim: tw=80 spell spelllang=en nocul