From 47035c1e52911a2a2bc49bdbc283e1d82dba669d Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Thu, 12 Oct 2023 21:39:36 +0200 Subject: [PATCH] =?UTF-8?q?=E2=9C=A8=20Added=20index=20with=20some=20nice?= =?UTF-8?q?=20text?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Makefile | 3 +- index.lagda.md | 52 ++++++++++++++++++++ src/Monad/Instance/Delay/Properties.lagda.md | 1 + src/Monad/Instance/K.lagda.md | 1 + 4 files changed, 55 insertions(+), 2 deletions(-) create mode 100644 index.lagda.md diff --git a/Makefile b/Makefile index d52d115..cc9cd48 100644 --- a/Makefile +++ b/Makefile @@ -9,10 +9,9 @@ pandoc: public/*.md ) agda: Everything.agda - agda --html --html-dir=public Everything.agda --html-highlight=auto -i. + agda --html --html-dir=public index.lagda.md --html-highlight=auto -i. rm -f public/Agda.css cp Agda.css public/Agda.css - mv public/Everything.html public/index.html clean: rm -f Everything.agda diff --git a/index.lagda.md b/index.lagda.md new file mode 100644 index 0000000..05d0606 --- /dev/null +++ b/index.lagda.md @@ -0,0 +1,52 @@ +# Implementing Categorical Notions of Partiality and Delay in Agda + +To see a full list of all the modules go to: + +```agda +open import Everything +``` + +For my bachelor's thesis I am implementing categorical notions of partiality in agda using the *agda-categories* library. The repo for this project can be found [here](https://git8.cs.fau.de/theses/bsc-leon-vatthauer). +This mostly is an implementation of this paper by Sergey Goncharov: [arxiv](https://arxiv.org/abs/2102.11828) + +## Structure + +We start out by formalizing Caprettas Delay Monad in category theory by existence of final coalgebras and showing that it is strong. + +```agda +open import Monad.Instance.Delay +``` + +The next step is to quotient the delay monad by weak bisimilarity, in category theory this corresponds to existence of fitting coequalizers. +This quotiented structure is not directly monadic, we implement conditions under which it extends to a monad and prove it. + +```agda +open import Monad.Instance.Delay.Quotienting +``` + +Next come some basic definitions of iteration algebras, we differentiate between uniform-iteration algebras and (un-)guarded elgot algebras: + +```agda +open import Algebra.ElgotAlgebra +open import Category.Construction.ElgotAlgebras +open import Algebra.UniformIterationAlgebra +open import Category.Construction.UniformIterationAlgebras +``` + +Existence of free uniform-iteration algebras yields a monad that is of interest to us, we call it **K** and want to show some of it's properties (i.e. that it is strong and an equational lifting monad): + +```agda +open import Monad.Instance.K -- TODO move to Monad.Construction.K +``` + +Later we will also show that free uniform-iteration algebras coincide with free elgot algebras + +```agda +-- TODO +``` + +For the final step we will come back to the quotiented delay monad and show that under variations of the axiom of countable choice it is an explicit construction for the aforementioned monad **K**. + +```agda +open import Monad.Instance.Delay.Properties +``` \ No newline at end of file diff --git a/src/Monad/Instance/Delay/Properties.lagda.md b/src/Monad/Instance/Delay/Properties.lagda.md index 5c266b1..2ea1c8c 100644 --- a/src/Monad/Instance/Delay/Properties.lagda.md +++ b/src/Monad/Instance/Delay/Properties.lagda.md @@ -1,5 +1,6 @@