Merge branch 'main' of git8.cs.fau.de:theses/bsc-leon-vatthauer

.gitlab-ci.yml

@@ -1,11 +0,0 @@
-image: busybox
-
-pages:
-  stage: deploy
-  script:
-    - echo "The site will be deployed to $CI_PAGES_URL"
-  artifacts:
-    paths:
-      - public
-  rules:
-    - if: $CI_COMMIT_BRANCH == $CI_DEFAULT_BRANCH

README.md

@@ -1,6 +1,8 @@
 # BSc Leon Vatthauer
 
 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/
 
 ## Running the project
 TODO
@@ -14,32 +16,11 @@ So far the contributions are:
     - `Categories.Category.Distributive`
     - `Categories.Category.Extensive.Bundle`
     - `Categories.Category.Extensive.Properties.Distributive`
-3. Commutative categories [TODO]
+3. Parametrized (or stable) natural numbers objects [[WIP](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 categories [TODO]
 
-## Goals
-- [ ] `Monad.Instance.Delay`
-    - [X] Formalize the delay monad (as kleisli triple)
-    - [ ] Show that a strong delay monad is commutative (also needs formalization of strong delay monad)
-- [X] `ElgotAlgebra.agda`
-    - [X] Formalize (un-)guarded elgot-algebra.
-    - [X] Show the equivalence of `#-Folding` and `#-Compositionality` in the unguarded case. (*Proposition 10*)
-- [ ] `ElgotAlgebras.agda`
-    - [X] Formalize the category of elgot algebras for a given carrier.
-    - [X] Show existence of products in this category
-    - [ ] Show existence of exponentials (if carrier has exponentials)
-- [ ] `ElgotMonad.agda` [TODO]
-    - [ ] Formalize (strong) (pre) elgot monad
-    - [ ] Show ElgotMonad->PreElgotMonat
-- [ ] Monad K [TODO]
-    - [ ] Definitions using free uniform iteration algebras
-    - [ ] strength
-    - [ ] stable free uniform iteration algebras (and the relation to CCC carriers)
-- [ ] ...
-- [ ] Theorem 37 [TODO] (final goal)
-
-## Roadmap
-TODO
-
-## TODOs
-- [ ] Create Roadmap (find what theorem 37 depends on and then create a game plan)
-- [X] Refactor `ElgotAlgebras.agda` using `Categories.Morphism.Reasoning` (nicer proofs)
+## TODO
+TODOs are found inside the literate agda files!