diff --git a/README.md b/README.md index 823402c..0094066 100644 --- a/README.md +++ b/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. -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/ +This repository contains the work I have done for my bachelor 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. +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. -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` +The subfolders contain my code, the thesis and the slides of my presentation, each with its own README documenting how to build it. \ No newline at end of file diff --git a/agda/README.md b/agda/README.md new file mode 100644 index 0000000..af356a7 --- /dev/null +++ b/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` diff --git a/slides/README.md b/slides/README.md new file mode 100644 index 0000000..c31fd03 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/thesis/README.md b/thesis/README.md new file mode 100644 index 0000000..76a08e5 --- /dev/null +++ b/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. \ No newline at end of file