Added READMEs

README.md

@@ -1,38 +1,7 @@
-# BSc Leon Vatthauer
+# Implementing Categorical Notions of Partiality and Delay in Agda
 
-Here I am formalizing some notions of this paper [https://arxiv.org/pdf/2102.11828.pdf](https://arxiv.org/pdf/2102.11828.pdf) in agda.
+This repository contains the work I have done for my bachelor thesis.
-The whole project consists of literate agda files, where I add my documentation as markdown.
-A (mostly up to date) version can be found here: https://wwwcip.cs.fau.de/~hy84coky/bsc-thesis/
 
-## Usage
+The goal was to formalize proofs of this paper [https://arxiv.org/pdf/2102.11828.pdf](https://arxiv.org/pdf/2102.11828.pdf) in Agda and study categorical notions in general.
-The project requires a new version of agda-categories (newer than some package managers ship), so the easiest way to use this project is via the provided nix flake, which fetches my fork of agda-categories that is guaranteed to work with this project.
 
-To use the project you just have to open a development shell:
+The subfolders contain my code, the thesis and the slides of my presentation, each with its own README documenting how to build it.
-```sh
-nix develop .
-```
-(this will take 20 - 30 minutes the first time, because it has to typecheck the agda-categories library)
-
-There is also a Makefile for compiling every module and generating the html documentation.
-
-```
-make
-```
-
-## Contributions to *agda-categories*
-This project uses the awesome category theory library for agda ([agda-categories](https://github.com/agda/agda-categories)), it is already very extensive, but some notions needed here are missing, so I contribute them to the library.
-So far the contributions are:
-1. Kleisli triples [[merged](https://github.com/agda/agda-categories/pull/381)]
-    - `Categories.Monad.Construction.Kleisli`
-2. Distributive categories (and the relation to extensivity) [[merged](https://github.com/agda/agda-categories/pull/383)] [[merged](https://github.com/agda/agda-categories/pull/410)]
-    - `Categories.Category.Distributive`
-    - `Categories.Category.Distributive.Properties`
-    - `Categories.Category.Extensive.Bundle`
-    - `Categories.Category.Extensive.Properties.Distributive`
-3. Parametrized (or stable) natural numbers objects [[merged](https://github.com/agda/agda-categories/pull/394)]
-    - `Categories.Object.NaturalNumbers.Parametrized`
-    - `Categories.Object.NaturalNumbers.Properties.F-Algebra`
-    - `Categories.Object.NaturalNumbers.Properties.Parametrized`
-4. Commutative monad [[merged](https://github.com/agda/agda-categories/pull/404)]
-    - `Categories.Monad.Commutative`
-    - `Categories.Monad.Strong.Properties`

agda/README.md

@@ -0,0 +1,37 @@
+# The Agda formalization
+
+The whole project consists of literate agda files, where I add my documentation as markdown.
+A (mostly up to date) version can be found here: https://wwwcip.cs.fau.de/~hy84coky/bsc-thesis/
+
+## Usage
+The project requires a new version of agda-categories (newer than some package managers ship), so the easiest way to use this project is via the provided nix flake, which fetches my fork of agda-categories that is guaranteed to work with this project.
+
+To use the project you just have to open a development shell:
+```sh
+nix develop .
+```
+(this will take 20 - 30 minutes the first time, because it has to typecheck the agda-categories library)
+
+There is also a Makefile for compiling every module and generating the html documentation.
+
+```
+make
+```
+
+## Contributions to *agda-categories*
+This project uses the awesome category theory library for agda ([agda-categories](https://github.com/agda/agda-categories)), it is already very extensive, but some notions needed here are missing, so I contribute them to the library.
+So far the contributions are:
+1. Kleisli triples [[merged](https://github.com/agda/agda-categories/pull/381)]
+    - `Categories.Monad.Construction.Kleisli`
+2. Distributive categories (and the relation to extensivity) [[merged](https://github.com/agda/agda-categories/pull/383)] [[merged](https://github.com/agda/agda-categories/pull/410)]
+    - `Categories.Category.Distributive`
+    - `Categories.Category.Distributive.Properties`
+    - `Categories.Category.Extensive.Bundle`
+    - `Categories.Category.Extensive.Properties.Distributive`
+3. Parametrized (or stable) natural numbers objects [[merged](https://github.com/agda/agda-categories/pull/394)]
+    - `Categories.Object.NaturalNumbers.Parametrized`
+    - `Categories.Object.NaturalNumbers.Properties.F-Algebra`
+    - `Categories.Object.NaturalNumbers.Properties.Parametrized`
+4. Commutative monad [[merged](https://github.com/agda/agda-categories/pull/404)]
+    - `Categories.Monad.Commutative`
+    - `Categories.Monad.Strong.Properties`

slides/README.md

@@ -0,0 +1,8 @@
+# The slides
+This folder contains the source of my slides for the presentation at the Oberseminar on the 23.01.2024.
+
+## Requirements
+Building the slides requires a working xelatex installation. Since I am using the [minted]([minted](https://ctan.org/pkg/minted)) package for representing Agda code you will also need the Python syntax highlighter [Pygments](https://pygments.org/).
+
+## Usage
+To compile the slides just run `make` with the needed programs installed.

thesis/README.md

@@ -0,0 +1,8 @@
+# The thesis
+This folder contains the source of my thesis.
+
+## Requirements
+Building the thesis requires a working xelatex installation. Since I am using the [minted]([minted](https://ctan.org/pkg/minted)) package for representing Agda code you will also need the Python syntax highlighter [Pygments](https://pygments.org/).
+
+## Usage
+To compile the thesis just run `make` with the needed programs installed.