🎨 rewrite index

.gitattributes

@@ -0,0 +1,2 @@
+*.lagda.md linguist-language=Literate Agda
+*.lagda.md linguist-detectable=true

.gitignore

@@ -1,7 +1,7 @@
 *.agdai
 *.pdf
 *.log
-Everything.agda
+src/Everything.agda
 public/
 .direnv
 .DS_Store

Makefile

@@ -9,19 +9,19 @@ pandoc: public/*.md
 	)
 
 agda: Everything.agda
-	agda --html --html-dir=public index.lagda.md --html-highlight=auto -i.
+	agda --html --html-dir=public src/index.lagda.md --html-highlight=auto -i.
 	rm -f public/Agda.css
 	cp Agda.css public/Agda.css
 
 clean:
-	rm -f  Everything.agda
+	rm -f src/Everything.agda
 	rm -rf public/*
 	find . -name '*.agdai' -exec rm \{\} \;
 
 # push compiled html to my cip directory
 push: all push'
 
-# just push without building
+# just push to CIP without rebuilding
 push':
 	chmod +w public/Agda.css
 	mv public bsc-thesis
@@ -29,7 +29,7 @@ push':
 	mv bsc-thesis public
 
 Everything.agda:
-	git ls-tree --full-tree -r --name-only HEAD | egrep '^src/[^\.]*.l?agda(\.md)?' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' -e 's/..md//' | LC_COLLATE='C' sort > Everything.agda
+	git ls-tree --full-tree -r --name-only HEAD | egrep '^src/[^\.]*.l?agda(\.md)?' | grep -v 'index.lagda.md' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' -e 's/..md//' | LC_COLLATE='C' sort > src/Everything.agda
 
 open:
 	firefox public/index.html

index.lagda.md

@@ -1,55 +0,0 @@
-# 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
-open import Monad.Instance.Delay.Strong
-open import Monad.Instance.Delay.Commutative
-```
-
-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
-open import Monad.Instance.K.Strong
-```
-
-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
-```

src/Misc/Algebra/Elgot/Properties.lagda.md

@@ -13,13 +13,16 @@ open import Categories.Functor.Coalgebra
 ```
 -->
 
+## Note
+This is currently removed, it would be needed for Theorem 35, 2⇒3
+
 ## Summary
 Some properties of elgot-algebras, namely:
 
 - Every elgot-algebra `(A, α : D₀ A ⇒ A)` satisfies `α (extend ι) ≈ α (D₁ π₁)` **[Lemma 32]**
 
 ```agda 
-module Algebra.Elgot.Properties {o ℓ e} (ambient : Ambient o ℓ e) where
+module Misc.Algebra.Elgot.Properties {o ℓ e} (ambient : Ambient o ℓ e) where
   open Ambient ambient
   open import Monad.Instance.Delay ambient using (DelayM)
   open import Algebra.ElgotAlgebra ambient

src/Misc/IsMonad.lagda.md

@@ -11,8 +11,10 @@ open import Categories.NaturalTransformation
 # Monads
 In this file we define some predicates like 'F extends to a monad'
 
+TODO: not needed without theorem 35
+
 ```agda
-module Monad.Core {o ℓ e} (C : Category o ℓ e) where
+module Misc.IsMonad {o ℓ e} (C : Category o ℓ e) where
   record ExtendsToMonad (F : Endofunctor C) : Set (o ⊔ ℓ ⊔ e) where
     field
       η : NaturalTransformation idF F

src/Misc/Kleene.lagda.md

@@ -1,5 +1,6 @@
 <!--
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Data.Product using (_,_)
 open import Category.Instance.AmbientCategory
@@ -13,10 +14,15 @@ import Monad.Instance.K as MIK
 ```
 -->
 
+# Obsolete
+This module contains some facts that are no longer needed, since Theorem 27 is not needed, namely:
 
+- primitive recursion and induction for PNNO
+- pre-order on a restriction category
+- restrict operator
 
 ```agda
-module Monad.Instance.K.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
+module Misc.Kleene {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
   open Ambient ambient
   open import Monad.Instance.K.Strong ambient MK
   open import Monad.Instance.K.Commutative ambient MK

src/Misc/Monad/Instance/Delay/Properties.lagda.md

@@ -17,7 +17,7 @@ open import Misc.FreeObject
 -->
 
 ```agda
-module Monad.Instance.Delay.Properties {o ℓ e} (ambient : Ambient o ℓ e) where
+module Misc.Monad.Instance.Delay.Properties {o ℓ e} (ambient : Ambient o ℓ e) where
   open Ambient ambient
   open import Categories.Diagram.Coequalizer C 
   open import Monad.Instance.Delay ambient

src/Monad/ElgotMonad.lagda.md

@@ -12,6 +12,8 @@ open import Categories.Functor
 ## Summary
 This file introduces Elgot Monads.
 
+TODO: Probably only Pre-Elgot is needed
+
 - [X] *Definition 13* Pre-Elgot Monads
 - [ ] *Definition 13* strong pre-Elgot
 - [X] *Definition 14* Elgot Monads

src/Monad/Instance/K/Compositionality.lagda.md

@@ -0,0 +1,5 @@
+# TODO: every KX satisfies compositionality
+
+```agda
+module Monad.Instance.K.Compositionality where
+```

src/index.lagda.md

@@ -0,0 +1,88 @@
+# 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 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 is an implementation of this paper by Sergey Goncharov: [arxiv](https://arxiv.org/abs/2102.11828)
+
+## Index
+
+### Preliminaries
+
+The work takes place in an ambient category that fits our needs:
+
+```agda
+open import Category.Instance.AmbientCategory
+```
+
+### Delay Monad
+
+We start out by formalizing Capretta's *Delay Monad* in a categorical setting and then proving that it is strong and commutative.
+
+```agda
+open import Monad.Instance.Delay
+open import Monad.Instance.Delay.Strong
+open import Monad.Instance.Delay.Commutative
+```
+
+The next step is to quotient the delay monad by weak bisimilarity, but this quotiented structure is not monadic, so we postulate conditions under which it extends to a monad.
+
+```agda
+open import Monad.Instance.Delay.Quotienting
+```
+
+### Monad K
+
+The goal of this last section is to formalize an equational lifting monad **K** that generalizes both the maybe monad and the delay monad.
+
+To do so we first need to look at iteration structures, i.e. functor algebras with an iteration operator.
+We differentiate between two kinds of iteration structures, *Elgot algebras* and *uniform-iteration algebras* where the latter is less restrictive than the former.
+
+```agda
+open import Algebra.ElgotAlgebra
+open import Algebra.UniformIterationAlgebra
+```
+
+Afterwards we also introduce categories of iteration algebras with iteration preserving morphisms:
+
+```agda
+open import Category.Construction.ElgotAlgebras
+open import Category.Construction.UniformIterationAlgebras
+```
+
+Lastly we need a notion of *stability* for uniform-iteration algebras:
+
+```agda
+open import Algebra.Properties
+```
+
+With this in hand we can now define *KX* as a *free uniform-iteration algebra* and proof that under *stability* it is a strong monad.
+
+```agda
+open import Monad.Instance.K
+open import Monad.Instance.K.Strong
+```
+
+The next step is to show that every *KX* satisfies compositionality, meaning that each *KX* is an Elgot algebra.
+
+```agda
+open import Monad.Instance.K.Compositionality
+```
+
+and with this we can show that K is and equational lifting monad, i.e. a commutative monad satisfying the equational lifting law:
+
+```agda
+open import Monad.Instance.K.Commutative
+open import Monad.Instance.K.EquationalLifting
+```
+
+and lastly we formalize the notion of *pre-Elgot monad* and show that **K** is pre-Elgot.
+
+```agda
+open import Monad.ElgotMonad
+-- open import Monad.Instance.K.PreElgot TODO
+```

src/thesis/motivation.agda

@@ -1,75 +0,0 @@
-{-# 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